feat(RingTheory): regular of finite global dimension

Mathlib.lean

@@ -149,6 +149,7 @@ public import Mathlib.Algebra.Category.ModuleCat.AB
 public import Mathlib.Algebra.Category.ModuleCat.Abelian
 public import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 public import Mathlib.Algebra.Category.ModuleCat.Algebra
+public import Mathlib.Algebra.Category.ModuleCat.Baer
 public import Mathlib.Algebra.Category.ModuleCat.Basic
 public import Mathlib.Algebra.Category.ModuleCat.Biproducts
 public import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
@@ -6139,6 +6140,7 @@ public import Mathlib.RingTheory.FractionalIdeal.Operations
 public import Mathlib.RingTheory.FreeCommRing
 public import Mathlib.RingTheory.FreeRing
 public import Mathlib.RingTheory.Frobenius
+public import Mathlib.RingTheory.GlobalDimension
 public import Mathlib.RingTheory.GradedAlgebra.Basic
 public import Mathlib.RingTheory.GradedAlgebra.FiniteType
 public import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
@@ -6450,11 +6452,16 @@ public import Mathlib.RingTheory.QuasiFinite.Weakly
 public import Mathlib.RingTheory.QuotSMulTop
 public import Mathlib.RingTheory.Radical
 public import Mathlib.RingTheory.ReesAlgebra
+public import Mathlib.RingTheory.Regular.AuslanderBuchsbaum
 public import Mathlib.RingTheory.Regular.Category
 public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
 public import Mathlib.RingTheory.Regular.IsSMulRegular
+public import Mathlib.RingTheory.Regular.Ischebeck
 public import Mathlib.RingTheory.Regular.RegularSequence
+public import Mathlib.RingTheory.RegularLocalRing.AuslanderBuchsbaumSerre
+public import Mathlib.RingTheory.RegularLocalRing.Basic
+public import Mathlib.RingTheory.RegularLocalRing.Defs
 public import Mathlib.RingTheory.RingHom.Bijective
 public import Mathlib.RingTheory.RingHom.EssFiniteType
 public import Mathlib.RingTheory.RingHom.Etale

Mathlib/Algebra/Category/ModuleCat/Baer.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2025 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.EnoughInjectives
+public import Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
+public import Mathlib.Algebra.Category.ModuleCat.Projective
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
+public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
+public import Mathlib.CategoryTheory.Abelian.Injective.Resolution
+public import Mathlib.RingTheory.Ideal.Quotient.Operations
+
+/-!
+# Category Language Baer Criterion
+-/
+
+@[expose] public section
+
+universe u u' v v'
+
+variable {R : Type u} [CommRing R]
+
+open CategoryTheory Abelian
+
+section
+
+set_option backward.isDefEq.respectTransparency false in
+lemma ext_quotient_one_subsingleton_iff [Small.{v} R] (M : ModuleCat.{v} R) (I : Ideal R) :
+    Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1) ↔
+    ∀ g : I →ₗ[R] M, ∃ g' : R →ₗ[R] M, ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩ := by
+  let Sf := (Shrink.linearEquiv.{v} R R).symm.toLinearMap.comp
+    (I.subtype.comp (Shrink.linearEquiv.{v} R I).toLinearMap)
+  let Sg := (Shrink.linearEquiv.{v} R (R ⧸ I)).symm.toLinearMap.comp
+    ((Ideal.Quotient.mkₐ R I).toLinearMap.comp (Shrink.linearEquiv.{v} R R).toLinearMap)
+  have exac : Function.Exact Sf Sg := by
+    intro x
+    simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, AlgHom.coe_toLinearMap,
+      Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, EmbeddingLike.map_eq_zero_iff,
+      Submodule.coe_subtype, Set.mem_range, Ideal.Quotient.eq_zero_iff_mem, Sg, Sf]
+    refine ⟨fun h ↦ ⟨(equivShrink I) ⟨_, h⟩, by simp⟩, fun ⟨y, hy⟩ ↦ by simp [← hy]⟩
+  have inj : Function.Injective Sf := by simpa [Sf] using (Shrink.linearEquiv R I).injective
+  have surj : Function.Surjective Sg := by simpa [Sg] using Ideal.Quotient.mk_surjective
+  let S : ShortComplex (ModuleCat.{v} R) := {
+    f := ModuleCat.ofHom Sf
+    g := ModuleCat.ofHom Sg
+    zero := by
+      ext x
+      simp [exac.apply_apply_eq_zero] }
+  have S_exact : S.ShortExact := {
+    exact := (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mpr exac
+    mono_f := (ModuleCat.mono_iff_injective _).mpr inj
+    epi_g := (ModuleCat.epi_iff_surjective _).mpr surj }
+  have : Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1) ↔
+    Function.Surjective ((Ext.mk₀ S.f).precomp M (add_zero 0)) := by
+    apply Iff.trans _ ((Ext.contravariant_sequence_exact₁' S_exact M 0 1 rfl).epi_f_iff.symm.trans
+      (AddCommGrpCat.epi_iff_surjective _))
+    refine ⟨fun h ↦ ((@AddCommGrpCat.isZero_of_subsingleton _ h).eq_zero_of_tgt _), fun h ↦ ?_⟩
+    exact AddCommGrpCat.subsingleton_of_isZero ((Ext.contravariant_sequence_exact₃' S_exact M 0 1
+      rfl).isZero_X₂ h ((@AddCommGrpCat.isZero_of_subsingleton _
+      (Ext.subsingleton_of_projective S.X₂ M 0)).eq_zero_of_tgt _))
+  apply this.trans ⟨fun h ↦ fun g ↦ ?_, fun h ↦ fun e ↦ ?_⟩
+  · let f := g.comp (Shrink.linearEquiv R I).toLinearMap
+    rcases h (Ext.mk₀ (ModuleCat.ofHom f)) with ⟨f', hf'⟩
+    rw [Ext.bilinearComp_apply_apply, ← Ext.mk₀_addEquiv₀_apply f', Ext.mk₀_comp_mk₀] at hf'
+    have eqcomp := congrArg ModuleCat.Hom.hom ((Ext.mk₀_bijective _ _).1 hf')
+    simp only [← LinearMap.comp_assoc, ModuleCat.hom_comp, ModuleCat.hom_ofHom,
+      LinearEquiv.eq_comp_toLinearMap_iff, S, Sf, f] at eqcomp
+    use (ModuleCat.Hom.hom (Ext.addEquiv₀ f')).comp (Shrink.linearEquiv R R).symm.toLinearMap
+    intro x hx
+    simp only [LinearMap.coe_comp, Function.comp_apply, ← eqcomp, LinearEquiv.coe_coe,
+      Submodule.coe_subtype]
+    rfl
+  · rcases h ((Ext.addEquiv₀ e).hom.comp (Shrink.linearEquiv R I).symm.toLinearMap) with ⟨g', hg'⟩
+    use Ext.mk₀ (ModuleCat.ofHom (g'.comp (Shrink.linearEquiv R R).toLinearMap))
+    rw [Ext.bilinearComp_apply_apply, Ext.mk₀_comp_mk₀, ← Ext.mk₀_addEquiv₀_apply e]
+    congr
+    ext x
+    have eq : (Shrink.linearEquiv R R) (Sf x) = ((Shrink.linearEquiv R I) x).1 :=
+      (Shrink.linearEquiv R R).apply_symm_apply _
+    simp only [ModuleCat.hom_comp, ModuleCat.hom_ofHom, LinearMap.coe_comp, LinearEquiv.coe_coe,
+      Function.comp_apply, S, eq, hg' _ ((Shrink.linearEquiv R I) x).2]
+    exact congrArg _ ((Shrink.linearEquiv R I).symm_apply_apply _)
+
+lemma injective_of_subsingleton_ext_quotient_one [Small.{v} R] (M : ModuleCat.{v} R)
+    (h : ∀ (I : Ideal R), Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M 1)) :
+    Injective M := by
+  rw [← Module.injective_iff_injective_object, ← Module.Baer.iff_injective]
+  exact fun I ↦ (ext_quotient_one_subsingleton_iff M I).mp (h I)
+
+open Limits in
+lemma ext_subsingleton_of_quotients' [Small.{v} R] (M : ModuleCat.{v} R) (n : ℕ)
+    (h : ∀ I : Ideal R, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M (n + 1))) :
+    ∀ N : ModuleCat.{v} R, Subsingleton (Ext N M (n + 1)) := by
+  induction n generalizing M
+  · have : Injective M := injective_of_subsingleton_ext_quotient_one M h
+    intro N
+    exact subsingleton_of_forall_eq 0 (fun e ↦ Ext.eq_zero_of_injective e)
+  · rename_i n ih
+    let ei : EnoughInjectives (ModuleCat R) := inferInstance
+    rcases ei.1 M with ⟨ip⟩
+    let S := ip.shortComplex
+    have (N : ModuleCat R) : Subsingleton (Ext N M (n + 2)) ↔
+      Subsingleton (Ext N (cokernel ip.3) (n + 1)) := by
+      let _ := Ext.subsingleton_of_injective N S.X₂
+      have := (Ext.covariantSequence_exact N ip.shortExact_shortComplex (n + 1) (n + 2)
+        rfl).isIso_map' 1 (by decide) ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
+        ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt  _)
+      exact (@asIso _ _ _ _ _ this).addCommGroupIsoToAddEquiv.subsingleton_congr.symm
+    simp only [this] at h ⊢
+    exact ih (cokernel ip.3) h
+
+lemma ext_subsingleton_of_quotients [Small.{v} R] (M : ModuleCat.{v} R) (n : ℕ)
+    (h : ∀ I : Ideal R, Subsingleton (Ext (ModuleCat.of R (Shrink.{v} (R ⧸ I))) M n)) :
+    ∀ N : ModuleCat.{v} R, Subsingleton (Ext N M n) := by
+  match n with
+  | 0 =>
+    let e₀ := (Shrink.linearEquiv R (R ⧸ (⊥ : Ideal R))).trans
+      (AlgEquiv.quotientBot R R).toLinearEquiv
+    have := (Ext.homEquiv₀.subsingleton_congr.mp (h ⊥))
+    rw [ModuleCat.homAddEquiv.subsingleton_congr,
+      ((e₀.congrLeft M R).trans (LinearMap.ringLmapEquivSelf R R M)).subsingleton_congr,
+      ← ModuleCat.isZero_iff_subsingleton] at this
+    intro N
+    rw [Ext.homEquiv₀.subsingleton_congr]
+    exact subsingleton_of_forall_eq 0 (fun y ↦ Limits.IsZero.eq_zero_of_tgt this y)
+  | n + 1 => exact ext_subsingleton_of_quotients' M n  h
+
+end

Mathlib/Algebra/Module/SpanRank.lean

@@ -6,6 +6,7 @@ Authors: Wanyi He, Jiedong Jiang, Xuchun Li, Christian Merten, Jingting Wang, An
 module
 
 public import Mathlib.Data.ENat.Lattice
+public import Mathlib.LinearAlgebra.Dimension.Free
 public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 public import Mathlib.RingTheory.Finiteness.Ideal
 
@@ -128,6 +129,9 @@ lemma fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFi
   rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]
   exact cast_toNat_eq_iff_lt_aleph0
 
+lemma FG.spanRank_eq_spanFinrank {p : Submodule R M} (fg : p.FG) : p.spanRank = p.spanFinrank :=
+  fg_iff_spanRank_eq_spanFinrank.mpr fg
+
 lemma spanRank_span_le_card (s : Set M) : (Submodule.span R s).spanRank ≤ #s := by
   rw [spanRank]
   let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩
@@ -363,6 +367,17 @@ theorem Submodule.rank_eq_spanRank_of_free [Module.Free R M] [StrongRankConditio
   rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
     Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]
 
+lemma Module.finrank_eq_spanFinrank_of_free [StrongRankCondition R]
+    (M : Type*) [AddCommGroup M] [Module R M] [Module.Free R M] :
+    Module.finrank R M = (⊤ : Submodule R M).spanFinrank := by
+  by_cases fin : Module.Finite R M
+  · have : Submodule.spanFinrank (⊤ : Submodule R M) = Module.rank R M := by
+      rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fin.1,
+        Submodule.rank_eq_spanRank_of_free]
+    simpa only [← Module.finrank_eq_rank, Nat.cast_inj] using this.symm
+  · have fin' : ¬ (⊤ : Submodule R M).FG := Not.intro (fun h ↦ fin ⟨h⟩)
+    rw [Module.finrank_of_not_finite fin, Submodule.spanFinrank_of_not_fg fin']
+
 theorem Submodule.rank_le_spanRank [StrongRankCondition R] :
     Module.rank R M ≤ (⊤ : Submodule R M).spanRank := by
   rw [Module.rank, Submodule.spanRank]

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -674,6 +674,10 @@ def submodule_torsionBy_orderIso (a : R) :
     left_inv := by intro; ext; simp [restrictScalarsEmbedding]
     right_inv := by intro; ext; simp [restrictScalarsEmbedding] }
 
+instance (M : Type*) [AddCommGroup M] [Module R M] [Module.Finite R M] (I : Ideal R) :
+    Module.Finite (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
+  Module.Finite.of_restrictScalars_finite R _ _
+
 end Submodule
 
 end NeedsGroup

Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

@@ -118,14 +118,30 @@ theorem add_eq_coe :
 lemma add_coe_eq_top_iff : x + b = ⊤ ↔ x = ⊤ := by simp
 lemma coe_add_eq_top_iff : a + y = ⊤ ↔ y = ⊤ := by simp
 
+lemma _root_.IsAddLeftRegular.withTop (ha : IsAddLeftRegular a) :
+    IsAddLeftRegular (a : WithTop α) := by
+  rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]
+
+lemma _root_.IsAddRightRegular.withTop (ha : IsAddRightRegular a) :
+    IsAddRightRegular (a : WithTop α) := by
+  rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]
+
+lemma _root_.AddLECancellable.withTop [LE α] (ha : AddLECancellable a) :
+    AddLECancellable (a : WithTop α) := by
+  rintro (_ | b) (_ | c)
+  · simp [none_eq_top]
+  · simp [none_eq_top]
+  · simp [some_eq_coe, ← coe_add, none_eq_top]
+  · simpa [none_eq_top, some_eq_coe, ← coe_add] using fun a ↦ ha a
+
 lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊤) : x + z = y + z ↔ x = y := by
-  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]
+  lift z to α using hz; exact (IsAddRightRegular.all _).withTop.eq_iff
 
 lemma add_right_cancel [IsRightCancelAdd α] (hz : z ≠ ⊤) (h : x + z = y + z) : x = y :=
   (WithTop.add_right_inj hz).1 h
 
 lemma add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊤) : x + y = x + z ↔ y = z := by
-  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]
+  lift x to α using hx; exact (IsAddLeftRegular.all _).withTop.eq_iff
 
 lemma add_left_cancel [IsLeftCancelAdd α] (hx : x ≠ ⊤) (h : x + y = x + z) : y = z :=
   (WithTop.add_left_inj hx).1 h
@@ -464,6 +480,22 @@ theorem add_eq_coe :
 lemma add_coe_eq_bot_iff : x + b = ⊥ ↔ x = ⊥ := by simp
 lemma coe_add_eq_bot_iff : a + y = ⊥ ↔ y = ⊥ := by simp
 
+lemma _root_.IsAddLeftRegular.withBot (ha : IsAddLeftRegular a) :
+    IsAddLeftRegular (a : WithBot α) := by
+  rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _
+
+lemma _root_.IsAddRightRegular.withBot (ha : IsAddRightRegular a) :
+    IsAddRightRegular (a : WithBot α) := by
+  rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]; simpa using @ha _ _
+
+lemma _root_.AddLECancellable.withBot [LE α] (ha : AddLECancellable a) :
+    AddLECancellable (a : WithBot α) := by
+  rintro (_ | b) (_ | c)
+  · simp [none_eq_bot]
+  · simp [none_eq_bot]
+  · simp [some_eq_coe, ← coe_add, none_eq_bot]
+  · simpa [none_eq_bot, some_eq_coe, ← coe_add] using fun a ↦ ha a
+
 lemma add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊥) : x + z = y + z ↔ x = y := by
   lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]
 
@@ -674,12 +706,4 @@ protected def _root_.AddMonoidHom.withBotMap {M N : Type*} [AddZeroClass M] [Add
     (f : M →+ N) : WithBot M →+ WithBot N :=
   { ZeroHom.withBotMap f.toZeroHom, AddHom.withBotMap f.toAddHom with toFun := WithBot.map f }
 
--- instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithBot α) :=
---   { WithBot.partialOrder, WithBot.addCommMonoid with
---     add_le_add_left := fun _ _ h c => add_le_add_left h c }
---
--- instance linearOrderedAddCommMonoid [LinearOrderedAddCommMonoid α] :
---     LinearOrderedAddCommMonoid (WithBot α) :=
---   { WithBot.linearOrder, WithBot.orderedAddCommMonoid with }
-
 end WithBot

Mathlib/Data/ENat/Basic.lean

@@ -611,3 +611,27 @@ lemma WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} : n + 1 ≤ m ↔ n
   · simp
   · rw [WithBot.coe_le_coe, ENat.coe_add, ENat.coe_one, ENat.add_one_le_iff (ENat.coe_ne_top n),
       ← WithBot.coe_lt_coe, WithBot.coe_natCast]
+
+lemma WithBot.add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} : a + c = b + c ↔ a = b :=
+  (IsAddRightRegular.all c).withTop.withBot.eq_iff
+
+lemma WithBot.add_one_cancel {a b : WithBot ℕ∞} : a + 1 = b + 1 ↔ a = b :=
+  (IsAddRightRegular.all 1).withTop.withBot.eq_iff
+
+lemma WithBot.natCast_add_cancel {a b : WithBot ℕ∞} {c : ℕ} : c + a = c + b ↔ a = b :=
+  (IsAddLeftRegular.all c).withTop.withBot.eq_iff
+
+lemma WithBot.one_add_cancel {a b : WithBot ℕ∞} : 1 + a = 1 + b ↔ a = b :=
+  (IsAddLeftRegular.all 1).withTop.withBot.eq_iff
+
+lemma WithBot.add_le_add_natCast_right_iff {a b : WithBot ℕ∞} {c : ℕ} : a + c ≤ b + c ↔ a ≤ b :=
+  (Contravariant.AddLECancellable (a := c)).withTop.withBot.add_le_add_iff_right
+
+lemma WithBot.add_le_add_one_right_iff {a b : WithBot ℕ∞} : a + 1 ≤ b + 1 ↔ a ≤ b :=
+  WithBot.add_le_add_natCast_right_iff
+
+lemma WithBot.add_le_add_natCast_left_iff {a b : WithBot ℕ∞} {c : ℕ} : c + a ≤ c + b ↔ a ≤ b := by
+  rw [add_comm _ a, add_comm _ b, WithBot.add_le_add_natCast_right_iff]
+
+lemma WithBot.add_le_add_one_left_iff {a b : WithBot ℕ∞} : 1 + a ≤ 1 + b ↔ a ≤ b :=
+  WithBot.add_le_add_natCast_left_iff

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -875,3 +875,8 @@ theorem coord_apply_smul (y : Submodule.span R ({x} : Set M)) : coord R M x h y
   Subtype.ext_iff.1 <| (toSpanNonzeroSingleton R M x h).apply_symm_apply _
 
 end LinearEquiv
+
+lemma Submodule.span_val_image_eq_iff {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
+    (p : Submodule R M) (s : Set p) :
+    Submodule.span R (Subtype.val '' s) = p ↔ Submodule.span R s = ⊤ := by
+  simp [← (Submodule.map_injective_of_injective p.injective_subtype).eq_iff, Submodule.map_span]