[Merged by Bors] - feat(RingTheory): definition of regular local ring

Mathlib.lean

@@ -5642,6 +5642,7 @@ import Mathlib.RingTheory.Regular.Category
 import Mathlib.RingTheory.Regular.Depth
 import Mathlib.RingTheory.Regular.IsSMulRegular
 import Mathlib.RingTheory.Regular.RegularSequence
+import Mathlib.RingTheory.RegularLocalRing
 import Mathlib.RingTheory.RingHom.Etale
 import Mathlib.RingTheory.RingHom.FaithfullyFlat
 import Mathlib.RingTheory.RingHom.Finite

Mathlib/RingTheory/RegularLocalRing.lean

@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2025 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan
+-/
+import Mathlib.RingTheory.Ideal.Cotangent
+import Mathlib.RingTheory.Ideal.KrullsHeightTheorem
+/-!
+# Define Regular Local Ring
+
+For a noetherian local ring `R`, we define `IsRegularLocalRing` as
+`(maximalIdeal R).spanFinrank = ringKrullDim R`
+
+# Main Definition and Results
+
+* `IsRegularLocalRing` : A noetherian local ring of dimesnion `d` `IsRegularLocalRing` if
+  `(maximalIdeal R).spanFinrank = ringKrullDim R`,
+  i.e. its maximal ideal can be generated by `d` elements.
+
+* `isRegularLocalRing_iff` : the equivalence of `IsRegularLocalRing` and
+  `Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R`
+
+-/
+
+open IsLocalRing
+
+variable (R : Type*) [CommRing R]
+
+/-- A noetherian local ring of dimesnion `d` is said to be regular if its maximal ideal
+can be generated by `d` elements. -/
+class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where
+  reg : (maximalIdeal R).spanFinrank = ringKrullDim R
+
+lemma isRegularLocalRing_def [IsLocalRing R] [IsNoetherianRing R] :
+    IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R :=
+  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
+
+lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] :
+    ringKrullDim R ≤ (maximalIdeal R).spanFinrank :=
+  le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm
+    (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (maximalIdeal R) Ideal.IsPrime.ne_top'))
+
+namespace IsRegularLocalRing
+
+lemma of_span_eq [IsLocalRing R] [IsNoetherianRing R] (S : Set R) (fin : S.Finite)
+    (span : Ideal.span S = maximalIdeal R) (card : S.ncard ≤ ringKrullDim R) :
+    IsRegularLocalRing R := by
+  apply (isRegularLocalRing_def _).mpr (le_antisymm _ (ringKrullDim_le_spanFinrank_maximalIdeal R))
+  apply le_trans _ card
+  rw [← span, ← Ideal.submodule_span_eq]
+  simpa using Submodule.spanFinrank_span_le_ncard_of_finite fin
+
+variable {R} in
+lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R']
+    (e : R ≃+* R') : IsRegularLocalRing R' := by
+  let _ := e.isLocalRing
+  let _ := isNoetherianRing_of_ringEquiv R e
+  have fg : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _
+  apply of_span_eq R' (e '' (maximalIdeal R).generators)
+    ((Submodule.FG.finite_generators fg).image _)
+  · simp only [← Ideal.map_span]
+    rw [← Ideal.submodule_span_eq, Submodule.span_generators (maximalIdeal R), ← Ideal.comap_symm]
+    exact ((local_hom_TFAE e.symm.toRingHom).out 0 4).mp (e.symm.surjective.isLocalHom _)
+  · simpa [← ringKrullDim_eq_of_ringEquiv e, ← IsRegularLocalRing.reg,
+      ← Submodule.FG.generators_ncard fg] using
+      Set.ncard_image_le (Submodule.FG.finite_generators fg)
+
+end IsRegularLocalRing
+
+lemma span_eq_top_iff [IsLocalRing R] (S : Set (maximalIdeal R)) :
+    Submodule.span R S = ⊤ ↔ Submodule.span R ((Submodule.subtype (maximalIdeal R)) '' S) =
+    maximalIdeal R := by
+  rw [← Submodule.map_span]
+  refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
+  rw [← Submodule.comap_map_eq_of_injective (maximalIdeal R).injective_subtype
+    (Submodule.span R S), h, Submodule.comap_subtype_self]
+
+open Set in
+lemma spanFinrank_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] :
+    (maximalIdeal R).spanFinrank = Module.finrank (ResidueField R) (CotangentSpace R) := by
+  let fg : Module.Finite (ResidueField R) (CotangentSpace R) := inferInstance
+  let fg' : (maximalIdeal R).FG := (isNoetherianRing_iff_ideal_fg R).mp inferInstance _
+  have : Submodule.spanFinrank (⊤ : Submodule (ResidueField R) (CotangentSpace R)) =
+    Module.rank (ResidueField R) (CotangentSpace R) := by
+    rw [← Submodule.fg_iff_spanRank_eq_spanFinrank.mpr fg.1, Submodule.rank_eq_spanRank_of_free]
+  simp only [← Module.finrank_eq_rank, Nat.cast_inj] at this
+  rw [← this]
+  apply le_antisymm
+  · have span : Submodule.span R
+      ((⊤ : Submodule (ResidueField R) (CotangentSpace R)).generators.image Quotient.out) = ⊤ := by
+      apply IsLocalRing.CotangentSpace.span_image_eq_top_iff.mp
+      convert Submodule.span_generators (⊤ : Submodule (ResidueField R) (CotangentSpace R))
+      have : ⇑(maximalIdeal R).toCotangent ∘ Quotient.out = id := by
+        ext
+        exact Submodule.Quotient.mk_out _
+      rw [← Set.image_comp, this, image_id]
+    rw [span_eq_top_iff, ← Set.image_comp] at span
+    rw [← Submodule.FG.generators_ncard fg.1, ← congrArg Submodule.spanFinrank span]
+    apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite
+      (Finite.image _ fg.1.finite_generators)) (Set.ncard_image_le fg.1.finite_generators)
+  · let G := ({x | ↑x ∈ (maximalIdeal R).generators} : Set (maximalIdeal R))
+    have : Submodule.span R G = ⊤ := by
+      simp only [span_eq_top_iff, Submodule.subtype_apply, Ideal.submodule_span_eq, G]
+      convert (maximalIdeal R).span_generators
+      ext
+      simpa using fun a ↦ Submodule.FG.generators_mem (maximalIdeal R) a
+    have fin : G.Finite := Set.Finite.of_injOn (by simp [MapsTo, G]) injOn_subtype_val
+        (Submodule.FG.finite_generators fg')
+    rw [← IsLocalRing.CotangentSpace.span_image_eq_top_iff.mpr this,
+      ← Submodule.FG.generators_ncard fg']
+    apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (Finite.image _ fin))
+    exact le_trans (Set.ncard_image_le fin) (Set.ncard_le_ncard_of_injOn Subtype.val (by simp [G])
+      injOn_subtype_val (Submodule.FG.finite_generators fg'))
+
+lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] :
+    IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by
+  rw [isRegularLocalRing_def, spanFinrank_maximalIdeal]