Theorems · Theorem · commutative algebra

tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain

∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
      IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = IsLocalRing.maximalIdeal R,
      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

Let (R, m, k) be a Noetherian local domain (possibly a field). The following are equivalent: 0. R is a PID 1. R is a valuation ring 2. R is a Dedekind domain 3. R is integrally closed with at most one non-zero prime ideal 4. m is principal 5. dimₖ m/m² ≤ 1 6. Every nonzero ideal is a power of m. Also see IsDiscreteValuationRing.TFAE for a version assuming ¬ IsField R.

Defined in

Mathlib.RingTheory.DiscreteValuationRing.TFAE

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingIsLocalRingIsDomain