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.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] :
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] :
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 x, ∀ (x : L), x sIsIntegral 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 b, ∀ (x : { x // 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] [IsSeparable K L] [IsIntegrallyClosed A] [IsNoetherianRing A] :
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] :
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] :
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] :
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] :