minimize imports

Author: vihdzp

Mathlib.lean

@@ -158,6 +158,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
 public import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
 public import Mathlib.Algebra.Category.ModuleCat.EpiMono
+public import Mathlib.Algebra.Category.ModuleCat.Ext.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
 public import Mathlib.Algebra.Category.ModuleCat.Ext.Finite
 public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
@@ -779,6 +780,7 @@ public import Mathlib.Algebra.Module.LinearMap.Basic
 public import Mathlib.Algebra.Module.LinearMap.Defs
 public import Mathlib.Algebra.Module.LinearMap.DivisionRing
 public import Mathlib.Algebra.Module.LinearMap.End
+public import Mathlib.Algebra.Module.LinearMap.FiniteRange
 public import Mathlib.Algebra.Module.LinearMap.Polynomial
 public import Mathlib.Algebra.Module.LinearMap.Prod
 public import Mathlib.Algebra.Module.LinearMap.Rat
@@ -1690,6 +1692,7 @@ public import Mathlib.Analysis.CStarAlgebra.Unitary.Maps
 public import Mathlib.Analysis.CStarAlgebra.Unitary.Span
 public import Mathlib.Analysis.CStarAlgebra.Unitization
 public import Mathlib.Analysis.CStarAlgebra.lpSpace
+public import Mathlib.Analysis.Calculus.AbsolutelyMonotone
 public import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
 public import Mathlib.Analysis.Calculus.AddTorsor.Coord
 public import Mathlib.Analysis.Calculus.BumpFunction.Basic
@@ -5916,8 +5919,7 @@ public import Mathlib.Order.Cover
 public import Mathlib.Order.Defs.LinearOrder
 public import Mathlib.Order.Defs.PartialOrder
 public import Mathlib.Order.Defs.Unbundled
-public import Mathlib.Order.DirSupClosed.Basic
-public import Mathlib.Order.DirSupClosed.Finite
+public import Mathlib.Order.DirSupClosed
 public import Mathlib.Order.Directed
 public import Mathlib.Order.DirectedInverseSystem
 public import Mathlib.Order.Disjoint

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Semi
 public import Mathlib.Algebra.Category.Grp.Preadditive
 public import Mathlib.CategoryTheory.Linear.Basic
 public import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
+public import Mathlib.LinearAlgebra.BilinearMap
 
 /-!
 # The category of `R`-modules
@@ -386,6 +387,15 @@ lemma isZero_iff_subsingleton : IsZero M ↔ Subsingleton M where
 lemma isZero_of_iff_subsingleton {M : Type*} [AddCommGroup M] [Module R M] :
     IsZero (of R M) ↔ Subsingleton M := isZero_iff_subsingleton
 
+@[simp]
+lemma ofHom_zero {M N : Type v} [AddCommGroup M] [Module R M]
+    [AddCommGroup N] [Module R N] : ModuleCat.ofHom (0 : M →ₗ[R] N) = 0 := rfl
+
+@[simp]
+lemma ofHom_add {M N : Type v} [AddCommGroup M] [Module R M]
+    [AddCommGroup N] [Module R N] (f g : M →ₗ[R] N) :
+    ModuleCat.ofHom (f + g) = ModuleCat.ofHom f + ModuleCat.ofHom g := rfl
+
 end AddCommGroup
 
 section SMul
@@ -456,6 +466,9 @@ variable {S : Type u} [CommRing S]
 
 instance : Linear S (ModuleCat.{v} S) := ModuleCat.Algebra.instLinear
 
+lemma lsmul_eq_smul_id (M : ModuleCat.{v} S) (s : S) :
+    ModuleCat.ofHom (LinearMap.lsmul S M s) = s • 𝟙 M := rfl
+
 variable {X Y X' Y' : ModuleCat.{v} S}
 
 set_option backward.privateInPublic true in

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

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan
+-/
+
+module
+
+public import Mathlib.Algebra.Category.Grp.Zero
+public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
+public import Mathlib.RingTheory.Ideal.Maps
+
+/-!
+
+# Some basic lemmas for manipulating `Ext` over `ModuleCat`
+
+-/
+
+@[expose] public section
+
+universe v u
+
+open LinearMap CategoryTheory Limits
+
+variable {R : Type u} [CommRing R]
+
+variable {M N : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+
+namespace CategoryTheory.Abelian
+
+variable [Small.{v} R] {M N : ModuleCat.{v} R}
+
+/-- If `r • N = 0`, then `r • 𝟙 M` induces the zero endomorphism on `Ext M N n`. -/
+lemma Ext.postcomp_smul_id_eq_zero_of_mem_annihilator {r : R} (mem_ann : r ∈ Module.annihilator R N)
+    (n : ℕ) : AddCommGrpCat.ofHom ((Ext.mk₀ (r • 𝟙 M)).postcomp N (add_zero n)) = 0 := by
+  ext h
+  have : r • 𝟙 N = 0 := by
+    simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]
+  have smul_eq : r • h = (Ext.mk₀ (r • 𝟙 N)).comp h (zero_add n) := by simp [Ext.mk₀_smul]
+  simp [Ext.mk₀_smul, this, smul_eq]
+
+/-- `r • 𝟙 M` induces a monomorphism in `Ext M N n` if and only if scalar multiplication by `r`
+is faithful on `Ext M N n`. -/
+lemma Ext.postcomp_smul_id_mono_iff (r : R) (i : ℕ) :
+    Mono (AddCommGrpCat.ofHom ((Ext.mk₀ (r • 𝟙 M)).postcomp N (add_zero i))) ↔
+      IsSMulRegular (Ext N M i) r := by
+  simp only [IsSMulRegular, AddCommGrpCat.mono_iff_injective]
+  congr!
+  ext
+  simp [Ext.mk₀_smul]
+
+end CategoryTheory.Abelian

Mathlib/Algebra/Category/Ring/Under/Basic.lean

@@ -80,7 +80,7 @@ def toUnder {A B : Type u} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
 @[simp]
 lemma toUnder_right {A B : Type u} [CommRing A] [CommRing B] [Algebra R A]
     [Algebra R B] (f : A →ₐ[R] B) (a : A) :
-    f.toUnder.right a = f a :=
+    Under.Hom.right f.toUnder a = f a :=
   rfl
 
 @[simp]
@@ -130,7 +130,7 @@ variable [Algebra R S]
 
 variable (R S) in
 /-- The base change functor `A ↦ S ⊗[R] A`. -/
-@[simps! map_right]
+@[simps! obj_right map_right]
 def tensorProd : Under R ⥤ Under S where
   obj A := mkUnder S (S ⊗[R] A)
   map f := Algebra.TensorProduct.map (AlgHom.id S S) (toAlgHom f) |>.toUnder

Mathlib/Algebra/Category/Ring/Under/Property.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Category.Ring.Under.Limits
 public import Mathlib.CategoryTheory.Limits.MorphismProperty
 public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
+public import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 
 /-!
 # Properties of `P.Under ⊤ R` for `R : CommRingCat`
@@ -19,6 +20,8 @@ In this file we translate ring theoretic properties of a property of ring homomo
 
 - `CommRingCat.Under.hasFiniteLimits`: If `P` is stable under finite products and equalizers,
   `P.Under ⊤ R` has finite limits.
+- `RingHom.HasStableEqualizers.preservesFiniteLimits_pushout`: If `P` has stable equalizers,
+  base change along arbitrary morphisms preserve finite limits.
 -/
 
 @[expose] public section
@@ -80,6 +83,18 @@ lemma RingHom.HasFiniteProducts.hasFiniteProducts (hQi : RespectsIso Q) (hQp : H
   have := hQp.createsFiniteProductsForget hQi R
   exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)
 
+lemma RingHom.HasFiniteProducts.preservesFiniteProducts_pushout (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) [(toMorphismProperty Q).IsStableUnderCobaseChange]
+    {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesFiniteProducts (Under.pushout (toMorphismProperty Q) ⊤ f) := by
+  have := hQp.createsFiniteProductsForget hQi R
+  refine ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩
+  have : PreservesLimit K (Under.pushout (toMorphismProperty Q) ⊤ f ⋙
+        Under.forget (toMorphismProperty Q) ⊤ S) := by
+    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
+    infer_instance
+  exact preservesLimit_of_reflects_of_preserves _ (MorphismProperty.Under.forget _ ⊤ S)
+
 /-- If `Q` is stable under equalizers, the inclusion from the subcategory of `Under R` defined
 by `Q` creates equalizers. -/
 @[implicit_reducible]
@@ -117,3 +132,74 @@ lemma Under.hasFiniteLimits (hQi : RingHom.RespectsIso Q)
   hasFiniteLimits_of_hasEqualizers_and_finite_products
 
 end CommRingCat
+
+variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)
+
+open RingHom
+
+variable {P}
+
+lemma CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective
+    {R S : CommRingCat.{u}} [Algebra R S] {A B : Under R} {f g : A ⟶ B} :
+    PreservesLimit (parallelPair f g) (tensorProd R S) ↔
+      Function.Bijective ((toAlgHom f).tensorEqualizer R S (toAlgHom g)) := by
+  let c : Fork f g := Under.equalizerFork f g
+  let hc : IsLimit c := Under.equalizerForkIsLimit f g
+  let ι : R.mkUnder (AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
+    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder
+  let h' := (R.tensorProd S).map ι
+  have w' : h' ≫ (tensorProd R S).map f = h' ≫ (tensorProd R S).map g := by
+    simpa using congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
+  let e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') :=
+    isLimitMapConeForkEquiv (tensorProd R S) (Under.equalizer_comp f g)
+  rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
+    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]
+  have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
+      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
+        Under.homMk (CommRingCat.ofHom (.id _)) := by
+    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
+    rw [Fork.IsLimit.lift_ι]
+    ext : 2
+    dsimp
+    ext x <;> rfl
+  rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
+    ConcreteCategory.isIso_iff_bijective]
+  rfl
+
+lemma RingHom.HasStableEqualizers.preservesLimit_parallelPair_tensorProd
+    (hPse : HasStableEqualizers P) {R S : CommRingCat.{u}} [Algebra R S]
+    {A B : Under R} (f g : A ⟶ B) (hA : P A.hom.hom) (hB : P B.hom.hom) :
+    PreservesLimit (parallelPair f g) (CommRingCat.tensorProd R S) := by
+  rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]
+  exact hPse _ _ hA hB
+
+lemma RingHom.HasStableEqualizers.preservesEqualizers_pushout (hPi : RespectsIso P)
+    (hPe : HasEqualizers P) (hPse : HasStableEqualizers P)
+    [(toMorphismProperty P).IsStableUnderCobaseChange] {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesLimitsOfShape WalkingParallelPair (Under.pushout (toMorphismProperty P) ⊤ f) := by
+  refine ⟨fun {K} ↦ ?_⟩
+  have := hPe.createsLimitsWalkingParallelPair hPi R
+  algebraize [f.hom]
+  have : PreservesLimit (K ⋙ Under.forget (toMorphismProperty P) ⊤ R)
+      (CategoryTheory.Under.pushout f) := by
+    rw [← CommRingCat.ofHom_hom f,
+      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
+      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
+    exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)
+  have : PreservesLimit K (Under.pushout (toMorphismProperty P) ⊤ f ⋙
+        Under.forget (toMorphismProperty P) ⊤ S) := by
+    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
+    infer_instance
+  exact preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)
+
+/-- If `P` is a property of ring homs that is stable under finite products and
+equalizers, and the latter are preserved by arbitrary base change,
+pushout along any ring homomorphism preserves finite limits. -/
+lemma RingHom.HasStableEqualizers.preservesFiniteLimits_pushout (hPi : RingHom.RespectsIso P)
+    (hPp : HasFiniteProducts P) (hPe : HasEqualizers P) (hPse : HasStableEqualizers P)
+    [(toMorphismProperty P).IsStableUnderCobaseChange] {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    PreservesFiniteLimits (Under.pushout (toMorphismProperty P) ⊤ f) :=
+  have := hPp.preservesFiniteProducts_pushout hPi f
+  have := hPse.preservesEqualizers_pushout hPi hPe f
+  have := CommRingCat.Under.hasFiniteLimits hPi hPp hPe
+  preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts _

Mathlib/Algebra/DirectSum/Module.lean

@@ -213,6 +213,14 @@ theorem component.of [DecidableEq ι] (i j : ι) (b : M j) :
     component R ι M i ((lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0 :=
   DFinsupp.single_apply
 
+lemma component_comp_lof [DecidableEq ι] (i j : ι) :
+    component R ι M i ∘ₗ lof R ι M j = if h : j = i then h ▸ .id else 0 := by
+  aesop (add simp component.of)
+
+@[simp]
+lemma component_comp_lof_same [DecidableEq ι] (i : ι) : component R ι M i ∘ₗ lof R ι M i = .id := by
+  simp [component_comp_lof]
+
 section map
 
 variable {R} {N : ι → Type*}

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -337,26 +337,30 @@ theorem mem_normalizer_iff_conj_image_eq {s : Set G} {g : G} :
   refine forall_congr' fun h ↦ ?_
   simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
 
-theorem _root_.AddSubgroup.mem_normalizer_iff_conj_image_eq {G : Type*} [AddGroup G] {s : Set G}
+theorem _root_.AddSubgroup.mem_normalizer_iff_addConj_image_eq {G : Type*} [AddGroup G] {s : Set G}
     {g : G} : g ∈ AddSubgroup.normalizer s ↔ AddAut.conj g '' s = s := by
   simp_rw [AddSubgroup.mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, AddAut.conj_apply]
   refine forall_congr' fun h ↦ ?_
   simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
 
+@[deprecated (since := "2026-05-12")]
+alias _root_.AddSubgroup.mem_normalizer_iff_conj_image_eq :=
+  AddSubgroup.mem_normalizer_iff_addConj_image_eq
+
 theorem normalizer_le_normalizer_closure (s : Set G) : normalizer s ≤ normalizer (closure s) := by
   intro g hg
   have : MulAut.conj g '' (closure s) = closure (MulAut.conj g '' s) :=
-    congr(SetLike.coe $(MulAut.conj g |>.toMonoidHom.map_closure s))
+    congr($(MulAut.conj g |>.toMonoidHom.map_closure s))
   rw [mem_normalizer_iff_conj_image_eq.mp hg] at this
   rwa [mem_normalizer_iff_conj_image_eq]
 
 theorem _root_.AddSubgroup.normalizer_le_normalizer_closure {G : Type*} [AddGroup G] (s : Set G) :
     AddSubgroup.normalizer s ≤ AddSubgroup.normalizer (AddSubgroup.closure s) := by
   intro g hg
   have : AddAut.conj g '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj g '' s) :=
-    congr(SetLike.coe $(AddAut.conj g |>.toAddMonoidHom.map_closure s))
-  rw [AddSubgroup.mem_normalizer_iff_conj_image_eq.mp hg] at this
-  rwa [AddSubgroup.mem_normalizer_iff_conj_image_eq]
+    congr($(AddAut.conj g |>.toAddMonoidHom.map_closure s))
+  rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq.mp hg] at this
+  rwa [AddSubgroup.mem_normalizer_iff_addConj_image_eq]
 
 variable {H}
 
@@ -371,6 +375,39 @@ variable (H) in
 theorem normalizer_eq_top [h : H.Normal] : normalizer (H : Set G) = ⊤ :=
   normalizer_eq_top_iff.mpr h
 
+@[to_additive]
+theorem le_set_normalizer_iff {s : Set G} :
+    H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
+  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk
+
+@[to_additive]
+theorem le_normalizer_iff : H ≤ normalizer K ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
+  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk
+
+theorem le_normalizer_closure_iff {s : Set G} :
+    H ≤ normalizer (closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
+  have : MulAut.conj h '' (closure s) = closure (MulAut.conj h '' s) :=
+    congr($(MulAut.conj h |>.toMonoidHom.map_closure s))
+  rw [mem_normalizer_iff_conj_image_eq, this]
+  apply subset_antisymm <| by simpa using hH h hh
+  rw [SetLike.coe_subset_coe, closure_le, ← this]
+  exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩
+
+theorem _root_.AddSubgroup.le_normalizer_closure_iff {G : Type*} [AddGroup G] {H : AddSubgroup G}
+    {s : Set G} :
+    H ≤ AddSubgroup.normalizer (AddSubgroup.closure s) ↔
+      ∀ h ∈ H, ∀ g ∈ s, h + g + -h ∈ AddSubgroup.closure s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| AddSubgroup.mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
+  have : AddAut.conj h '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj h '' s) :=
+    congr($(AddAut.conj h |>.toAddMonoidHom.map_closure s))
+  rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq, this]
+  apply subset_antisymm <| by simpa using hH h hh
+  rw [SetLike.coe_subset_coe, AddSubgroup.closure_le, ← this]
+  exact fun g hg ↦ ⟨_, hH _ (neg_mem hh) g hg, by simp [add_assoc]⟩
+
 variable {N : Type*} [Group N]
 
 /-- The preimage of the normalizer is contained in the normalizer of the preimage. -/