Regular Local Ring

Results named in Tau Ceti's TauCeti.RingTheory.RegularLocalRing modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Jacobian criterion for a hypersurface#

Let f ∈ A and let P be a prime of A ⧸ (f) lying over the prime Q of A, with A_Q a regular local ring. If some derivation D of A maps f outside Q, then the localization of A ⧸ (f) at P is a regular local ring.

Ideal.isRegularLocalRing_localization_of_derivation_notMem.{u_1, u_2} {R : Type u_1} {A : Type u_2}
  [CommRing R] [CommRing A] [Algebra R A] {f : A} (P : Ideal (A ⧸ Ideal.span {f})) [P.IsPrime]
  [IsRegularLocalRing (Localization.AtPrime (Ideal.comap (Ideal.Quotient.mk (Ideal.span {f})) P))]
  {D : Derivation R A A} (hD : D f ∉ Ideal.comap (Ideal.Quotient.mk (Ideal.span {f})) P) :
  IsRegularLocalRing (Localization.AtPrime P)

Lean

Formalized in Tau Ceti as Ideal.isRegularLocalRing_localization_of_derivation_notMem.

Sources

• Tau Ceti documentation: Ideal.isRegularLocalRing_localization_of_derivation_notMem
• Source of Ideal.isRegularLocalRing_localization_of_derivation_notMem in TauCeti/RingTheory/RegularLocalRing/Hypersurface.lean

LeanIdeal.isRegularLocalRing_localization_of_derivation_notMem

Used by 1

Used byThe genus of a smooth projective plane curve (Fulton, *Algebraic Curves*, Section 8.3)

TheoremKunz's theorem#

The Frobenius endomorphism of a regular ring of exponential characteristic p is flat. Stacks, Lemma 51.17.6 (0EC0), the implication from regularity to flatness.

TauCeti.IsRegularRing.flat_frobenius.{u_1} {R : Type u_1} [CommRing R] (p : ℕ) [ExpChar R p]
  [IsRegularRing R] : (frobenius R p).Flat

Lean

Formalized in Tau Ceti as TauCeti.IsRegularRing.flat_frobenius.

Sources

• Tau Ceti documentation: TauCeti.IsRegularRing.flat_frobenius
• Source of TauCeti.IsRegularRing.flat_frobenius in TauCeti/RingTheory/RegularLocalRing/Frobenius.lean

LeanTauCeti.IsRegularRing.flat_frobenius

Uses 1

Proof usesA regular local ring is Cohen–Macaulay

TheoremSerre's theorem (TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE)#

A Noetherian local ring whose residue field has finite projective dimension is a regular local ring. Its dimension is then that projective dimension, by TauCeti.IsRegularLocalRing.projectiveDimension_quotient_maximalIdeal_eq_ringKrullDim.

TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE.{v, u} {R : Type u} [CommRing R]
  [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLE (↧(Shrink.{v, u} (R ⧸ IsLocalRing.maximalIdeal R))) n] :
  IsRegularLocalRing R

Lean

Formalized in Tau Ceti as TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE.

Other forms

Serre's theorem, global dimension form. Formalized in Tau Ceti as TauCeti.IsRegularLocalRing.of_globalDimension_lt_top.

TauCeti.IsRegularLocalRing.of_globalDimension_lt_top.{v, u} {R : Type u} [CommRing R]
  [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (h : TauCeti.globalDimension R < ⊤) :
  IsRegularLocalRing R

Sources

• Tau Ceti documentation: TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE
• Source of TauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE in TauCeti/RingTheory/RegularLocalRing/ProjectiveDimension.lean

LeanTauCeti.IsRegularLocalRing.of_hasProjectiveDimensionLE · TauCeti.IsRegularLocalRing.of_globalDimension_lt_top

Used by 1

Used byThe Chevalley–Shephard–Todd theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.