Regular local rings are domains

A Noetherian local ring R is regular (IsRegularLocalRing) when its maximal ideal 𝔪 can be generated by dim R elements. This file proves that a regular local ring is an integral domain. Consequently the local rings of a regular scheme are domains, which is what makes a connected regular scheme irreducible, and a regular local ring of dimension one is a discrete valuation ring, so that the local rings of a regular curve at its codimension-one points are discrete valuation rings.

Main declarations

• TauCeti.IsRegularLocalRing.isDomain: a regular local ring is an integral domain;
• TauCeti.IsRegularLocalRing.quotient_span_singleton: for x ∈ 𝔪 \ 𝔪², the quotient R ⧸ (x) is again a regular local ring, and TauCeti.IsRegularLocalRing.quotient_span_singleton_iff: for a nonzero x ∈ 𝔪 this happens exactly when x ∉ 𝔪²;
• TauCeti.IsRegularLocalRing.span_singleton_isPrime_of_notMem_sq: the quotient by such a parameter is a domain, so the ideal the parameter generates is prime, the hypothesis the statements for an irreducible first equation of TauCeti.RingTheory.Intersection take;
• TauCeti.IsRegularLocalRing.isDiscreteValuationRing_iff_ringKrullDim_eq_one: a regular local ring is a discrete valuation ring exactly when it has dimension one.

References

• The Stacks Project, Lemma 10.106.2 and Lemma 10.106.3.
• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Lemma 11.23.

@[instance 100]

instance TauCeti.IsRegularLocalRing.isDomain {R : Type u} [CommRing R] [IsRegularLocalRing R] : IsDomain R

A regular local ring is an integral domain.

theorem TauCeti.IsRegularLocalRing.quotient_span_singleton {R : Type u} [CommRing R] [IsRegularLocalRing R] {x : R} (hxm : x ∈ IsLocalRing.maximalIdeal R) (hx : x ∉ IsLocalRing.maximalIdeal R ^ 2) : IsRegularLocalRing (R ⧸ Ideal.span {x})

If R is a regular local ring and x ∈ 𝔪 \ 𝔪², then R ⧸ (x) is a regular local ring.

theorem TauCeti.IsRegularLocalRing.quotient_span_singleton_iff {R : Type u} [CommRing R] [IsRegularLocalRing R] {x : R} (hxm : x ∈ IsLocalRing.maximalIdeal R) (hx0 : x ≠ 0) : IsRegularLocalRing (R ⧸ Ideal.span {x}) ↔ x ∉ IsLocalRing.maximalIdeal R ^ 2

If R is a regular local ring and x ∈ 𝔪 is nonzero, then R ⧸ (x) is a regular local ring exactly when x ∉ 𝔪².

theorem TauCeti.IsRegularLocalRing.span_singleton_isPrime_of_notMem_sq {R : Type u} [CommRing R] [IsRegularLocalRing R] {f : R} (hfm : f ∈ IsLocalRing.maximalIdeal R) (hf2 : f ∉ IsLocalRing.maximalIdeal R ^ 2) : (Ideal.span {f}).IsPrime

The curve a parameter cuts out is a domain, so its principal ideal is prime. Let (R, 𝔪) be a regular local ring and let f ∈ 𝔪 \ 𝔪², so that f is a parameter. Then the quotient R ⧸ (f) is a regular local ring by TauCeti.IsRegularLocalRing.quotient_span_singleton, hence a domain by TauCeti.IsRegularLocalRing.isDomain, and Ideal.Quotient.isDomain_iff_prime reads that back as the primality of (f), the hypothesis the statements for an irreducible first equation of TauCeti.RingTheory.Intersection take. A consumer needing the domain instance itself obtains it from the primality, as (Ideal.Quotient.isDomain_iff_prime _).mp of it.

In a ring of Krull dimension two that curve is a discrete valuation ring as well, being a regular local ring of dimension one by TauCeti.ringKrullDim_quotient_span_singleton_eq_one and therefore by TauCeti.IsRegularLocalRing.isDiscreteValuationRing_iff_ringKrullDim_eq_one.

theorem TauCeti.IsRegularLocalRing.isDiscreteValuationRing_iff_ringKrullDim_eq_one {R : Type u} [CommRing R] [IsRegularLocalRing R] : IsDiscreteValuationRing R ↔ ringKrullDim R = 1

A regular local ring is a discrete valuation ring exactly when it has dimension one.