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

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

theorem IsIntegralClosure.isLocalization (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] :

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

theorem IsIntegralClosure.isLocalization_of_isSeparable (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] :
theorem IsIntegralClosure.range_le_span_dualBasis {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] {L : Type u_4} [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] {ι : Type u_6} [] [] (b : Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) :
LinearMap.range (A ()) Submodule.span A (Set.range (().dualBasis b))
theorem integralClosure_le_span_dualBasis {A : Type u_2} {K : Type u_3} [] [] [Algebra A K] [] {L : Type u_4} [] [Algebra K L] [Algebra A L] [] [] [] {ι : Type u_6} [] [] (b : Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) :
Subalgebra.toSubmodule () Submodule.span A (Set.range (().dualBasis b))
theorem exists_integral_multiples (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] {L : Type u_4} [] [Algebra K L] [Algebra A L] [] [] (s : ) :
∃ (y : A), y 0 xs, IsIntegral A (y x)

Send a set of xs in a finite extension L of the fraction field of R to (y : R) • x ∈ integralClosure R L.

theorem FiniteDimensional.exists_is_basis_integral (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] [Algebra K L] [Algebra A L] [] [] :
∃ (s : ) (b : Basis { x : L // x s } K L), ∀ (x : { x : L // x s }), IsIntegral A (b x)

If L is a finite extension of K = Frac(A), then L has a basis over A consisting of integral elements.

theorem IsIntegralClosure.isNoetherian (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] [] :

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.

theorem IsIntegralClosure.isNoetherianRing (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] [] :

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.

theorem IsIntegralClosure.module_free (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] [] :

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.

theorem IsIntegralClosure.rank (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] [] :

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.

theorem integralClosure.isNoetherianRing {A : Type u_2} {K : Type u_3} [] [] [] [Algebra A K] [] (L : Type u_4) [] [Algebra K L] [Algebra A 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.

theorem IsIntegralClosure.isDedekindDomain (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] (C : Type u_5) [] [Algebra K L] [Algebra A L] [] [Algebra C L] [] [Algebra A C] [] [] [] [] [] :

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.

theorem integralClosure.isDedekindDomain (A : Type u_2) (K : Type u_3) [] [] [] [Algebra A K] [] (L : Type u_4) [] [Algebra K L] [Algebra 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.

instance integralClosure.isDedekindDomain_fractionRing (A : Type u_2) [] [] (L : Type u_4) [] [Algebra A L] [Algebra () L] [] [] [] [] :

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
• =