Dedekind domains #
This file defines an equivalent notion of a Dedekind domain (or Dedekind ring), namely a Noetherian integral domain where the localization at all nonzero prime ideals is a DVR (TODO: and shows that it is equivalent to the main definition).
Main definitions #
is_dedekind_domain_dvralternatively defines a Dedekind domain as an integral domain that is Noetherian, and the localization at every nonzero prime ideal is a DVR.
Implementation notes #
The definitions that involve a field of fractions choose a canonical field of fractions,
but are independent of that choice. The
..._iff lemmas express this independence.
Often, definitions assume that Dedekind domains are not fields. We found it more practical
to add a
(h : ¬ is_field A) assumption whenever this is explicitly needed.
- D. Marcus, Number Fields
- J.W.S. Cassels, A. Frölich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
dedekind domain, dedekind ring
- is_noetherian_ring : is_noetherian_ring A
- is_dvr_at_nonzero_prime : ∀ (P : ideal A), P ≠ ⊥ → ∀ (ᾰ : P.is_prime), discrete_valuation_ring (localization.at_prime P)
A Dedekind domain is an integral domain that is Noetherian, and the localization at every nonzero prime is a discrete valuation ring.
This is equivalent to
TODO: prove the equivalence.