Equivalent conditions for DVR

In IsDiscreteValuationRing.TFAE, we show that the following are equivalent for a Noetherian local domain that is not a field (R, m, k):

• R is a discrete valuation ring
• R is a valuation ring
• R is a Dedekind domain
• R is integrally closed with a unique prime ideal
• m is principal
• dimₖ m/m² = 1
• Every nonzero ideal is a power of m.

Also see tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain for a version without ¬ IsField R.

theorem exists_maximalIdeal_pow_eq_of_principal (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] (h' : Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)) (I : Ideal R) (hI : I ≠ ⊥) : ∃ (n : ℕ), I = IsLocalRing.maximalIdeal R ^ n

theorem maximalIdeal_isPrincipal_of_isDedekindDomain (R : Type u_1) [CommRing R] [IsLocalRing R] [IsDedekindDomain R] : Submodule.IsPrincipal (IsLocalRing.maximalIdeal R)

theorem tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [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.

theorem IsDiscreteValuationRing.TFAE (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] (h : ¬IsField R) : [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P : Ideal R, 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.

theorem IsLocalRing.finrank_CotangentSpace_eq_one_iff {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] : Module.finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

theorem IsLocalRing.finrank_CotangentSpace_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : Module.finrank (ResidueField R) (CotangentSpace R) = 1

theorem IsDiscreteValuationRing.ringKrullDim_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ringKrullDim R = 1

theorem IsDiscreteValuationRing.not_krullDimLE_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ¬Ring.KrullDimLE 0 R

instance instKrullDimLEOfNatNatOfIsDiscreteValuationRing (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : Ring.KrullDimLE 1 R

@[instance 100]

instance IsDedekindDomain.isPrincipalIdealRing (R : Type u_1) [CommRing R] [IsLocalRing R] [IsDedekindDomain R] : IsPrincipalIdealRing R