Dedekind domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the notion of a Dedekind domain (or Dedekind ring), as a Noetherian integrally closed commutative ring of Krull dimension at most one.
Main definitions #
is_dedekind_domaindefines a Dedekind domain as a commutative ring that is Noetherian, integrally closed in its field of fractions and has Krull dimension at most one.
is_dedekind_domain_iffshows that this does not depend on the choice of field of fractions.
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
- dimension_le_one : ring.dimension_le_one A
- is_integrally_closed : is_integrally_closed A
A Dedekind domain is an integral domain that is Noetherian, integrally closed, and has Krull dimension at most one.
This is definition 3.2 of [Neu99].
An integral domain is a Dedekind domain iff and only if it is Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field. In particular, this definition does not depend on the choice of this fraction field.