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][marcus1977number]
[J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
[J. Neukirch, Algebraic Number Theory][Neukirch1992]

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.

source

theorem IsIntegralClosure.isLocalization (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] (hKL : Algebra.IsAlgebraic K L) :

IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L

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

source

theorem IsIntegralClosure.isLocalization_of_isSeparable (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [IsSeparable K L] :

IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L

source

theorem IsIntegralClosure.range_le_span_dualBasis {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_4} [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) [IsIntegrallyClosed A] :

LinearMap.range (↑A (Algebra.linearMap C L)) ≤ Submodule.span A (Set.range ⇑(LinearMap.BilinForm.dualBasis (Algebra.traceForm K L) ⋯ b))

source

theorem integralClosure_le_span_dualBasis {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_4} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsSeparable K L] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) [IsIntegrallyClosed A] :

Subalgebra.toSubmodule (integralClosure A L) ≤ Submodule.span A (Set.range ⇑(LinearMap.BilinForm.dualBasis (Algebra.traceForm K L) ⋯ b))

source

theorem exists_integral_multiples (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] {L : Type u_4} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] (s : Finset L) :

∃ (y : A), y ≠ 0 ∧ ∀ x ∈ s, 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.

source

theorem FiniteDimensional.exists_is_basis_integral (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] :

∃ (s : Finset L) (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.

source

theorem IsIntegralClosure.isNoetherian (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A] :

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

source

theorem IsIntegralClosure.isNoetherianRing (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A] :

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

source

theorem IsIntegralClosure.module_free (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] [NoZeroSMulDivisors A L] [IsPrincipalIdealRing A] :

Module.Free 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.

source

theorem IsIntegralClosure.rank (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L] :

FiniteDimensional.finrank A C = FiniteDimensional.finrank K L

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.

source

theorem integralClosure.isNoetherianRing {A : Type u_2} {K : Type u_3} [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A] :

IsNoetherianRing ↥(integralClosure 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.

source

theorem IsIntegralClosure.isDedekindDomain (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] (C : Type u_5) [CommRing C] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra C L] [IsIntegralClosure C A L] [Algebra A C] [IsScalarTower A C L] [FiniteDimensional K L] [IsSeparable K L] [IsDomain C] [IsDedekindDomain A] :

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

source

theorem integralClosure.isDedekindDomain (A : Type u_2) (K : Type u_3) [CommRing A] [Field K] [IsDomain A] [Algebra A K] [IsFractionRing A K] (L : Type u_4) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsSeparable K L] [IsDedekindDomain A] :

IsDedekindDomain ↥(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.

source