Integrally closed local domains of dimension one

A Noetherian integrally closed local domain of Krull dimension one is a discrete valuation ring (Stacks, Lemma 10.119.7 (00PD)). Mathlib proves the equivalence of the conditions in tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, one of which asks for integral closedness together with "every nonzero prime is the maximal ideal"; this file supplies that condition from the dimension.

Main results

• IsPrincipalIdealRing.of_krullDimLE_one: a Noetherian integrally closed local domain of Krull dimension at most one is a principal ideal ring.
• IsDiscreteValuationRing.of_krullDimLE_one: a Noetherian integrally closed local domain of Krull dimension at most one that is not a field is a discrete valuation ring.
• IsDiscreteValuationRing.of_ringKrullDim_eq_one: the dimension-one specialization.
• IsLocalization.AtPrime.isDiscreteValuationRing_of_height_eq_one: the localization of a Noetherian integrally closed domain at a prime of height one is a discrete valuation ring.
• IsLocalization.AtPrime.isPrincipalIdealRing_of_height_le_one: the localization of a Noetherian integrally closed domain at a prime of height at most one is a principal ideal ring.

References

• Stacks Project, Lemma 10.119.7.
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0): the ring-level step of Pcf.isDiscreteValuationRing_localizationAtPrime_of_heightOne in lean/Pcf/Bounding/Divisors.lean, stated there for the localization of a Noetherian integrally closed domain at a prime of height one.

theorem IsPrincipalIdealRing.of_krullDimLE_one {R : Type u_1} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R] [IsIntegrallyClosed R] [Ring.KrullDimLE 1 R] : IsPrincipalIdealRing R

A Noetherian integrally closed local domain of Krull dimension at most one is a principal ideal ring: it is a field or a discrete valuation ring.

theorem IsDiscreteValuationRing.of_krullDimLE_one {R : Type u_1} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R] [IsIntegrallyClosed R] [Ring.KrullDimLE 1 R] (hnot : ¬IsField R) : IsDiscreteValuationRing R

A Noetherian integrally closed local domain of Krull dimension at most one that is not a field is a discrete valuation ring.

theorem IsDiscreteValuationRing.of_ringKrullDim_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [IsLocalRing R] [IsNoetherianRing R] [IsIntegrallyClosed R] (h : ringKrullDim R = 1) : IsDiscreteValuationRing R

A Noetherian integrally closed local domain of Krull dimension one is a discrete valuation ring. Stacks, Lemma 10.119.7 (00PD).

theorem IsLocalization.AtPrime.isDiscreteValuationRing_of_height_eq_one {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] {P : Ideal A} [P.IsPrime] (hP : P.height = 1) (Aₚ : Type u_2) [CommRing Aₚ] [IsDomain Aₚ] [Algebra A Aₚ] [IsLocalization.AtPrime Aₚ P] : IsDiscreteValuationRing Aₚ

The localization of a Noetherian integrally closed domain at a prime of height one is a discrete valuation ring. Stacks, Lemma 10.119.7 (00PD).

theorem IsLocalization.AtPrime.isPrincipalIdealRing_of_height_le_one {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] [IsIntegrallyClosed A] {P : Ideal A} [P.IsPrime] (hP : P.height ≤ 1) (Aₚ : Type u_2) [CommRing Aₚ] [Algebra A Aₚ] [IsLocalization.AtPrime Aₚ P] : IsPrincipalIdealRing Aₚ

The localization of a Noetherian integrally closed domain at a prime of height at most one is a principal ideal ring: a field at the zero ideal, and a discrete valuation ring at a prime of height one.