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

class IsRegularLocalRing (R : Type u_1) [CommRing R] extends IsLocalRing R, IsNoetherian R R : Prop

A Noetherian local ring is said to be regular if its maximal ideal can be generated by dim R elements.

• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one {a b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b
• noetherian (s : Submodule R R) : s.FG
• spanFinrank_maximalIdeal : ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) = ringKrullDim R

theorem isRegularLocalRing_iff (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) = ringKrullDim R

theorem IsRegularLocalRing.of_spanFinrank_maximalIdeal_le (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (le : ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) ≤ ringKrullDim R) : IsRegularLocalRing R

theorem IsRegularLocalRing.of_ringEquiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {R' : Type u_2} [CommRing R'] (e : R ≃+* R') : IsRegularLocalRing R'

theorem IsRegularLocalRing.iff_finrank_cotangentSpace (R : Type u_1) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsRegularLocalRing R ↔ ↑(Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)) = ringKrullDim R

instance IsRegularLocalRing.instOfIsLocalRingOfIsDomainOfIsPrincipalIdealRing (R : Type u_1) [CommRing R] [IsLocalRing R] [IsDomain R] [IsPrincipalIdealRing R] : IsRegularLocalRing R