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.

theorem IsIntegralClosure.isLocalization (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [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⁰.

theorem IsIntegralClosure.isLocalization_of_isSeparable (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.IsSeparable K L] : IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L

theorem IsIntegralClosure.range_le_span_dualBasis {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] (C : Type u_4) [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] [Algebra.IsSeparable K L] {ι : Type u_5} [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 ⇑((Algebra.traceForm K L).dualBasis ⋯ b))

theorem integralClosure_le_span_dualBasis {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] {ι : Type u_5} [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 ⇑((Algebra.traceForm K L).dualBasis ⋯ b))

theorem exists_integral_multiples (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsDomain A] (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.

theorem FiniteDimensional.exists_is_basis_integral (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsDomain A] : ∃ (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.

theorem IsIntegralClosure.isNoetherian (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.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.

theorem IsIntegralClosure.isNoetherianRing (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.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.

theorem IsIntegralClosure.finite (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A] : Module.Finite 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 finite over A.

theorem IsIntegralClosure.module_free (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.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.

theorem IsIntegralClosure.rank (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.IsSeparable K L] [IsPrincipalIdealRing A] [NoZeroSMulDivisors A L] : Module.finrank A C = Module.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.

theorem integralClosure.isNoetherianRing {A : Type u_1} {K : Type u_2} [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsDomain A] [Algebra.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.

theorem IsIntegralClosure.isDedekindDomain (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] (C : Type u_4) [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] [IsDomain A] [Algebra.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.

theorem integralClosure.isDedekindDomain (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsDomain A] [Algebra.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.

instance integralClosure.isDedekindDomain_fractionRing (A : Type u_1) [CommRing A] (L : Type u_3) [Field L] [Algebra A L] [IsDomain A] [Algebra (FractionRing A) L] [IsScalarTower A (FractionRing A) L] [FiniteDimensional (FractionRing A) L] [Algebra.IsSeparable (FractionRing A) L] [IsDedekindDomain A] : IsDedekindDomain ↥(integralClosure A 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

• ⋯ = ⋯