mathlib3documentation

ring_theory.integral_closure

Integral closure of a subring. #

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

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_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 : R[X] 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] [ 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 : R[X]. Equivalently, the element is integral over R with respect to the induced algebra_map

Equations
@[protected]
def algebra.is_integral (R : Type u_1) (A : Type u_3) [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 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] [ A] {x : R} :
( A) x)
theorem is_integral_of_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [ A] (H : A) (x : A) :
x
theorem is_integral_of_submodule_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [ A] (S : A) (H : ) (x : A) (hx : x S) :
x
theorem map_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {B : Type u_3} {C : Type u_4} {F : Type u_5} [ring B] [ring C] [ B] [ B] [ C] [ B] [ C] [ C] {b : B} [ B C] (f : F) (hb : b) :
(f b)
theorem is_integral_map_of_comp_eq_of_is_integral {R : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [comm_ring R] [comm_ring S] [comm_ring T] [comm_ring U] [ S] [ U] (φ : R →+* T) (ψ : S →+* U) (h : U).comp φ = ψ.comp S)) {a : S} (ha : a) :
(ψ a)
theorem is_integral_alg_hom_iff {R : Type u_1} [comm_ring R] {A : Type u_2} {B : Type u_3} [ring A] [ring B] [ A] [ B] (f : A →ₐ[R] B) (hf : function.injective f) {x : A} :
(f x) x
@[simp]
theorem is_integral_alg_equiv {R : Type u_1} [comm_ring R] {A : Type u_2} {B : Type u_3} [ring A] [ring B] [ A] [ B] (f : A ≃ₐ[R] B) {x : A} :
(f x) 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} (hx : x) :
x
theorem map_is_integral_int {B : Type u_1} {C : Type u_2} {F : Type u_3} [ring B] [ring C] {b : B} [ C] (f : F) (hb : b) :
(f b)
theorem is_integral_of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (T : subring R) (hx : x) :
x
theorem is_integral.algebra_map {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 : A} (h : x) :
( B) 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] [ A] [ B] [ B] [ B] {x : A} (hAB : function.injective B)) :
( B) 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
theorem fg_adjoin_singleton_of_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (x : A) (hx : x) :
theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {s : set A} (hfs : s.finite) (his : (x : A), x s x) :
theorem is_noetherian_adjoin_finset {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (s : finset A) (hs : (x : A), x s x) :
s)
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 : .fg) (x : A) (hx : x S) :
x

If S is a sub-R-algebra of A and S is finitely-generated as an R-module, then all elements of S are integral over R.

theorem module.End.is_integral {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] [ M] :
M)
theorem is_integral_of_smul_mem_submodule {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {M : Type u_3} [ M] [ M] [ M] (N : M) (hN : N ) (hN' : N.fg) (x : A) (hx : (n : M), n N x n N) :
x

Suppose A is an R-algebra, M is an A-module such that a • m ≠ 0 for all non-zero a and m. If x : A fixes a nontrivial f.g. R-submodule N of M, then x is R-integral.

theorem ring_hom.finite.to_is_integral {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] {f : R →+* S} (h : f.finite) :
theorem ring_hom.is_integral.of_finite {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] {f : R →+* S} (h : f.finite) :

Alias of ring_hom.finite.to_is_integral.

theorem ring_hom.is_integral.to_finite {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] {f : R →+* S} (h : f.is_integral) (h' : f.finite_type) :
theorem ring_hom.finite.of_is_integral_of_finite_type {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] {f : R →+* S} (h : f.is_integral) (h' : f.finite_type) :

Alias of ring_hom.is_integral.to_finite.

theorem ring_hom.finite_iff_is_integral_and_finite_type {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] {f : R →+* S} :

finite = integral + finite type

theorem algebra.is_integral.finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (h : A) [h' : A] :
theorem algebra.is_integral.of_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] [h : A] :
theorem algebra.finite_iff_is_integral_and_finite_type {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :

finite = integral + finite type

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 subring.closure {x, y}) :
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} (hx : x) (hy : y) (hz : z subring.closure {x, y}) :
z
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] [ A] :
0
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] [ A] :
1
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] [ A] {x y : A} (hx : x) (hy : y) :
(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] [ A] {x : A} (hx : x) :
(-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] [ A] {x y : A} (hx : x) (hy : y) :
(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] [ A] {x y : A} (hx : x) (hy : y) :
(x * y)
theorem is_integral_smul {R : Type u_1} {A : Type u_2} {S : Type u_4} [comm_ring R] [comm_ring A] [comm_ring S] [ A] [ A] [ S] [ A] {x : A} (r : R) (hx : x) :
(r x)
theorem is_integral_of_pow {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} {n : } (hn : 0 < n) (hx : (x ^ n)) :
x
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
Instances for ↥integral_closure
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), r M
theorem adjoin_le_integral_closure {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (hx : x) :
{x}
theorem le_integral_closure_iff_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {S : A} :
S
theorem is_integral_sup {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {S T : A} :
(S T)
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) =

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 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] [ A] {x y : A} {r : R} (hr : A) r * y = 1) (hx : (x * y)) :
x
theorem is_integral_of_mem_closure' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (G : set A) (hG : (x : A), x G x) (x : A) (H : x ) :
x

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 G ) (x : S) (H : x ) :
theorem is_integral.pow {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (h : x) (n : ) :
(x ^ n)
theorem is_integral.nsmul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (h : x) (n : ) :
(n x)
theorem is_integral.zsmul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} (h : x) (n : ) :
(n x)
theorem is_integral.multiset_prod {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {s : multiset A} (h : (x : A), x s x) :
s.prod
theorem is_integral.multiset_sum {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {s : multiset A} (h : (x : A), x s x) :
s.sum
theorem is_integral.prod {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {α : Type u_3} {s : finset α} (f : α A) (h : (x : α), x s (f x)) :
(s.prod (λ (x : α), f x))
theorem is_integral.sum {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {α : Type u_3} {s : finset α} (f : α A) (h : (x : α), x s (f x)) :
(s.sum (λ (x : α), f x))
theorem is_integral.det {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {n : Type u_3} [fintype n] [decidable_eq n] {M : n A} (h : (i j : n), (M i j)) :
M.det
@[simp]
theorem is_integral.pow_iff {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {x : A} {n : } (hn : 0 < n) :
(x ^ n) x
theorem is_integral.tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (x : A) {y : B} (h : y) :
(x ⊗ₜ[R] y)
noncomputable def normalize_scale_roots {R : Type u_1} [comm_ring R] (p : polynomial R) :

The monic polynomial whose roots are p.leading_coeff * x for roots x of p.

Equations
theorem normalize_scale_roots_support {R : Type u_1} [comm_ring R] (p : polynomial R) :
theorem normalize_scale_roots_degree {R : Type u_1} [comm_ring R] (p : polynomial R) :
theorem normalize_scale_roots_eval₂_leading_coeff_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (p : polynomial R) (h : 1 p.nat_degree) (f : R →+* S) (x : S) :
theorem normalize_scale_roots_monic {R : Type u_1} [comm_ring R] (p : polynomial R) (h : p 0) :
theorem ring_hom.is_integral_elem_leading_coeff_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (p : polynomial R) (x : S) (h : p = 0) :

Given a p : R[X] and a x : S such that p.eval₂ f x = 0, f p.leading_coeff * x is integral.

theorem is_integral_leading_coeff_smul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (p : polynomial R) (x : S) [ S] (h : p = 0) :

Given a p : R[X] and a root x : S, then p.leading_coeff • x : S is integral over R.

@[class]
structure is_integral_closure (A : Type u_1) (R : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring B] [ B] [ B] :
Prop
• algebra_map_injective :
• is_integral_iff : {x : B}, x (y : A), B) y = x

is_integral_closure A R B is the characteristic predicate stating A is the integral closure of R in B, i.e. that an element of B is integral over R iff it is an element of (the image of) A.

Instances of this typeclass
@[protected, instance]
def integral_closure.is_integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [ A] :
A
@[protected]
theorem is_integral_closure.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] [ B] [ A] [ B] (x : A) :
x
theorem is_integral_closure.is_integral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] [ A] [ B] :
theorem is_integral_closure.no_zero_smul_divisors (R : Type u_1) {A : Type u_2} (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] [ A] [ B]  :
noncomputable def is_integral_closure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (x : B) (hx : x) :
A

If x : B is integral over R, then it is an element of the integral closure of R in B.

Equations
@[simp]
theorem is_integral_closure.algebra_map_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (x : B) (hx : x) :
B) hx) = x
@[simp]
theorem is_integral_closure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (h : 1 := is_integral_one) :
= 1
@[simp]
theorem is_integral_closure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (h : 0 := is_integral_zero) :
= 0
@[simp]
theorem is_integral_closure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (x y : B) (hx : x) (hy : y) :
(x + y) _ = hx + hy
@[simp]
theorem is_integral_closure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (x y : B) (hx : x) (hy : y) :
(x * y) _ = hx * hy
@[simp]
theorem is_integral_closure.mk'_algebra_map {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] [ A] [ B] (x : R) (h : ( B) x) := is_integral_algebra_map) :
( B) x) h = A) x
noncomputable def is_integral_closure.lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] {S : Type u_4} [comm_ring S] [ S] [ B] [ B] [ A] [ B] (h : S) :

If B / S / R is a tower of ring extensions where S is integral over R, then S maps (uniquely) into an integral closure B / A / R.

Equations
@[simp]
theorem is_integral_closure.algebra_map_lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] {S : Type u_4} [comm_ring S] [ S] [ B] [ B] [ A] [ B] (h : S) (x : S) :
B) ( h) x) = B) x
noncomputable def is_integral_closure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (A' : Type u_4) [comm_ring A'] [algebra A' B] [ B] [ A] [ A'] [ B] [ A' B] :
A ≃ₐ[R] A'

Integral closures are all isomorphic to each other.

Equations
• A' = _) _ _
@[simp]
theorem is_integral_closure.algebra_map_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [ B] [ B] [ B] (A' : Type u_4) [comm_ring A'] [algebra A' B] [ B] [ A] [ A'] [ B] [ A' B] (x : A) :
(algebra_map A' B) ( A') x) = B) 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} (pmonic : p.monic) (hp : 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] [ B] [ B] [ A] [ B] (A_int : A) (x : B) (hx : 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] (hA : A) (hB : 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] [ A] (h : function.surjective 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} (h : ( 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 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] [ A] [ B] [ B] [ B] {x : A} (h : ( B) x)) :
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] [ B] [ B] [ A] [ B] {x : B} (h : x) :
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] [ A] {I : ideal A} (hRA : 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} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S] [ S] (H : S) (hRS : function.injective 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 is_field_of_is_integral_of_is_field' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain S] [ S] (H : S) (hR : is_field R) :
theorem algebra.is_integral.is_field_iff_is_field {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S] [ S] (H : S) (hRS : function.injective S)) :
theorem integral_closure_idem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] :
@[protected, instance]
def integral_closure.is_domain {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain S] [ S] :
theorem roots_mem_integral_closure {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain S] [ S] {f : polynomial R} (hf : f.monic) {a : S} (ha : a (polynomial.map S) f).roots) :
a