Discrete valuation rings at height-one primes

TheoremLocalization at a height-one prime is a DVR#✓fully proved

In a Noetherian integrally closed domain, the localization at a height-one prime ideal is a discrete valuation ring.

theorem Localization.AtPrime.isDiscreteValuationRing_of_height_eq_one
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    (p : Ideal R) [p.IsPrime] (hp : p.height = 1) :
    IsDiscreteValuationRing (Localization.AtPrime p)

Used by 1

Used byValuation subring at a height-one prime of a normal domain

TheoremValuation subring at a height-one prime of a normal domain#✓fully proved

At a height-one prime of a Noetherian integrally closed domain, there is a principal ideal valuation subring of the fraction field whose membership is the usual numerator-denominator criterion.

theorem IsIntegrallyClosed.exists_valuationSubring_mem_iff_of_height_eq_one
    {R : Type*} [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R]
    (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
    (p : Ideal R) [p.IsPrime] (hp : p.height = 1) :
    ∃ V : ValuationSubring K, IsPrincipalIdealRing V ∧ V ≠ ⊤ ∧
      ∀ x : K, x ∈ V ↔
        ∃ r s : R, s ∉ p ∧ x * algebraMap R K s = algebraMap R K r

Uses 1

Proof usesLocalization at a height-one prime is a DVR

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.