Documentation

Mathlib.RingTheory.DedekindDomain.IntegralClosure

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 #

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) [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] [Algebra.IsAlgebraic K 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.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] [Algebra.IsSeparable K L] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ (i : ι), IsIntegral A (b i)) [IsIntegrallyClosed A] :
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] [Algebra.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 ((Algebra.traceForm K L).dualBasis b))
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 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) [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.

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] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing 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 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.

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] [Algebra.IsSeparable K L] [NoZeroSMulDivisors A L] [IsPrincipalIdealRing A] :

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.

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] [Algebra.IsSeparable K L] [IsDomain C] [IsDedekindDomain A] :

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