Merge branch 'master' into chore/copy-spelling

Author: FordUniver

Mathlib.lean

@@ -232,6 +232,7 @@ public import Mathlib.Algebra.Category.Ring.FinitePresentation
 public import Mathlib.Algebra.Category.Ring.Instances
 public import Mathlib.Algebra.Category.Ring.Limits
 public import Mathlib.Algebra.Category.Ring.LinearAlgebra
+public import Mathlib.Algebra.Category.Ring.Small
 public import Mathlib.Algebra.Category.Ring.Topology
 public import Mathlib.Algebra.Category.Ring.Under.Basic
 public import Mathlib.Algebra.Category.Ring.Under.Limits
@@ -5654,6 +5655,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
@@ -6407,6 +6409,7 @@ public import Mathlib.RingTheory.Flat.EquationalCriterion
 public import Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
 public import Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
 public import Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
+public import Mathlib.RingTheory.Flat.IsBaseChange
 public import Mathlib.RingTheory.Flat.Localization
 public import Mathlib.RingTheory.Flat.Rank
 public import Mathlib.RingTheory.Flat.Stability
@@ -6843,6 +6846,7 @@ public import Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
 public import Mathlib.RingTheory.TensorProduct.IsBaseChangeFree
 public import Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
 public import Mathlib.RingTheory.TensorProduct.IsBaseChangePi
+public import Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact
 public import Mathlib.RingTheory.TensorProduct.Maps
 public import Mathlib.RingTheory.TensorProduct.MonoidAlgebra
 public import Mathlib.RingTheory.TensorProduct.MvPolynomial

Mathlib/Algebra/Algebra/Defs.lean

@@ -386,7 +386,7 @@ instance (priority := 1100) id : Algebra R R where
   -- be made so without a significant performance hit.
   -- see library note [reducible non-instances].
   toSMul := instSMulOfMul
-  __ := ({ RingHom.id R with toFun x := x }).toAlgebra
+  __ := (RingHom.id R).toAlgebra
 
 @[simp] lemma linearMap_self : Algebra.linearMap R R = .id := rfl
 

Mathlib/Algebra/Category/CommAlgCat/FiniteType.lean

@@ -47,6 +47,13 @@ lemma Algebra.FiniteType.exists_fgAlgCatSkeleton (A : Type v) [CommRing A] [Alge
   obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h
   exact ⟨⟨n, RingHom.ker f⟩, ⟨(Ideal.quotientKerAlgEquivOfSurjective hf).symm⟩⟩
 
+lemma RingHom.FiniteType.exists_smallRepr {S : Type v} [CommRing S] {f : R →+* S}
+    (hf : f.FiniteType) :
+    ∃ (T : FGAlgCatSkeleton R) (e : T.eval.obj ≃+* S), f = e.toRingHom.comp (algebraMap _ _) := by
+  algebraize [f]
+  obtain ⟨T, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R S
+  exact ⟨T, e.symm.toRingEquiv, e.symm.toAlgHom.comp_algebraMap.symm⟩
+
 /-- Universe lift functor for finitely generated algebras. -/
 def FGAlgCat.uliftFunctor : FGAlgCat.{v} R ⥤ FGAlgCat.{max v w} R where
   obj A := ⟨.of R <| ULift A.1, .equiv inferInstance ULift.algEquiv.symm⟩

Mathlib/Algebra/Category/Grp/FilteredColimits.lean

@@ -130,7 +130,7 @@ noncomputable def colimitCocone : Cocone F where
   ι.app J := GrpCat.ofHom ((MonCat.FilteredColimits.colimitCocone
     (F ⋙ forget₂ GrpCat MonCat)).ι.app J).hom
   ι.naturality _ _ f := (forget₂ _ MonCat).map_injective
-    ((MonCat.FilteredColimits.colimitCocone _).ι.naturality f)
+    ((MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ GrpCat MonCat)).ι.naturality f)
 
 /-- The proposed colimit cocone is a colimit in `GrpCat`. -/
 @[to_additive /-- The proposed colimit cocone is a colimit in `AddGroup`. -/]
@@ -191,7 +191,7 @@ noncomputable def colimitCocone : Cocone F where
   ι.app J := CommGrpCat.ofHom
     ((GrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommGrpCat GrpCat)).ι.app J).hom
   ι.naturality _ _ f := (forget₂ _ GrpCat).map_injective
-    ((GrpCat.FilteredColimits.colimitCocone _).ι.naturality f)
+    ((GrpCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommGrpCat GrpCat)).ι.naturality f)
 
 /-- The proposed colimit cocone is a colimit in `CommGrpCat`. -/
 @[to_additive /-- The proposed colimit cocone is a colimit in `AddCommGroup`. -/]

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -421,7 +421,7 @@ def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y :=
     ext x
     simp [coe_freeObj]⟩
 
-lemma freeMap_map {X Y : TopCat} (f : X ⟶ Y) (v : X →₀ R) :
+lemma freeMap_map {X Y : TopCat.{v}} (f : X ⟶ Y) (v : X →₀ R) :
     (freeMap R f : (X →₀ R) → (Y →₀ R)) v = Finsupp.mapDomain f.hom v := rfl
 
 /-- The free topological module over a topological space as a functor.

Mathlib/Algebra/Category/Ring/Small.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+module
+
+public import Mathlib.Algebra.Category.CommAlgCat.FiniteType
+public import Mathlib.CategoryTheory.ObjectProperty.Small
+
+
+/-! # Smallness results on the category of `CommRing` -/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory
+
+namespace CommRingCat
+
+variable {P Q : ObjectProperty CommRingCat.{u}}
+
+lemma essentiallySmall_of_finiteType [ObjectProperty.EssentiallySmall.{u} Q]
+    (hPQ : ∀ S, P S → ∃ R, Q R ∧ ∃ (f : R ⟶ S), f.hom.FiniteType) :
+    ObjectProperty.EssentiallySmall.{u} P := by
+  obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
+  let f (S : Σ R : Subtype Q', FGAlgCatSkeleton R) : CommRingCat := .of S.2.eval.obj
+  refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
+  obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS
+  wlog hR' : Q' R generalizing R
+  · obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR
+    exact this R' (hQ'Q _ hR') (e.inv ≫ φ)
+      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'
+  obtain ⟨T, e, he⟩ := hφ.exists_smallRepr
+  exact ⟨_, ⟨⟨_, hR'⟩, T⟩, ⟨RingEquiv.toCommRingCatIso e.symm⟩⟩
+
+lemma essentiallySmall_of_localizationAway [ObjectProperty.EssentiallySmall.{u} Q]
+    (hPQ : ∀ S, P S → ∃ s : Set S, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (.of (Localization.Away f))) :
+    ObjectProperty.EssentiallySmall.{u} P := by
+  obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
+  let f (S : Σ (n : ℕ) (R : Fin n → Subtype Q'), Subring (Π i, (R i).1)) : CommRingCat := .of S.2.2
+  refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
+  obtain ⟨s, hs, H⟩ := hPQ S hS
+  wlog hs' : s.Finite generalizing s
+  · obtain ⟨s', hs's, hs'⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
+    exact this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet
+  choose S' hS' e using fun (f : s) ↦ hQQ' _ (H _ f.2)
+  let φ : S →+* Π i, S' (hs'.equivFin.symm i) :=
+    ((RingEquiv.piCongrRight fun i ↦ (e i).some.commRingCatIsoToRingEquiv).trans
+      (RingEquiv.piCongrLeft (S' ·) hs'.equivFin.symm).symm).toRingHom.comp (algebraMap _ _)
+  have hφ : Function.Injective φ := by
+    dsimp only [RingHom.coe_comp, φ]
+    refine (RingEquiv.injective _).comp (Localization.algebraMap_injective_of_span_eq_top _ hs)
+  refine ⟨_, ⟨Nat.card s, (fun f ↦ ⟨S' f, hS' f⟩) ∘ hs'.equivFin.symm, φ.range⟩, ⟨?_⟩⟩
+  exact (RingEquiv.ofBijective φ.rangeRestrict
+    ⟨φ.injective_codRestrict.mpr hφ, φ.rangeRestrict_surjective⟩).toCommRingCatIso
+
+end CommRingCat

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -717,19 +717,22 @@ alias isDedekindFiniteMonoid_of_injective := IsDedekindFiniteMonoid.of_injective
 end MonoidHom
 
 /-- The identity map from a type with 1 to itself. -/
-@[to_additive (attr := simps) /-- The identity map from a type with zero to itself. -/]
+@[to_additive (attr := simps, implicit_reducible)
+/-- The identity map from a type with zero to itself. -/]
 def OneHom.id (M : Type*) [One M] : OneHom M M where
   toFun x := x
   map_one' := rfl
 
 /-- The identity map from a type with multiplication to itself. -/
-@[to_additive (attr := simps) /-- The identity map from a type with addition to itself. -/]
+@[to_additive (attr := simps, implicit_reducible)
+/-- The identity map from a type with addition to itself. -/]
 def MulHom.id (M : Type*) [Mul M] : M →ₙ* M where
   toFun x := x
   map_mul' _ _ := rfl
 
 /-- The identity map from a monoid to itself. -/
-@[to_additive (attr := simps) /-- The identity map from an additive monoid to itself. -/]
+@[to_additive (attr := simps, implicit_reducible)
+/-- The identity map from an additive monoid to itself. -/]
 def MonoidHom.id (M : Type*) [MulOne M] : M →* M where
   toFun x := x
   map_one' := rfl
@@ -745,22 +748,23 @@ lemma MulHom.coe_id {M : Type*} [Mul M] : (MulHom.id M : M → M) = _root_.id :=
 lemma MonoidHom.coe_id {M : Type*} [MulOne M] : (MonoidHom.id M : M → M) = _root_.id := rfl
 
 /-- Composition of `OneHom`s as a `OneHom`. -/
-@[to_additive /-- Composition of `ZeroHom`s as a `ZeroHom`. -/]
+@[to_additive (attr := implicit_reducible) /-- Composition of `ZeroHom`s as a `ZeroHom`. -/]
 def OneHom.comp [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) : OneHom M P where
-  toFun := hnp ∘ hmn
+  toFun x := hnp (hmn x)
   map_one' := by simp
 
 /-- Composition of `MulHom`s as a `MulHom`. -/
-@[to_additive /-- Composition of `AddHom`s as an `AddHom`. -/]
+@[to_additive (attr := implicit_reducible) /-- Composition of `AddHom`s as an `AddHom`. -/]
 def MulHom.comp [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) : M →ₙ* P where
-  toFun := hnp ∘ hmn
+  toFun x := hnp (hmn x)
   map_mul' x y := by simp
 
 /-- Composition of monoid morphisms as a monoid morphism. -/
-@[to_additive /-- Composition of additive monoid morphisms as an additive monoid morphism. -/]
+@[to_additive (attr := implicit_reducible)
+/-- Composition of additive monoid morphisms as an additive monoid morphism. -/]
 def MonoidHom.comp [MulOne M] [MulOne N] [MulOne P] (hnp : N →* P) (hmn : M →* N) :
     M →* P where
-  toFun := hnp ∘ hmn
+  toFun x := hnp (hmn x)
   map_one' := by simp
   map_mul' := by simp
 

Mathlib/Algebra/Homology/Additive.lean

@@ -214,8 +214,7 @@ theorem map_chain_complex_of (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (X :
         rw [← F.map_comp, sq n, Functor.map_zero] := by
   refine HomologicalComplex.ext rfl ?_
   rintro i j (rfl : j + 1 = i)
-  simp only [CategoryTheory.Functor.mapHomologicalComplex_obj_d, of_d, eqToHom_refl, comp_id,
-    id_comp]
+  simp
 
 end ChainComplex
 

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -631,32 +631,34 @@ section Of
 
 variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 
+/-- Auxiliary definition for differentials for `ChainComplex.of`. -/
+def of.d (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (i : α) (j : α) : X i ⟶ X j :=
+  if h : i = j + 1 then eqToHom (by rw [h]) ≫ d j else 0
+
 /-- Construct an `α`-indexed chain complex from a dependently-typed differential.
 -/
-def of (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) : ChainComplex V α :=
+abbrev of (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) :
+    ChainComplex V α :=
   { X := X
-    d := fun i j => if h : i = j + 1 then eqToHom (by rw [h]) ≫ d j else 0
-    shape := fun i j w => by
-      rw [dif_neg (Ne.symm w)]
+    d := of.d X d
+    shape := fun i j w => by simp [of.d, (Ne.symm w)]
     d_comp_d' := fun i j k hij hjk => by
-      dsimp at hij hjk
+      dsimp [of.d] at hij hjk ⊢
       substs hij hjk
       simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq] }
 
 variable (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0)
 
-@[simp]
 theorem of_X : (of X d sq).X = X :=
   rfl
 
 @[simp]
-theorem of_d (j : α) : (of X d sq).d (j + 1) j = d j := by
-  dsimp [of]
+theorem of_d (j : α) : of.d X d (j + 1) j = d j := by
+  dsimp [of.d]
   rw [if_pos rfl, Category.id_comp]
 
-theorem of_d_ne {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0 := by
-  rw [of]
-  simp [dif_neg h]
+theorem of_d_ne {i j : α} (h : i ≠ j + 1) : of.d X d i j = 0 := by
+  simp [of.d, dif_neg h]
 
 end Of
 
@@ -674,7 +676,7 @@ def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f (i + 1) ≫ d_Y i
     of X d_X sq_X ⟶ of Y d_Y sq_Y :=
   { f
     comm' := fun n m => by
-      simp only [ComplexShape.down_Rel]
+      simp only [of.d, ComplexShape.down_Rel]
       rintro rfl
       simpa using comm m }
 
@@ -739,7 +741,7 @@ lemma mkAux_eq_shortComplex_mk_d_comp_d (n : ℕ) :
     mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
       ShortComplex.mk _ _ ((mk X₀ X₁ X₂ d₀ d₁ s succ).d_comp_d (n + 2) (n + 1) n) := by
   rw [show n + 2 = n + 1 + 1 from rfl]
-  simp only [mk, of_X, of_d, mkAux]
+  simp [mk, mkAux]
 
 /-- The isomorphism from `(mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3)` that is given by
 the inductive construction. -/
@@ -760,7 +762,7 @@ lemma mk_d (n : ℕ) :
   set_option backward.isDefEq.respectTransparency false in
     rw [eqToHom_refl, comp_id] at eq
   refine Eq.trans ?_ eq
-  dsimp only [mk, of]
+  dsimp only [mk, of, of.d]
   rw [dif_pos (by rfl), eqToHom_refl, id_comp]
   rfl
 
@@ -797,7 +799,7 @@ def mk'XIso (n : ℕ) :
     (mk' X₀ X₁ d₀ succ').X (n + 2) ≅ (succ' ((mk' X₀ X₁ d₀ succ').d (n + 1) n)).1 := by
   obtain _ | n := n
   · apply eqToIso
-    dsimp [mk', mk, of, mkAux]
+    dsimp [mk', mk, of, mkAux, of.d]
     rw [id_comp]
   · exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n
 
@@ -886,36 +888,36 @@ section Of
 
 variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 
+/-- Auxiliary definition for differentials for `CochainComplex.of`. -/
+def of.d (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (i : α) (j : α) : X i ⟶ X j :=
+  if h : i + 1 = j then d _ ≫ eqToHom (by rw [h]) else 0
+
 /-- Construct an `α`-indexed cochain complex from a dependently-typed differential.
 -/
-def of (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0) :
+abbrev of (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0) :
     CochainComplex V α :=
   { X := X
-    d := fun i j => if h : i + 1 = j then d _ ≫ eqToHom (by rw [h]) else 0
-    shape := fun i j w => by
-      rw [dif_neg]
-      exact w
+    d := of.d X d
+    shape := fun i j w => dif_neg (c := i + 1 = j) w
     d_comp_d' := fun i j k => by
-      dsimp
+      dsimp [of.d]
       split_ifs with h h' h'
       · substs h h'
         simp [sq]
       all_goals simp }
 
 variable (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0)
 
-@[simp]
 theorem of_X : (of X d sq).X = X :=
   rfl
 
 @[simp]
-theorem of_d (j : α) : (of X d sq).d j (j + 1) = d j := by
-  dsimp [of]
+theorem of_d (j : α) : of.d X d j (j + 1) = d j := by
+  dsimp [of.d]
   rw [if_pos rfl, Category.comp_id]
 
-theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : (of X d sq).d i j = 0 := by
-  rw [of]
-  simp [dif_neg h]
+theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : of.d X d i j = 0 := by
+  simp [of.d, dif_neg h]
 
 end Of
 
@@ -934,7 +936,7 @@ def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f i ≫ d_Y i = d_X
     of X d_X sq_X ⟶ of Y d_Y sq_Y :=
   { f
     comm' := fun n m => by
-      simp only [ComplexShape.up_Rel]
+      simp only [of.d, ComplexShape.up_Rel]
       rintro rfl
       simpa using comm n }