mathlib documentation

ring_theory.integral_closure

Integral closure of a subring. #

If A is an R-algebra then a : A is integral over R if it is a root of a monic polynomial with coefficients in R. Enough theory is developed to prove that integral elements form a sub-R-algebra of A.

Main definitions #

Let R be a comm_ring and let A be an R-algebra.

def ring_hom.is_integral_elem {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] (f : R →+* A) (x : A) :
Prop

An element x of A is said to be integral over R with respect to f if it is a root of a monic polynomial p : polynomial R evaluated under f

Equations
def ring_hom.is_integral {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] (f : R →+* A) :
Prop

A ring homomorphism f : R →+* A is said to be integral if every element A is integral with respect to the map f

Equations
def is_integral (R : Type u_1) {A : Type u_3} [comm_ring R] [ring A] [algebra R A] (x : A) :
Prop

An element x of an algebra A over a commutative ring R is said to be integral, if it is a root of some monic polynomial p : polynomial R. Equivalently, the element is integral over R with respect to the induced algebra_map

Equations
def algebra.is_integral (R : Type u_1) (A : Type u_3) [comm_ring R] [ring A] [algebra R A] :
Prop

An algebra is integral if every element of the extension is integral over the base ring

Equations
theorem ring_hom.is_integral_map {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] (f : R →+* S) {x : R} :
theorem is_integral_algebra_map {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] {x : R} :
theorem is_integral_of_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] (H : is_noetherian R A) (x : A) :
theorem is_integral_of_submodule_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) (H : is_noetherian R (S.to_submodule)) (x : A) (hx : x S) :
theorem is_integral_alg_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) {x : A} (hx : is_integral R x) :
theorem is_integral_of_is_scalar_tower {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x : B) (hx : is_integral R x) :
theorem is_integral_of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (T : set R) [is_subring T] (hx : is_integral T x) :
theorem is_integral_algebra_map_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] {x : A} (hAB : function.injective (algebra_map A B)) :
theorem is_integral_iff_is_integral_closure_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {r : A} :
theorem fg_adjoin_singleton_of_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : A) (hx : is_integral R x) :
theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {s : set A} (hfs : s.finite) (his : ∀ (x : A), x sis_integral R x) :
theorem is_integral_of_mem_of_fg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) (HS : S.to_submodule.fg) (x : A) (hx : x S) :
theorem ring_hom.is_integral_of_mem_closure {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y z : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) (hz : z ring.closure {x, y}) :
theorem is_integral_of_mem_closure {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y z : A} (hx : is_integral R x) (hy : is_integral R y) (hz : z ring.closure {x, y}) :
theorem ring_hom.is_integral_zero {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) :
theorem is_integral_zero {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
theorem ring_hom.is_integral_one {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) :
theorem is_integral_one {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :
theorem ring_hom.is_integral_add {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :
theorem is_integral_add {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :
is_integral R (x + y)
theorem ring_hom.is_integral_neg {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x : S} (hx : f.is_integral_elem x) :
theorem is_integral_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (hx : is_integral R x) :
theorem ring_hom.is_integral_sub {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :
theorem is_integral_sub {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :
is_integral R (x - y)
theorem ring_hom.is_integral_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :
theorem is_integral_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :
is_integral R (x * y)
def integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

The integral closure of R in an R-algebra A.

Equations
theorem mem_integral_closure_iff_mem_fg (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] {r : A} :
theorem integral_closure_map_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A ≃ₐ[R] B) :

Mapping an integral closure along an alg_equiv gives the integral closure.

theorem integral_closure.is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : (integral_closure R A)) :
theorem ring_hom.is_integral_of_is_integral_mul_unit {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (x y : S) (r : R) (hr : (f r) * y = 1) (hx : f.is_integral_elem (x * y)) :
theorem is_integral_of_is_integral_mul_unit {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} {r : R} (hr : ((algebra_map R A) r) * y = 1) (hx : is_integral R (x * y)) :
theorem is_integral_of_mem_closure' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (G : set A) (hG : ∀ (x : A), x Gis_integral R x) (x : A) (H : x subring.closure G) :

Generalization of is_integral_of_mem_closure bootstrapped up from that lemma

theorem is_integral_of_mem_closure'' {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {f : R →+* S} (G : set S) (hG : ∀ (x : S), x Gf.is_integral_elem x) (x : S) (H : x subring.closure G) :
theorem is_integral_trans_aux {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] (x : B) {p : polynomial A} (pmonic : p.monic) (hp : (polynomial.aeval x) p = 0) :
theorem is_integral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (A_int : algebra.is_integral R A) (x : B) (hx : is_integral A x) :

If A is an R-algebra all of whose elements are integral over R, and x is an element of an A-algebra that is integral over A, then x is integral over R.

theorem algebra.is_integral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (hA : algebra.is_integral R A) (hB : algebra.is_integral A B) :

If A is an R-algebra all of whose elements are integral over R, and B is an A-algebra all of whose elements are integral over A, then all elements of B are integral over R.

theorem ring_hom.is_integral_trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (hf : f.is_integral) (hg : g.is_integral) :
theorem ring_hom.is_integral_of_surjective {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective f) :
theorem is_integral_of_surjective {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (h : function.surjective (algebra_map R A)) :
theorem is_integral_tower_bot_of_is_integral {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (H : function.injective (algebra_map A B)) {x : A} (h : is_integral R ((algebra_map A B) x)) :

If R → A → B is an algebra tower with A → B injective, then if the entire tower is an integral extension so is R → A

theorem ring_hom.is_integral_tower_bot_of_is_integral {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (hg : function.injective g) (hfg : (g.comp f).is_integral) :
theorem is_integral_tower_bot_of_is_integral_field {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [field A] [comm_ring B] [nontrivial B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] {x : A} (h : is_integral R ((algebra_map A B) x)) :
theorem ring_hom.is_integral_elem_of_is_integral_elem_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) {x : T} (h : (g.comp f).is_integral_elem x) :
theorem ring_hom.is_integral_tower_top_of_is_integral {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (h : (g.comp f).is_integral) :
theorem is_integral_tower_top_of_is_integral {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] {x : B} (h : is_integral R x) :

If R → A → B is an algebra tower, then if the entire tower is an integral extension so is A → B.

theorem ring_hom.is_integral_quotient_of_is_integral {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal S} (hf : f.is_integral) :
theorem is_integral_quotient_of_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {I : ideal A} (hRA : algebra.is_integral R A) :
theorem is_integral_quotient_map_iff {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal S} :
theorem is_field_of_is_integral_of_is_field {R : Type u_1} {S : Type u_2} [integral_domain R] [integral_domain S] [algebra R S] (H : algebra.is_integral R S) (hRS : function.injective (algebra_map R S)) (hS : is_field S) :

If the integral extension R → S is injective, and S is a field, then R is also a field.

theorem integral_closure_idem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :