Merge branch 'master' into club

Author: vihdzp

.github/workflows/labels_from_comment.yml

@@ -29,7 +29,7 @@ jobs:
     steps:
     - name: Add / remove label based on comment
       run: |
-        labelArray=("awaiting-author" "awaiting-zulip" "WIP" "easy" "please-adopt" "help-wanted" "CI" "brownian" "carleson" "CFT" "FLT" "infinity-cosmos" "sphere-packing" "toric" "IMO" "t-algebra" "t-algebraic-geometry" "t-algebraic-topology" "t-analysis" "t-category-theory" "t-combinatorics" "t-computability" "t-condensed" "t-convex-geometry" "t-data" "t-differential-geometry" "t-dynamics" "t-euclidean-geometry" "t-geometric-group-theory" "t-group-theory" "t-linter" "t-logic" "t-measure-probability" "t-meta" "t-number-theory" "t-order" "t-ring-theory" "t-set-theory" "t-topology")
+        labelArray=("awaiting-author" "awaiting-zulip" "WIP" "easy" "please-adopt" "help-wanted" "CI" "brownian" "carleson" "CFT" "FLT" "infinity-cosmos" "sphere-packing" "toric" "LLM-generated" "IMO" "t-algebra" "t-algebraic-geometry" "t-algebraic-topology" "t-analysis" "t-category-theory" "t-combinatorics" "t-computability" "t-condensed" "t-convex-geometry" "t-data" "t-differential-geometry" "t-dynamics" "t-euclidean-geometry" "t-geometric-group-theory" "t-group-theory" "t-linter" "t-logic" "t-measure-probability" "t-meta" "t-number-theory" "t-order" "t-ring-theory" "t-set-theory" "t-topology")
 
         # we strip `\r` since line endings from GitHub contain this character
         COMMENT="${COMMENT//$'\r'/}"

Mathlib.lean

@@ -1554,6 +1554,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
+public import Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.Homotopy
 public import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
 public import Mathlib.AlgebraicTopology.SimplicialSet.Horn
@@ -2731,6 +2732,7 @@ public import Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
 public import Mathlib.CategoryTheory.GuitartExact.KanExtension
 public import Mathlib.CategoryTheory.GuitartExact.Opposite
 public import Mathlib.CategoryTheory.GuitartExact.Over
+public import Mathlib.CategoryTheory.GuitartExact.Quotient
 public import Mathlib.CategoryTheory.GuitartExact.VerticalComposition
 public import Mathlib.CategoryTheory.HomCongr
 public import Mathlib.CategoryTheory.Idempotents.Basic
@@ -2757,6 +2759,7 @@ public import Mathlib.CategoryTheory.LiftingProperties.Over
 public import Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
 public import Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
 public import Mathlib.CategoryTheory.Limits.Bicones
+public import Mathlib.CategoryTheory.Limits.Chosen.End
 public import Mathlib.CategoryTheory.Limits.ColimitLimit
 public import Mathlib.CategoryTheory.Limits.Comma
 public import Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
@@ -2942,6 +2945,7 @@ public import Mathlib.CategoryTheory.Limits.Types.ColimitType
 public import Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
 public import Mathlib.CategoryTheory.Limits.Types.Colimits
 public import Mathlib.CategoryTheory.Limits.Types.Coproducts
+public import Mathlib.CategoryTheory.Limits.Types.End
 public import Mathlib.CategoryTheory.Limits.Types.Equalizers
 public import Mathlib.CategoryTheory.Limits.Types.Filtered
 public import Mathlib.CategoryTheory.Limits.Types.Images
@@ -4405,6 +4409,7 @@ public import Mathlib.Dynamics.Newton
 public import Mathlib.Dynamics.OmegaLimit
 public import Mathlib.Dynamics.PeriodicPts.Defs
 public import Mathlib.Dynamics.PeriodicPts.Lemmas
+public import Mathlib.Dynamics.SymbolicDynamics.Basic
 public import Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
 public import Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
 public import Mathlib.Dynamics.TopologicalEntropy.NetEntropy
@@ -5684,6 +5689,7 @@ public import Mathlib.NumberTheory.ModularForms.Cusps
 public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.Delta
 public import Mathlib.NumberTheory.ModularForms.Derivative
+public import Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne
 public import Mathlib.NumberTheory.ModularForms.Discriminant
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
@@ -5701,6 +5707,7 @@ public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
+public import Mathlib.NumberTheory.ModularForms.LevelOne
 public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
 public import Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
@@ -6397,6 +6404,7 @@ public import Mathlib.RingTheory.Etale.Locus
 public import Mathlib.RingTheory.Etale.Pi
 public import Mathlib.RingTheory.Etale.QuasiFinite
 public import Mathlib.RingTheory.Etale.StandardEtale
+public import Mathlib.RingTheory.Etale.Weakly
 public import Mathlib.RingTheory.EuclideanDomain
 public import Mathlib.RingTheory.Extension.Basic
 public import Mathlib.RingTheory.Extension.Cotangent.BaseChange
@@ -7094,6 +7102,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Core
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.DSimpPercent
 public import Mathlib.Tactic.DeclarationNames
 public import Mathlib.Tactic.DefEqAbuse
@@ -7298,6 +7307,7 @@ public import Mathlib.Tactic.Says
 public import Mathlib.Tactic.ScopedNS
 public import Mathlib.Tactic.Set
 public import Mathlib.Tactic.SetLike
+public import Mathlib.Tactic.SetNotationForOrder
 public import Mathlib.Tactic.SimpIntro
 public import Mathlib.Tactic.SimpRw
 public import Mathlib.Tactic.Simproc.Divisors
@@ -7309,7 +7319,6 @@ public import Mathlib.Tactic.Simps.Basic
 public import Mathlib.Tactic.Simps.NotationClass
 public import Mathlib.Tactic.SplitIfs
 public import Mathlib.Tactic.Spread
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Substs
 public import Mathlib.Tactic.SuccessIfFailWithMsg
@@ -7715,6 +7724,7 @@ public import Mathlib.Topology.Hom.ContinuousEvalConst
 public import Mathlib.Topology.Hom.Open
 public import Mathlib.Topology.Homeomorph.Defs
 public import Mathlib.Topology.Homeomorph.Lemmas
+public import Mathlib.Topology.Homeomorph.Quotient
 public import Mathlib.Topology.Homeomorph.TransferInstance
 public import Mathlib.Topology.Homotopy.Affine
 public import Mathlib.Topology.Homotopy.Basic
@@ -8009,6 +8019,7 @@ public import Mathlib.Topology.UrysohnsBounded
 public import Mathlib.Topology.UrysohnsLemma
 public import Mathlib.Topology.VectorBundle.Basic
 public import Mathlib.Topology.VectorBundle.Constructions
+public import Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
 public import Mathlib.Topology.VectorBundle.FiniteDimensional
 public import Mathlib.Topology.VectorBundle.Hom
 public import Mathlib.Topology.VectorBundle.Riemannian

Mathlib/Algebra/Algebra/Equiv.lean

@@ -278,16 +278,11 @@ theorem mk_coe' (e : A₁ ≃ₐ[R] A₂) (f h₁ h₂ h₃ h₄ h₅) :
     (⟨⟨f, e, h₁, h₂⟩, h₃, h₄, h₅⟩ : A₂ ≃ₐ[R] A₁) = e.symm :=
   symm_bijective.injective <| ext fun _ => rfl
 
-/-- Auxiliary definition to avoid looping in `dsimp` with `AlgEquiv.symm_mk`. -/
-protected def symm_mk.aux (f f') (h₁ h₂ h₃ h₄ h₅) :=
-  (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm
-
 @[simp]
-theorem symm_mk (f f') (h₁ h₂ h₃ h₄ h₅) :
-    (⟨⟨f, f', h₁, h₂⟩, h₃, h₄, h₅⟩ : A₁ ≃ₐ[R] A₂).symm =
-      { symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ with
-        toFun := f'
-        invFun := f } :=
+theorem symm_mk (e : A₁ ≃ A₂) (h₁ h₂ h₃) : dsimp%
+    (mk e h₁ h₂ h₃ : A₁ ≃ₐ[R] A₂).symm =
+      { (mk e h₁ h₂ h₃ : A₁ ≃ₐ[R] A₂).symm with
+        toEquiv := e.symm } :=
   rfl
 
 @[simp]

Mathlib/Algebra/Lie/Classical.lean

@@ -238,8 +238,10 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) :
 
 It looks like this as a `2l x 2l` matrix of `l x l` blocks:
 
-   [ 0 1 ]
-   [ 1 0 ]
+```
+[ 0 1 ]
+[ 1 0 ]
+```
 -/
 def JD : Matrix (l ⊕ l) (l ⊕ l) R :=
   Matrix.fromBlocks 0 1 1 0
@@ -254,9 +256,10 @@ diagonal matrix.
 
 It looks like this as a `2l x 2l` matrix of `l x l` blocks:
 
-   [ 1 -1 ]
-   [ 1  1 ]
--/
+```
+[ 1 -1 ]
+[ 1  1 ]
+``` -/
 def PD : Matrix (l ⊕ l) (l ⊕ l) R :=
   Matrix.fromBlocks 1 (-1) 1 1
 
@@ -295,15 +298,19 @@ noncomputable def typeDEquivSo' [Fintype l] [Invertible (2 : R)] : typeD l R ≃
 
 It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
 
-   [ 2 0 0 ]
-   [ 0 0 1 ]
-   [ 0 1 0 ]
+```
+[ 2 0 0 ]
+[ 0 0 1 ]
+[ 0 1 0 ]
+```
 
 where sizes of the blocks are:
 
-   [`1 x 1` `1 x l` `1 x l`]
-   [`l x 1` `l x l` `l x l`]
-   [`l x 1` `l x l` `l x l`]
+```
+[`1 x 1` `1 x l` `1 x l`]
+[`l x 1` `l x l` `l x l`]
+[`l x 1` `l x l` `l x l`]
+```
 -/
 def JB :=
   Matrix.fromBlocks ((2 : R) • (1 : Matrix Unit Unit R)) 0 0 (JD l R)
@@ -318,16 +325,19 @@ almost-split-signature diagonal matrix.
 
 It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:
 
-   [ 1 0  0 ]
-   [ 0 1 -1 ]
-   [ 0 1  1 ]
+```
+[ 1 0  0 ]
+[ 0 1 -1 ]
+[ 0 1  1 ]
+```
 
 where sizes of the blocks are:
 
-   [`1 x 1` `1 x l` `1 x l`]
-   [`l x 1` `l x l` `l x l`]
-   [`l x 1` `l x l` `l x l`]
--/
+```
+[`1 x 1` `1 x l` `1 x l`]
+[`l x 1` `l x l` `l x l`]
+[`l x 1` `l x l` `l x l`]
+``` -/
 def PB :=
   Matrix.fromBlocks (1 : Matrix Unit Unit R) 0 0 (PD l R)
 

Mathlib/Algebra/Lie/OfAssociative.lean

@@ -71,9 +71,9 @@ bracket equal to its ring commutator.
 
 Note that this cannot be a global instance because it would create a diamond when `M = A`,
 specifically we can build two mathematically-different `bracket A A`s:
- 1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
- 2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
-    (and thus `⁅a, b⁆ = a * b`)
+1. `@Ring.bracket A _` which says `⁅a, b⁆ = a * b - b * a`
+2. `(@LieRingModule.ofAssociativeModule A _ A _ _).toBracket` which says `⁅a, b⁆ = a • b`
+  (and thus `⁅a, b⁆ = a * b`)
 
 See note [reducible non-instances] -/
 abbrev LieRingModule.ofAssociativeModule : LieRingModule A M where

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -528,15 +528,12 @@ theorem mk_coe' (f h₁ h₂ h₃ h₄) :
     (LinearEquiv.mk ⟨⟨f, h₁⟩, h₂⟩ (⇑e) h₃ h₄ : M₂ ≃ₛₗ[σ'] M) = e.symm :=
   symm_bijective.injective <| ext fun _ ↦ rfl
 
-/-- Auxiliary definition to avoid looping in `dsimp` with `LinearEquiv.symm_mk`. -/
-protected def symm_mk.aux (f h₁ h₂ h₃ h₄) := (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm
-
 @[simp]
-theorem symm_mk (f h₁ h₂ h₃ h₄) :
-    (⟨⟨⟨e, h₁⟩, h₂⟩, f, h₃, h₄⟩ : M ≃ₛₗ[σ] M₂).symm =
-      { symm_mk.aux e f h₁ h₂ h₃ h₄ with
-        toFun := f
-        invFun := e } :=
+theorem symm_mk (toLinearMap invFun h₁ h₂) : dsimp%
+    (mk toLinearMap invFun h₁ h₂ : M ≃ₛₗ[σ] M₂).symm =
+      { (mk toLinearMap invFun h₁ h₂ : M ≃ₛₗ[σ] M₂).symm with
+        toFun := invFun
+        invFun := toLinearMap } :=
   rfl
 
 /-- For a more powerful version, see `coe_symm_mk'`. -/

Mathlib/Algebra/Module/Projective.lean

@@ -48,13 +48,6 @@ and it's unclear if projective modules are even a useful notion.
 
 https://en.wikipedia.org/wiki/Projective_module
 
-## TODO
-
-- Direct sum of two projective modules is projective.
-- Arbitrary sum of projective modules is projective.
-
-All of these should be relatively straightforward.
-
 ## Tags
 
 projective module

Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

@@ -33,6 +33,15 @@ Given a function `f : M → N` between magmas, return the corresponding map `R[M
 by summing the coefficients along each fiber of `f`. -/]
 abbrev mapDomain (f : M → N) (x : R[M]) : R[N] := Finsupp.mapDomain f x
 
+@[to_additive (attr := simp)]
+lemma coeff_mapDomain (f : M → N) (x : R[M]) :
+    (mapDomain f x).coeff = x.coeff.mapDomain f := rfl
+
+/-- This isn't marked as simp to avoid looping with unfolding `coeff`. -/
+@[to_additive /-- This isn't marked as simp to avoid looping with unfolding `coeff`. -/]
+lemma ofCoeff_mapDomain (f : M → N) (x : M →₀ R) :
+    ofCoeff (.mapDomain f x) = mapDomain f (ofCoeff x) := rfl
+
 @[to_additive]
 lemma mapDomain_zero (f : M → N) : mapDomain f (0 : R[M]) = 0 := Finsupp.mapDomain_zero ..
 
@@ -94,6 +103,28 @@ lemma map_id (x : R[M]) : map (.id R) x = x := by simp [map, coeff, ofCoeff]
 lemma map_map (f : S →+ T) (g : R →+ S) (x : R[M]) :
     map f (map g x) = map (f.comp g) x := by simp [map, coeff, ofCoeff]
 
+@[to_additive]
+lemma range_map (f : R →+ S) : Set.range (map (M := M) f) = {x | ∀ i, x.coeff i ∈ Set.range f} :=
+  calc
+    _ = coeffEquiv ⁻¹' (Set.range (mapRange f (map_zero f) ∘ coeffEquiv)) := by
+      simp_rw [comp_def, Equiv.eq_preimage_iff_image_eq, ← Set.range_comp', coeffEquiv_apply,
+        coeff_map]
+    _ = _ := by simp [Finsupp.range_mapRange]
+
+/-- `MonoidAlgebra.map` of an injective function is injective. -/
+@[to_additive /-- `AddMonoidAlgebra.map` of an injective function is injective. -/]
+lemma map_injective (f : R →+ S) (he : Injective f) : Injective (map (M := M) f) := by
+  have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
+    ext; simp [ofCoeff_mapRange]
+  simpa [this] using mapRange_injective _ (map_zero f) he
+
+/-- `MonoidAlgebra.map` of a surjective function is surjective. -/
+@[to_additive /-- `AddMonoidAlgebra.map` of an surjective function is surjective. -/]
+lemma map_surjective (f : R →+ S) (he : Surjective f) : Surjective (map (M := M) f) := by
+  have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
+    ext; simp [ofCoeff_mapRange]
+  simpa [this] using mapRange_surjective _ (map_zero f) he
+
 /-- Pullback the coefficients of an element of `R[N]` under an injective `f : M → N`.
 
 Coefficients not in the range of `f` are dropped. -/

Mathlib/Algebra/Order/IsBotOne.lean

@@ -6,9 +6,7 @@ Authors: Violeta Hernández Palacios
 module
 
 public import Mathlib.Algebra.Order.ZeroLEOne
-public import Mathlib.Tactic.ToAdditive
-public import Mathlib.Order.Max
-public import Mathlib.Order.BoundedOrder.Basic
+public import Mathlib.Order.BoundedOrder.Lattice
 
 /-!
 # Typeclasses expressing `IsBot 1` and `IsBot 0`
@@ -129,12 +127,26 @@ section LinearOrder
 variable [LinearOrder α] [One α] [IsBotOneClass α]
 
 @[to_additive]
-theorem one_min (a : α) : min 1 a = 1 :=
-  min_eq_left one_le
+theorem one_min (a : α) : min 1 a = 1 := by simp
 
 @[to_additive]
-theorem min_one (a : α) : min a 1 = 1 :=
-  min_eq_right one_le
+theorem min_one (a : α) : min a 1 = 1 := by simp
+
+@[to_additive]
+theorem one_max (a : α) : max 1 a = a := by simp
+
+@[to_additive]
+theorem max_one (a : α) : max a 1 = a := by simp
+
+@[to_additive (attr := simp)]
+theorem max_eq_one {a b : α} : max a b = 1 ↔ a = 1 ∧ b = 1 :=
+  let := IsBotOneClass.toOrderBot α
+  max_eq_bot
+
+@[to_additive (attr := simp)]
+theorem min_eq_one {a b : α} : min a b = 1 ↔ a = 1 ∨ b = 1 :=
+  let := IsBotOneClass.toOrderBot α
+  min_eq_bot
 
 end LinearOrder
 

Mathlib/Algebra/Polynomial/Splits.lean

@@ -537,6 +537,11 @@ section
 variable {A B : Type*} [CommRing R] [Field A] [Algebra R A]
   [CommRing B] [IsDomain B] [Algebra R B] {f : R[X]}
 
+theorem Splits.map_aroots_algebraMap [Algebra A B] [IsScalarTower R A B]
+    (hf : (f.map (algebraMap R A)).Splits) :
+    (f.aroots A).map (algebraMap A B) = f.aroots B := by
+  rw [← aroots_map B A, aroots, aroots, hf.roots_map]
+
 theorem Splits.image_rootSet (hf : (f.map (algebraMap R A)).Splits)
     (g : A →ₐ[R] B) : g '' f.rootSet A = f.rootSet B := by
   classical