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 implies the main definition).
Main definitions #
IsDedekindDomainDvralternatively defines a Dedekind domain as an integral domain that is Noetherian, and the localization at every nonzero prime ideal is a DVR.
Main results #
IsDedekindDomainimplies the localization at each nonzero prime ideal is a DVR.
IsDedekindDomain.isDedekindDomainDvris one direction of the equivalence of definitions of a Dedekind domain
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 : ¬ IsField A) assumption whenever this is explicitly needed.
- [D. Marcus, Number Fields][marcus1977number]
- [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
- [J. Neukirch, Algebraic Number Theory][Neukirch1992]
dedekind domain, dedekind ring
- isNoetherianRing : IsNoetherianRing A
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.
Localizing a domain of Krull dimension
≤ 1 gives another ring of Krull dimension
Note that the same proof can/should be generalized to preserving any Krull dimension, once we have a suitable definition.
The localization of a Dedekind domain is a Dedekind domain.
The localization of a Dedekind domain at every nonzero prime ideal is a Dedekind domain.
In a Dedekind domain, the localization at every nonzero prime ideal is a DVR.
Dedekind domains, in the sense of Noetherian integrally closed domains of Krull dimension ≤ 1, are also Dedekind domains in the sense of Noetherian domains where the localization at every nonzero prime ideal is a DVR.