feat(RingTheory): definition of regular local ring (#28682)

In this PR, we give the definition of regular local ring.
The class `IsRegularLocalRing` is defined as `(maximalIdeal R).spanFinrank = ringKrullDim R`
We also established the lemma `IsRegularLocalRing.iff_finrank_cotangentSpace` proving this definition is equivalent to the cotangent space version.

Author: Thmoas-Guan

Mathlib.lean

@@ -6659,6 +6659,7 @@ public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
 public import Mathlib.RingTheory.Regular.IsSMulRegular
 public import Mathlib.RingTheory.Regular.RegularSequence
+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/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -470,4 +470,11 @@ lemma Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown [IsNoetherianRing S
   simp [hlq, l', ← PrimeSpectrum.asIdeal_le_asIdeal, map_le_iff_le_comap,
     LiesOver.over (p := p) (P := P)]
 
+variable (R) in
+lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] :
+    ringKrullDim R ≤ (IsLocalRing.maximalIdeal R).spanFinrank :=
+  le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm
+    (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (IsLocalRing.maximalIdeal R)
+      Ideal.IsPrime.ne_top'))
+
 end Algebra

Mathlib/RingTheory/RegularLocalRing/Defs.lean

@@ -0,0 +1,79 @@
+/-
+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.Module.SpanRankOperations
+public import Mathlib.RingTheory.DiscreteValuationRing.Basic
+public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem
+public import Mathlib.RingTheory.KrullDimension.Field
+public import Mathlib.RingTheory.KrullDimension.PID
+
+/-!
+# Regular local rings
+
+For a Noetherian local ring `R`, we define `IsRegularLocalRing` as
+`(maximalIdeal R).spanFinrank = ringKrullDim R`. This definition is equivalent to
+the dimension of the cotangent space over the residue field being equal to `ringKrullDim R`,
+(see `IsRegularLocalRing.iff_finrank_cotangentSpace`).
+
+# Main Definition and Results
+
+* `IsRegularLocalRing` : A Noetherian local ring is regular if
+  `(maximalIdeal R).spanFinrank = ringKrullDim R`,
+  i.e. its maximal ideal can be generated by `dim R` elements.
+
+* `IsRegularLocalRing.iff_finrank_cotangentSpace` : the equivalence of `IsRegularLocalRing` and
+  `Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R`
+
+-/
+
+@[expose] public section
+
+open IsLocalRing
+
+/-- A Noetherian local ring is said to be regular if its maximal ideal
+can be generated by `dim R` elements. -/
+@[stacks 00KU]
+class IsRegularLocalRing (R : Type*) [CommRing R] : Prop extends
+    IsLocalRing R, IsNoetherianRing R where
+  spanFinrank_maximalIdeal : (maximalIdeal R).spanFinrank = ringKrullDim R
+
+variable (R : Type*) [CommRing R]
+
+lemma isRegularLocalRing_iff [IsLocalRing R] [IsNoetherianRing R] :
+    IsRegularLocalRing R ↔ (maximalIdeal R).spanFinrank = ringKrullDim R :=
+  ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
+
+namespace IsRegularLocalRing
+
+lemma of_spanFinrank_maximalIdeal_le [IsLocalRing R] [IsNoetherianRing R]
+    (le : (maximalIdeal R).spanFinrank ≤ ringKrullDim R) : IsRegularLocalRing R :=
+  (isRegularLocalRing_iff _).mpr (le_antisymm le (ringKrullDim_le_spanFinrank_maximalIdeal R))
+
+variable {R} in
+lemma of_ringEquiv [IsRegularLocalRing R] {R' : Type*} [CommRing R']
+    (e : R ≃+* R') : IsRegularLocalRing R' := by
+  have := e.isLocalRing
+  have := isNoetherianRing_of_ringEquiv R e
+  rwa [isRegularLocalRing_iff, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
+    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_iff]
+
+lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] :
+    IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by
+  rw [isRegularLocalRing_iff, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]
+
+set_option backward.isDefEq.respectTransparency false in
+instance [IsLocalRing R] [IsDomain R] [IsPrincipalIdealRing R] : IsRegularLocalRing R := by
+  by_cases isf : IsField R
+  · let _ := isf.toField
+    simp [isRegularLocalRing_iff, maximalIdeal_eq_bot]
+  · apply of_spanFinrank_maximalIdeal_le
+    rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩
+    simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) isf,
+      Nat.cast_le_one, ← Set.ncard_singleton x, hx] using
+        Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)
+
+end IsRegularLocalRing