mathlib documentation

ring_theory.dedekind_domain.integral_closure

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 : ¬ is_field A) assumption whenever this is explicitly needed.

References #

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.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] [finite_dimensional 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] {ι : Type u_1} [fintype ι] [decidable_eq ι] (b : basis ι K L) (hb_int : ∀ (i : ι), is_integral A (b i)) [is_integrally_closed A] :
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] [finite_dimensional K L] [algebra A L] [is_scalar_tower A 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] :
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] [finite_dimensional K L] [algebra A L] [is_scalar_tower A K L] (s : finset L) :
∃ (y : A) (H : y 0), ∀ (x : L), x sis_integral A (y x)

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] [finite_dimensional K L] [algebra A L] [is_scalar_tower A K L] :
∃ (s : finset L) (b : basis s K L), ∀ (x : s), is_integral 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 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] [finite_dimensional 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] [is_integrally_closed A] [is_noetherian_ring A] :
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] [finite_dimensional 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] [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] [finite_dimensional 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] [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] [finite_dimensional K L] [algebra A L] [is_scalar_tower A K L] [is_separable K L] [h : is_dedekind_domain A] :