Theorems · Theorem · commutative algebra

IsDiscreteValuationRing.TFAE

∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  ¬IsField R →
    [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime,
        Submodule.IsPrincipal (IsLocalRing.maximalIdeal R),
        Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1,
        ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE

The following are equivalent for a Noetherian local domain that is not a field (R, m, k): 0. R is a discrete valuation ring 1. R is a valuation ring 2. R is a Dedekind domain 3. R is integrally closed with a unique non-zero prime ideal 4. m is principal 5. dimₖ m/m² = 1 6. Every nonzero ideal is a power of m. Also see tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain for a version without ¬ IsField R.

Defined in

Mathlib.RingTheory.DiscreteValuationRing.TFAE

Cited by

3 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsNoetherianRingIsLocalRingIsDomain