# mathlibdocumentation

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.

• ring_hom.is_integral_elem (f : R →+* A) (x : A) : x is integral with respect to the map f,

• is_integral (x : A) : x is integral over R, i.e., is a root of a monic polynomial with coefficients in R.

• integral_closure R A : the integral closure of R in A, regarded as a sub-R-algebra of A.
def ring_hom.is_integral_elem {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] :
(R →+* A)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_2} [comm_ring R] [ring A] :
(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_2} [comm_ring R] [ring A] [ A] :
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_2) [comm_ring R] [ring A] [ A] :
Prop

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

Equations
theorem is_integral_algebra_map {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {x : R} :
( A) x)

theorem is_integral_of_noetherian {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] (H : A) (x : A) :
x

theorem is_integral_of_submodule_noetherian {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] (S : A) (H : S) (x : A) :
x S x

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] [ A] [ B] (f : A →ₐ[R] B) {x : A} :
x (f 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] [ A] [ B] [ B] [ B] (x : B) :
x x

theorem is_integral_of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (T : set R) [is_subring T] :
x x

theorem is_integral_iff_is_integral_closure_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {r : A} :
r ∃ (s : set R), s.finite r

theorem fg_adjoin_singleton_of_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : A) :
x {x}).fg

theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {s : set A} :
s.finite(∀ (x : A), x s x) s).fg

theorem is_integral_of_mem_of_fg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (S : A) (HS : S.fg) (x : A) :
x S x

theorem is_integral_of_mem_closure {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x y z : A} :
x yz ring.closure {x, y} z

theorem is_integral_zero {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
0

theorem is_integral_one {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
1

theorem is_integral_add {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x y : A} :
x y (x + y)

theorem is_integral_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} :
x (-x)

theorem is_integral_sub {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x y : A} :
x y (x - y)

theorem is_integral_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x y : A} :
x y (x * y)

def integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
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] [ A] {r : A} :
r ∃ (M : A), M.fg r M

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] [ A] [ B] (f : A ≃ₐ[R] B) :
A).map f =

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] [ A] (x : A)) :
x

theorem is_integral_of_is_integral_mul_unit {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x y : A} {r : R} :
( A) r) * y = 1 (x * y) x

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] [ B] [ B] (x : B) {p : polynomial A} :

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] [ B] [ B] [ A] [ B] (A_int : A) (x : B) :
x 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] [ B] [ B] [ 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 is_integral_of_surjective {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ 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] [ B] [ B] [ A] [ B] (H : function.injective B)) {x : A} :
( B) x) 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 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] [ A] [ B] [ B] [ B] {x : A} :
( B) x) x

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] [ B] [ B] [ A] [ B] {x : B} :
x x

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

theorem is_integral_quotient_of_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {I : ideal A} :
I.quotient

theorem is_field_of_is_integral_of_is_field {R : Type u_1} {S : Type u_2} [ 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] [ A] :

@[instance]
def integral_closure.integral_domain {R : Type u_1} {S : Type u_2} [comm_ring R] [ S] :

Equations