mathlib documentation

ring_theory.integrally_closed

Integrally closed rings #

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 #

Main results #

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

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
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.

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

@[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] :
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
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
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
@[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] :
theorem integral_closure.mem_lifts_of_monic_of_dvd_map {R : Type u_1} [comm_ring R] (K : Type u_2) [field K] [algebra R K] {f : polynomial R} (hf : f.monic) {g : polynomial K} (hg : g.monic) (hd : g polynomial.map (algebra_map R K) f) :

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leading_coeff⁻¹) has coefficients in R