Equivalent conditions for DVR

In DiscreteValuationRing.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_localRing_of_isDomain for a version without ¬ IsField R.

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

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

theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain (R : Type u_1) [CommRing R] [IsNoetherianRing R] [LocalRing R] [IsDomain R] : List.TFAE [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → Ideal.IsPrime P → P = LocalRing.maximalIdeal R, Submodule.IsPrincipal (LocalRing.maximalIdeal R), FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) ≤ 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = LocalRing.maximalIdeal R ^ n]

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 DiscreteValuationRing.TFAE for a version assuming ¬ IsField R.

theorem DiscreteValuationRing.TFAE (R : Type u_1) [CommRing R] [IsNoetherianRing R] [LocalRing R] [IsDomain R] (h : ¬IsField R) : List.TFAE [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ Ideal.IsPrime P, Submodule.IsPrincipal (LocalRing.maximalIdeal R), FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ (n : ℕ), I = LocalRing.maximalIdeal R ^ n]

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_localRing_of_isDomain for a version without ¬ IsField R.

theorem LocalRing.finrank_CotangentSpace_eq_one_iff {R : Type u_1} [CommRing R] [IsNoetherianRing R] [LocalRing R] [IsDomain R] : FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1 ↔ DiscreteValuationRing R

theorem LocalRing.finrank_CotangentSpace_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [DiscreteValuationRing R] : FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1

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

Equations

• ⋯ = ⋯