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

Mathlib.lean

@@ -6637,6 +6637,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

@@ -473,4 +473,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,77 @@
+/-
+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
+
+/-!
+# Define Regular Local Ring
+
+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
+
+variable (R : Type*) [CommRing R]
+
+/-- A Noetherian local ring is said to be regular if its maximal ideal
+can be generated by `dim R` elements. -/
+class IsRegularLocalRing : Prop extends IsLocalRing R, IsNoetherianRing R where
+  spanFinrank_maximalIdeal : (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⟩⟩
+
+namespace IsRegularLocalRing
+
+lemma of_spanFinrank_maximalIdeal_le [IsLocalRing R] [IsNoetherianRing R]
+    (le : (maximalIdeal R).spanFinrank ≤ ringKrullDim R) : IsRegularLocalRing R :=
+  (isRegularLocalRing_def _).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
+  let _ := e.isLocalRing
+  let _ := isNoetherianRing_of_ringEquiv R e
+  rwa [isRegularLocalRing_def, ← ringKrullDim_eq_of_ringEquiv e, ← map_ringEquiv_maximalIdeal e,
+    Ideal.spanFinrank_map_eq_of_ringEquiv, ← isRegularLocalRing_def]
+
+lemma iff_finrank_cotangentSpace [IsLocalRing R] [IsNoetherianRing R] :
+    IsRegularLocalRing R ↔ Module.finrank (ResidueField R) (CotangentSpace R) = ringKrullDim R := by
+  rw [isRegularLocalRing_def, spanFinrank_maximalIdeal_eq_finrank_cotangentSpace]
+
+instance {k : Type*} [Field k] : IsRegularLocalRing k := by
+  simp [isRegularLocalRing_def, maximalIdeal_eq_bot]
+
+set_option backward.isDefEq.respectTransparency false in
+instance [IsDomain R] [IsDiscreteValuationRing R] : IsRegularLocalRing R := by
+  apply of_spanFinrank_maximalIdeal_le
+  rcases IsPrincipalIdealRing.principal (maximalIdeal R) with ⟨x, hx⟩
+  simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) (IsDiscreteValuationRing.not_isField R),
+    Nat.cast_le_one, ← Set.ncard_singleton x, hx] using
+    Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)
+
+end IsRegularLocalRing