Regular local rings

TheoremQuotient of a regular local ring by a regular parameter is regular#✓fully proved

Quotienting a regular local ring by a parameter outside the square of the maximal ideal and outside every minimal prime stays regular, with the embedding dimension dropping by exactly one.

theorem IsRegularLocalRing.quotient_span_singleton_of_notMem_sq_of_forall_minimalPrimes_notMem
    (R : Type u) [CommRing R] [IsRegularLocalRing R] {x : R}
    (hx : x ∈ maximalIdeal R) (hx2 : x ∉ maximalIdeal R ^ 2)
    (hxmin : ∀ p ∈ minimalPrimes R, x ∉ p) [IsLocalRing (R ⧸ Ideal.span {x})] :
    IsRegularLocalRing (R ⧸ Ideal.span {x}) ∧
      (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1 =
        (maximalIdeal R).spanFinrank

Used by 2

Used byRegular local rings are domains · Regular local rings of dimension at most two are UFDs

• Power series over a regular local ring
• Regular local rings are domains

TheoremUnique factorization from a principal ideal ring quotient#✓fully proved

A Noetherian local domain is a unique factorization monoid when quotienting by a principal prime ideal gives a principal ideal ring.

theorem IsLocalRing.uniqueFactorizationMonoid_of_isPrincipalIdealRing_quotient
    {A : Type*} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsLocalRing A] (t : A)
    [IsDomain (A ⧸ Ideal.span {t})] [IsPrincipalIdealRing (A ⧸ Ideal.span {t})] :
    UniqueFactorizationMonoid A

Used by 1

Used byRegular local rings of dimension at most two are UFDs

TheoremMultivariable power series over a regular local ring are regular local#✓fully proved

Multivariable power series over a regular local ring form a regular local ring. The discrete-valuation-ring case follows by typeclass inference, since a DVR is a regular local ring.

theorem IsRegularLocalRing.mvPowerSeries_fin (𝓞 : Type*) [CommRing 𝓞]
    [IsRegularLocalRing 𝓞] (n : ℕ) : IsRegularLocalRing (MvPowerSeries (Fin n) 𝓞)

Uses 1

Proof usesPower series over a regular local ring are regular local

TheoremRegular local rings of dimension at most one are normal domains#✓fully proved

A regular local ring of Krull dimension at most one is a domain and integrally closed.

theorem IsRegularLocalRing.isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one
    (A : Type*) [CommRing A] [IsRegularLocalRing A] (h : ringKrullDim A ≤ 1) :
    IsDomain A ∧ IsIntegrallyClosed A

TheoremAdjoining a root of an Eisenstein-like polynomial preserves regularity#✓fully proved

Adjoining a root of a monic polynomial whose non-leading coefficients lie in the maximal ideal and whose constant coefficient lies outside the square of the maximal ideal preserves regularity and Krull dimension.

theorem IsRegularLocalRing.adjoinRoot_of_monic_of_coeff_mem_maximalIdeal_of_coeff_zero_not_mem_sq
    (S : Type*) [CommRing S] [IsRegularLocalRing S]
    (g : S[X]) (hg : g.Monic) (hn : 1 ≤ g.natDegree)
    (hcoeff : ∀ i < g.natDegree, g.coeff i ∈ maximalIdeal S)
    (h0 : g.coeff 0 ∉ maximalIdeal S ^ 2) :
    IsRegularLocalRing (AdjoinRoot g) ∧ ringKrullDim (AdjoinRoot g) = ringKrullDim S

Uses 1

Proof usesInjective integral maps preserve Krull dimension

TheoremRegular local rings of dimension at most two are UFDs#✓fully proved

A regular local ring of Krull dimension at most two is a unique factorization monoid.

theorem IsRegularLocalRing.uniqueFactorizationMonoid_of_ringKrullDim_le_two
    (R : Type*) [CommRing R] [IsRegularLocalRing R]
    (hdim : ringKrullDim R ≤ 2) : UniqueFactorizationMonoid R

Uses 4

Proof usesExistence of a parameter avoiding minimal primes and the square · Unique factorization from a principal ideal ring quotient · Regular local rings are domains · Quotient of a regular local ring by a regular parameter is regular

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.