Regularity lifts along a regular quotient

Let R be a Noetherian local ring and x₁, …, x_r a regular sequence in its maximal ideal 𝔪. If R ⧸ (x₁, …, x_r) is a regular local ring, then so is R (Stacks, Lemma 10.106.7 (00NU)). The case r = 1 is used in the proof of Abhyankar's lemma for a regular divisor: the local rings of a scheme along a regular divisor are regular. Globally, if x is a nonzerodivisor of a Noetherian ring R with R ⧸ (x) regular, then R is regular at every prime containing x, since R_P ⧸ (x) is a localization of R ⧸ (x).

Main results

• Ideal.isRegularLocalRing_of_quotient_of_spanFinrank_le: if R ⧸ I is a regular local ring, I needs at most n generators and dim (R ⧸ I) + n ≤ dim R, then R is a regular local ring.
• TauCeti.IsRegularLocalRing.of_quotient_isRegular: if rs is a regular sequence in a Noetherian local ring R and R ⧸ Ideal.ofList rs is a regular local ring, then R is a regular local ring.
• TauCeti.IsRegularLocalRing.of_quotient_nonZeroDivisor: the case of one nonzerodivisor x in the maximal ideal.
• TauCeti.IsRegularLocalRing.localization_of_quotient_nonZeroDivisor: for a nonzerodivisor x of a Noetherian ring R and a prime P of R ⧸ (x) at which R ⧸ (x) is regular, R is regular at the preimage of P.
• TauCeti.IsRegularLocalRing.localization_of_isRegularRing_quotient: if moreover R ⧸ (x) is a regular ring, then R is regular at every prime containing x.

References

• Stacks Project, Lemma 10.106.7.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Bounding/PrincipalQuotientRegular.lean: of_quotient_nonZeroDivisor is its Pcf.isRegularLocalRing_of_quotient_nonZeroDivisor. The regular-sequence form of_quotient_isRegular extends the same argument to sequences of any length.

theorem Ideal.isRegularLocalRing_of_quotient_of_spanFinrank_le {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (I : Ideal R) [IsRegularLocalRing (R ⧸ I)] {n : ℕ} (hn : Submodule.spanFinrank I ≤ n) (hdim : ringKrullDim (R ⧸ I) + ↑n ≤ ringKrullDim R) : IsRegularLocalRing R

Regularity lifts along a quotient of the expected dimension. Let I be an ideal of a Noetherian local ring R with R ⧸ I regular local (so I ≤ 𝔪). If I is generated by at most n elements and dim (R ⧸ I) + n ≤ dim R, then R is regular local. The two theorems TauCeti.IsRegularLocalRing.of_quotient_isRegular and TauCeti.IsRegularLocalRing.of_quotient_nonZeroDivisor are the cases where I is generated by a regular sequence.

theorem TauCeti.IsRegularLocalRing.of_quotient_isRegular {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {rs : List R} (hrs : RingTheory.Sequence.IsRegular R rs) [IsRegularLocalRing (R ⧸ Ideal.ofList rs)] : IsRegularLocalRing R

Regularity lifts along a regular sequence. If rs is a regular sequence in a Noetherian local ring R and R ⧸ (rs) is a regular local ring, then R is a regular local ring. Stacks, Lemma 10.106.7 (00NU), second sentence.

theorem TauCeti.IsRegularLocalRing.of_quotient_nonZeroDivisor (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) (hreg : x ∈ nonZeroDivisors R) [IsRegularLocalRing (R ⧸ Ideal.span {x})] : IsRegularLocalRing R

Regularity lifts along a nonzerodivisor. A Noetherian local ring with a nonzerodivisor x in the maximal ideal such that R ⧸ (x) is a regular local ring is a regular local ring. Stacks, Lemma 10.106.7 (00NU), first sentence.

theorem TauCeti.IsRegularLocalRing.localization_of_quotient_nonZeroDivisor {R : Type u} [CommRing R] [IsNoetherianRing R] {x : R} (hx : x ∈ nonZeroDivisors R) (P : Ideal (R ⧸ Ideal.span {x})) [P.IsPrime] [IsRegularLocalRing (Localization.AtPrime P)] : IsRegularLocalRing (Localization.AtPrime (Ideal.comap (Ideal.Quotient.mk (Ideal.span {x})) P))

Regularity lifts along a nonzerodivisor, at a prime. Let x be a nonzerodivisor of a Noetherian ring R and P a prime of R ⧸ (x) at which R ⧸ (x) is regular. Then R is regular at the preimage of P, a prime containing x.

theorem TauCeti.IsRegularLocalRing.localization_of_isRegularRing_quotient {R : Type u} [CommRing R] [IsNoetherianRing R] {x : R} (hx : x ∈ nonZeroDivisors R) [IsRegularRing (R ⧸ Ideal.span {x})] (P : Ideal R) [P.IsPrime] (hxP : x ∈ P) : IsRegularLocalRing (Localization.AtPrime P)

Regularity lifts along a nonzerodivisor with regular quotient. If x is a nonzerodivisor of a Noetherian ring R and R ⧸ (x) is a regular ring, then R is regular at every prime containing x.