Integral closure of Dedekind domains #
This file shows the integral closure of a Dedekind domain (in particular, the ring of integers of a number field) is 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
IsIntegralClosure section #
We show that an integral closure of a Dedekind domain in a finite separable field extension is again a Dedekind domain. This implies the ring of integers of a number field is a Dedekind domain.
Send a set of
xs in a finite extension
L of the fraction field of
(y : R) • x ∈ integralClosure R L.
L is a finite extension of
K = Frac(A),
L has a basis over
A consisting of integral elements.