Integrally closed rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An integrally closed domain R contains all the elements of Frac(R) that are integral over R. A special case of integrally closed domains are the Dedekind domains.

Main definitions #

is_integrally_closed R states R contains all integral elements of Frac(R)

Main results #

is_integrally_closed_iff K, where K is a fraction field of R, states R is integrally closed iff it is the integral closure of R in K

source

@[class]

structure is_integrally_closed (R : Type u_1) [comm_ring R] [is_domain R] :

Prop

algebra_map_eq_of_integral : ∀ {x : fraction_ring R}, is_integral R x → (∃ (y : R), ⇑(algebra_map R (fraction_ring R)) y = x)

R is integrally closed if all integral elements of Frac(R) are also elements of R.

This definition uses fraction_ring R to denote Frac(R). See is_integrally_closed_iff if you want to choose another field of fractions for R.

Instances of this typeclass

source

theorem is_integrally_closed_iff {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] :

is_integrally_closed R ↔ ∀ {x : K}, is_integral R x → (∃ (y : R), ⇑(algebra_map R K) y = x)

R is integrally closed iff all integral elements of its fraction field K are also elements of R.

source

theorem is_integrally_closed_iff_is_integral_closure {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [algebra R K] [is_fraction_ring R K] :

is_integrally_closed R ↔ is_integral_closure R R K

R is integrally closed iff it is the integral closure of itself in its field of fractions.

source

@[protected, instance]

def is_integrally_closed.is_integral_closure {R : Type u_1} [comm_ring R] [id : is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [algebra R K] [ifr : is_fraction_ring R K] :

is_integral_closure R R K

source

theorem is_integrally_closed.is_integral_iff {R : Type u_1} [comm_ring R] [id : is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [algebra R K] [ifr : is_fraction_ring R K] {x : K} :

is_integral R x ↔ ∃ (y : R), ⇑(algebra_map R K) y = x

source

theorem is_integrally_closed.exists_algebra_map_eq_of_is_integral_pow {R : Type u_1} [comm_ring R] [id : is_domain R] [iic : is_integrally_closed R] {K : Type u_2} [field K] [algebra R K] [ifr : is_fraction_ring R K] {x : K} {n : ℕ} (hn : 0 < n) (hx : is_integral R (x ^ n)) :

∃ (y : R), ⇑(algebra_map R K) y = x

source

theorem is_integrally_closed.exists_algebra_map_eq_of_pow_mem_subalgebra {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [algebra R K] {S : subalgebra R K} [is_integrally_closed ↥S] [is_fraction_ring ↥S K] {x : K} {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ S) :

∃ (y : ↥S), ⇑(algebra_map ↥S K) y = x

source

theorem is_integrally_closed.integral_closure_eq_bot_iff {R : Type u_1} [comm_ring R] [id : is_domain R] (K : Type u_2) [field K] [algebra R K] [ifr : is_fraction_ring R K] :

integral_closure R K = ⊥ ↔ is_integrally_closed R

source

@[simp]

theorem is_integrally_closed.integral_closure_eq_bot (R : Type u_1) [comm_ring R] [id : is_domain R] [iic : is_integrally_closed R] (K : Type u_2) [field K] [algebra R K] [ifr : is_fraction_ring R K] :

integral_closure R K = ⊥

source

theorem integral_closure.is_integrally_closed_of_finite_extension {R : Type u_1} [comm_ring R] (K : Type u_2) [field K] [algebra R K] [is_domain R] [is_fraction_ring R K] {L : Type u_3} [field L] [algebra K L] [algebra R L] [is_scalar_tower R K L] [finite_dimensional K L] :

is_integrally_closed ↥(integral_closure R L)