# 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.

## References #

- D. Marcus,
*Number Fields* - J.W.S. Cassels, A. Frölich,
*Algebraic Number Theory* - J. Neukirch,
*Algebraic Number Theory*

## Tags #

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.

If `L`

is an algebraic extension of `K = Frac(A)`

and `L`

has no zero smul divisors by `A`

,
then `L`

is the localization of the integral closure `C`

of `A`

in `L`

at `A⁰`

.

Send a set of `x`

s in a finite extension `L`

of the fraction field of `R`

to `(y : R) • x ∈ integralClosure R L`

.

If `L`

is a finite extension of `K = Frac(A)`

,
then `L`

has a basis over `A`

consisting of integral elements.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is
integrally closed and Noetherian, the integral closure `C`

of `A`

in `L`

is
Noetherian over `A`

.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is
integrally closed and Noetherian, the integral closure `C`

of `A`

in `L`

is
Noetherian.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is a principal ring
and `L`

has no zero smul divisors by `A`

, the integral closure `C`

of `A`

in `L`

is
a free `A`

-module.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is a principal ring
and `L`

has no zero smul divisors by `A`

, the `A`

-rank of the integral closure `C`

of `A`

in `L`

is equal to the `K`

-rank of `L`

.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is
integrally closed and Noetherian, the integral closure of `A`

in `L`

is
Noetherian.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is a Dedekind domain,
the integral closure `C`

of `A`

in `L`

is a Dedekind domain.

This cannot be an instance since `A`

, `K`

or `L`

can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing`

where `K := FractionRing A`

and `C := integralClosure A L`

.

If `L`

is a finite separable extension of `K = Frac(A)`

, where `A`

is a Dedekind domain,
the integral closure of `A`

in `L`

is a Dedekind domain.

This cannot be an instance since `K`

can't be inferred. See also the instance
`integralClosure.isDedekindDomain_fractionRing`

where `K := FractionRing A`

.

If `L`

is a finite separable extension of `Frac(A)`

, where `A`

is a Dedekind domain,
the integral closure of `A`

in `L`

is a Dedekind domain.

See also the lemma `integralClosure.isDedekindDomain`

where you can choose
the field of fractions yourself.

## Equations

- ⋯ = ⋯