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_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)
:
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]
:
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 ⇑(BilinForm.dualBasis (Algebra.traceForm K L) (_ : BilinForm.Nondegenerate (Algebra.traceForm K L)) b))
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 ⇑(BilinForm.dualBasis (Algebra.traceForm K L) (_ : BilinForm.Nondegenerate (Algebra.traceForm K L)) 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 ∧ ∀ 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_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]
[IsSeparable K L]
[IsIntegrallyClosed A]
[IsNoetherianRing A]
:
IsNoetherian A C
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]
:
Module.Free A C
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]
:
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)
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]
:
IsDedekindDomain ↥(integralClosure A L)
instance
integralClosure.isDedekindDomain_fractionRing
(A : Type u_2)
[CommRing A]
[IsDomain A]
(L : Type u_4)
[Field L]
[Algebra A L]
[Algebra (FractionRing A) L]
[IsScalarTower A (FractionRing A) L]
[FiniteDimensional (FractionRing A) L]
[IsSeparable (FractionRing A) L]
[IsDedekindDomain A]
:
IsDedekindDomain ↥(integralClosure A L)
Equations
- (_ : IsDedekindDomain ↥(integralClosure A L)) = (_ : IsDedekindDomain ↥(integralClosure A L))