Documentation

Mathlib.RingTheory.DiscreteValuationRing.TFAE

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):

Also see tfae_of_isNoetherianRing_of_localRing_of_isDomain for a version without ¬ IsField R.

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.

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.

@[instance 100]
Equations
  • =