Equivalent conditions for DVR #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In discrete_valuation_ring.tfae, we show that the following are equivalent for a
noetherian local domain (R, m, k):
Ris a discrete valuation ringRis a valuation ringRis a dedekind domainRis integrally closed with a unique prime idealmis principaldimₖ m/m² = 1- Every nonzero ideal is a power of
m.
theorem
exists_maximal_ideal_pow_eq_of_principal
(R : Type u_1)
[comm_ring R]
[is_noetherian_ring R]
[local_ring R]
[is_domain R]
(h : ¬is_field R)
(h' : submodule.is_principal (local_ring.maximal_ideal R))
(I : ideal R)
(hI : I ≠ ⊥) :
theorem
maximal_ideal_is_principal_of_is_dedekind_domain
(R : Type u_1)
[comm_ring R]
[local_ring R]
[is_domain R]
[is_dedekind_domain R] :
theorem
discrete_valuation_ring.tfae
(R : Type u_1)
[comm_ring R]
[is_noetherian_ring R]
[local_ring R]
[is_domain R]
(h : ¬is_field R) :
[discrete_valuation_ring R, valuation_ring R, is_dedekind_domain R, is_integrally_closed R ∧ ∃! (P : ideal R), P ≠ ⊥ ∧ P.is_prime, submodule.is_principal (local_ring.maximal_ideal R), finite_dimensional.finrank (local_ring.residue_field R) (local_ring.cotangent_space R) = 1, ∀ (I : ideal R), I ≠ ⊥ → (∃ (n : ℕ), I = local_ring.maximal_ideal R ^ n)].tfae