mathlibdocumentation

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.

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] [ K] [ K] {L : Type u_4} [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ L] {ι : Type u_1} [fintype ι] [decidable_eq ι] (b : K L) (hb_int : ∀ (i : ι), (b i))  :
theorem integral_closure_le_span_dual_basis {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] {L : Type u_4} [field L] [ L] [ L] [ L] [ L] [ L] {ι : Type u_1} [fintype ι] [decidable_eq ι] (b : K L) (hb_int : ∀ (i : ι), (b i))  :
theorem exists_integral_multiples (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] {L : Type u_4} [field L] [ L] [ L] [ L] [ L] (s : finset L) :
∃ (y : A) (H : y 0), ∀ (x : L), x s (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] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] :
∃ (s : finset L) (b : K L), ∀ (x : s), (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_ring (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ L]  :
theorem integral_closure.is_noetherian_ring {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] [ L]  :
theorem is_integral_closure.is_dedekind_domain (A : Type u_2) (K : Type u_3) [comm_ring A] [field K] [is_domain A] [ K] [ K] (L : Type u_4) [field L] (C : Type u_5) [comm_ring C] [ L] [ L] [ L] [ L] [ L] [ L] [ C] [ L] [ 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] [ K] [ K] (L : Type u_4) [field L] [ L] [ L] [ L] [ L] [ 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] [ L] [ L] [ L] [ L] [ L]  :