Integral closure of Dedekind domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : ¬ is_field A) assumption whenever this is explicitly needed.
References #
- D. Marcus, Number Fields
- J.W.S. Cassels, A. Frölich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
Tags #
dedekind domain, dedekind ring
is_integral_closure 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
is_integral_closure.is_localization
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[is_separable K L]
[no_zero_smul_divisors A L] :
theorem
is_integral_closure.range_le_span_dual_basis
{A : Type u_2}
{K : Type u_3}
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
{L : Type u_4}
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(b : basis ι K L)
(hb_int : ∀ (i : ι), is_integral A (⇑b i))
[is_integrally_closed A] :
linear_map.range (linear_map.restrict_scalars A (algebra.linear_map C L)) ≤ submodule.span A (set.range ⇑((algebra.trace_form K L).dual_basis _ b))
theorem
integral_closure_le_span_dual_basis
{A : Type u_2}
{K : Type u_3}
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
{L : Type u_4}
[field L]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[finite_dimensional K L]
[is_separable K L]
{ι : Type u_1}
[fintype ι]
[decidable_eq ι]
(b : basis ι K L)
(hb_int : ∀ (i : ι), is_integral A (⇑b i))
[is_integrally_closed A] :
⇑subalgebra.to_submodule (integral_closure A L) ≤ submodule.span A (set.range ⇑((algebra.trace_form K L).dual_basis _ b))
theorem
exists_integral_multiples
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
{L : Type u_4}
[field L]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[finite_dimensional K L]
(s : finset L) :
Send a set of x'es in a finite extension L of the fraction field of R
to (y : R) • x ∈ integral_closure R L.
theorem
finite_dimensional.exists_is_basis_integral
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[finite_dimensional K L] :
If L is a finite extension of K = Frac(A),
then L has a basis over A consisting of integral elements.
theorem
is_integral_closure.is_noetherian
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
[is_integrally_closed A]
[is_noetherian_ring A] :
is_noetherian A C
theorem
is_integral_closure.is_noetherian_ring
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
[is_integrally_closed A]
[is_noetherian_ring A] :
theorem
is_integral_closure.module_free
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
[no_zero_smul_divisors A L]
[is_principal_ideal_ring A] :
module.free A C
theorem
is_integral_closure.rank
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
[is_principal_ideal_ring A]
[no_zero_smul_divisors A L] :
theorem
integral_closure.is_noetherian_ring
{A : Type u_2}
{K : Type u_3}
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[finite_dimensional K L]
[is_separable K L]
[is_integrally_closed A]
[is_noetherian_ring A] :
theorem
is_integral_closure.is_dedekind_domain
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
(C : Type u_5)
[comm_ring C]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[algebra C L]
[is_integral_closure C A L]
[algebra A C]
[is_scalar_tower A C L]
[finite_dimensional K L]
[is_separable K L]
[is_domain C]
[h : is_dedekind_domain A] :
theorem
integral_closure.is_dedekind_domain
(A : Type u_2)
(K : Type u_3)
[comm_ring A]
[field K]
[is_domain A]
[algebra A K]
[is_fraction_ring A K]
(L : Type u_4)
[field L]
[algebra K L]
[algebra A L]
[is_scalar_tower A K L]
[finite_dimensional K L]
[is_separable K L]
[h : is_dedekind_domain A] :
@[protected, instance]
def
integral_closure.is_dedekind_domain_fraction_ring
(A : Type u_2)
[comm_ring A]
[is_domain A]
(L : Type u_4)
[field L]
[algebra A L]
[algebra (fraction_ring A) L]
[is_scalar_tower A (fraction_ring A) L]
[finite_dimensional (fraction_ring A) L]
[is_separable (fraction_ring A) L]
[is_dedekind_domain A] :