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).

For the next section, we define regular rings as Noetherian rings whose localization at every prime are regular local rings. (Note that a regular local ring is a regular ring, but this is not immediate under this definition).

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

• IsRegularRing : A noetherian ring is regular if its localization at any prime IsRegularLocalRing.

TODO

Show that regular local rings are regular under this definition. This follows from localizations of regular local rings being regular (@Thmoas-Guan).

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

class IsRegularRing (R : Type u_2) [CommRing R] extends IsNoetherian R R : Prop

A noetherian ring is regular if its localization at any prime IsRegularLocalRing.

• noetherian (s : Submodule R R) : s.FG
• isRegularLocalRing_localization (p : Ideal R) [p.IsPrime] : IsRegularLocalRing (Localization.AtPrime p)

theorem isRegularRing_iff {R : Type u_1} [CommRing R] [IsNoetherianRing R] : IsRegularRing R ↔ ∀ (p : Ideal R) [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)

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

theorem IsRegularLocalRing.of_isRegularRing_of_isLocalRing (R : Type u_1) [CommRing R] [IsLocalRing R] [IsRegularRing R] : IsRegularLocalRing R

@[instance 100]

instance instIsRegularRingOfIsDedekindDomain (R : Type u_1) [CommRing R] [IsDedekindDomain R] : IsRegularRing R