# 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 CommRing and let A be an R-algebra.

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

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

• integralClosure R A : the integral closure of R in A, regarded as a sub-R-algebra of A.

def RingHom.IsIntegralElem {R : Type u_1} {A : Type u_3} [] [Ring A] (f : R →+* A) (x : A) :

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
Instances For
def RingHom.IsIntegral {R : Type u_1} {A : Type u_3} [] [Ring A] (f : R →+* A) :

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

Equations
• = ∀ (x : A),
Instances For
def IsIntegral (R : Type u_1) {A : Type u_3} [] [Ring A] [Algebra R A] (x : A) :

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 algebraMap

Equations
Instances For
def Algebra.IsIntegral (R : Type u_1) (A : Type u_3) [] [Ring A] [Algebra R A] :

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

Equations
• = ∀ (x : A),
Instances For
theorem RingHom.isIntegralElem_map {R : Type u_1} {S : Type u_2} [] [Ring S] (f : R →+* S) {x : R} :
theorem isIntegral_algebraMap {R : Type u_1} {A : Type u_3} [] [Ring A] [Algebra R A] {x : R} :
IsIntegral R (() x)
theorem IsIntegral.map {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {B : Type u_5} {C : Type u_6} {F : Type u_7} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C] [] [Algebra A C] [] {b : B} [FunLike F B C] [AlgHomClass F A B C] (f : F) (hb : ) :
IsIntegral R (f b)
theorem IsIntegral.map_of_comp_eq {R : Type u_5} {S : Type u_6} {T : Type u_7} {U : Type u_8} [] [Ring S] [] [Ring U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U) (h : RingHom.comp () φ = RingHom.comp ψ ()) {a : S} (ha : ) :
IsIntegral T (ψ a)
theorem isIntegral_algHom_iff {R : Type u_1} [] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ) {x : A} :
IsIntegral R (f x)
theorem Algebra.IsIntegral.of_injective {R : Type u_1} [] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ) (h : ) :
@[simp]
theorem isIntegral_algEquiv {R : Type u_1} [] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {x : A} :
IsIntegral R (f x)
theorem IsIntegral.tower_top {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra R A] [Algebra R B] [Algebra A B] [] {x : B} (hx : ) :

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

theorem map_isIntegral_int {B : Type u_5} {C : Type u_6} {F : Type u_7} [Ring B] [Ring C] {b : B} [FunLike F B C] [RingHomClass F B C] (f : F) (hb : ) :
theorem IsIntegral.of_subring {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (T : ) (hx : IsIntegral (T) x) :
theorem IsIntegral.algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra R A] [Algebra R B] [Algebra A B] [] {x : A} (h : ) :
IsIntegral R (() x)
theorem isIntegral_algebraMap_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra R A] [Algebra R B] [Algebra A B] [] {x : A} (hAB : Function.Injective ()) :
IsIntegral R (() x)
theorem isIntegral_iff_isIntegral_closure_finite {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {r : B} :
∃ (s : Set R), IsIntegral (()) r
theorem Submodule.span_range_natDegree_eq_adjoin {R : Type u_5} {A : Type u_6} [] [] [Algebra R A] {x : A} {f : } (hf : ) (hfx : () f = 0) :
Submodule.span R (Finset.image (fun (x_1 : ) => x ^ x_1) ) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
theorem IsIntegral.fg_adjoin_singleton {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (hx : ) :
theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {s : Set A} (hfs : ) (his : xs, ) :
Submodule.FG (Subalgebra.toSubmodule ())
theorem isNoetherian_adjoin_finset {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] [] (s : ) (hs : xs, ) :
IsNoetherian R ()
theorem Module.End.isIntegral {R : Type u_1} [] {M : Type u_5} [] [Module R M] [] :
theorem IsIntegral.of_finite (R : Type u_1) {B : Type u_3} [] [Ring B] [Algebra R B] [] (x : B) :
theorem Algebra.IsIntegral.of_finite (R : Type u_1) (B : Type u_3) [] [Ring B] [Algebra R B] [] :
theorem IsIntegral.of_mem_of_fg {R : Type u_1} [] {A : Type u_5} [Ring A] [Algebra R A] (S : ) (HS : Submodule.FG (Subalgebra.toSubmodule S)) (x : A) (hx : x S) :

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 isIntegral_of_noetherian {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] :
∀ (x : B),
theorem isIntegral_of_submodule_noetherian {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] (S : ) (H : IsNoetherian R (Subalgebra.toSubmodule S)) (x : B) (hx : x S) :
theorem isIntegral_of_smul_mem_submodule {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {M : Type u_5} [] [Module R M] [Module A M] [] [] (N : ) (hN : N ) (hN' : ) (x : A) (hx : nN, x n N) :

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 RingHom.Finite.to_isIntegral {R : Type u_1} {S : Type u_4} [] [] {f : R →+* S} (h : ) :
theorem RingHom.IsIntegral.of_finite {R : Type u_1} {S : Type u_4} [] [] {f : R →+* S} (h : ) :

Alias of RingHom.Finite.to_isIntegral.

theorem Algebra.IsIntegral.finite {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (h : ) [h' : ] :

The Kurosh problem asks to show that this is still true when A is not necessarily commutative and R is a field, but it has been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a finitely generated algebraic (= integral) algebra over a field to be finite dimensional.

theorem Algebra.finite_iff_isIntegral_and_finiteType {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :

finite = integral + finite type

theorem RingHom.IsIntegral.to_finite {R : Type u_1} {S : Type u_4} [] [] {f : R →+* S} (h : ) (h' : ) :
theorem RingHom.Finite.of_isIntegral_of_finiteType {R : Type u_1} {S : Type u_4} [] [] {f : R →+* S} (h : ) (h' : ) :

Alias of RingHom.IsIntegral.to_finite.

theorem RingHom.finite_iff_isIntegral_and_finiteType {R : Type u_1} {S : Type u_4} [] [] {f : R →+* S} :

finite = integral + finite type

theorem RingHom.IsIntegralElem.of_mem_closure {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {x : S} {y : S} {z : S} (hx : ) (hy : ) (hz : z Subring.closure {x, y}) :
theorem IsIntegral.of_mem_closure {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} {y : A} {z : A} (hx : ) (hy : ) (hz : z Subring.closure {x, y}) :
theorem RingHom.isIntegralElem_zero {R : Type u_1} {B : Type u_3} [] [Ring B] (f : R →+* B) :
theorem isIntegral_zero {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] :
theorem RingHom.isIntegralElem_one {R : Type u_1} {B : Type u_3} [] [Ring B] (f : R →+* B) :
theorem isIntegral_one {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] :
theorem RingHom.IsIntegralElem.add {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {x : S} {y : S} (hx : ) (hy : ) :
theorem IsIntegral.add {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} {y : A} (hx : ) (hy : ) :
IsIntegral R (x + y)
theorem RingHom.IsIntegralElem.neg {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {x : S} (hx : ) :
theorem IsIntegral.neg {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (hx : ) :
theorem RingHom.IsIntegralElem.sub {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {x : S} {y : S} (hx : ) (hy : ) :
theorem IsIntegral.sub {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} {y : A} (hx : ) (hy : ) :
IsIntegral R (x - y)
theorem RingHom.IsIntegralElem.mul {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {x : S} {y : S} (hx : ) (hy : ) :
theorem IsIntegral.mul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} {y : A} (hx : ) (hy : ) :
IsIntegral R (x * y)
theorem IsIntegral.smul {B : Type u_3} {S : Type u_4} [Ring B] {R : Type u_5} [] [] [Algebra R B] [Algebra S B] [Algebra R S] [] {x : B} (r : R) (hx : ) :
IsIntegral S (r x)
theorem IsIntegral.of_pow {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} {n : } (hn : 0 < n) (hx : IsIntegral R (x ^ n)) :
def integralClosure (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem mem_integralClosure_iff_mem_fg (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] {r : A} :
r ∃ (M : ), Submodule.FG (Subalgebra.toSubmodule M) r M
theorem adjoin_le_integralClosure {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} (hx : ) :
theorem le_integralClosure_iff_isIntegral {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {S : } :
S
theorem Algebra.isIntegral_sup {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {S : } {T : } :
theorem integralClosure_map_algEquiv {R : Type u_1} {A : Type u_2} {S : Type u_4} [] [] [] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :
Subalgebra.map (f) () =

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

def AlgHom.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [] [] [] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) :
() →ₐ[R] ()

An AlgHom between two rings restrict to an AlgHom between the integral closures inside them.

Equations
Instances For
@[simp]
theorem AlgHom.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [] [] [] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) (x : ()) :
() = f x
def AlgEquiv.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [] [] [] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :
() ≃ₐ[R] ()

An AlgEquiv between two rings restrict to an AlgEquiv between the integral closures inside them.

Equations
Instances For
@[simp]
theorem AlgEquiv.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [] [] [] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) (x : ()) :
() = f x
theorem integralClosure.isIntegral {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (x : ()) :
theorem IsIntegral.of_mul_unit {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} {y : B} {r : R} (hr : () r * y = 1) (hx : IsIntegral R (x * y)) :
theorem RingHom.IsIntegralElem.of_mul_unit {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) (x : S) (y : S) (r : R) (hr : f r * y = 1) (hx : RingHom.IsIntegralElem f (x * y)) :
theorem IsIntegral.of_mem_closure' {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (G : Set A) (hG : xG, ) (x : A) :

Generalization of IsIntegral.of_mem_closure bootstrapped up from that lemma

theorem IsIntegral.of_mem_closure'' {R : Type u_1} [] {S : Type u_5} [] {f : R →+* S} (G : Set S) (hG : xG, ) (x : S) :
theorem IsIntegral.pow {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (h : ) (n : ) :
IsIntegral R (x ^ n)
theorem IsIntegral.nsmul {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (h : ) (n : ) :
IsIntegral R (n x)
theorem IsIntegral.zsmul {R : Type u_1} {B : Type u_3} [] [Ring B] [Algebra R B] {x : B} (h : ) (n : ) :
IsIntegral R (n x)
theorem IsIntegral.multiset_prod {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {s : } (h : xs, ) :
theorem IsIntegral.multiset_sum {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {s : } (h : xs, ) :
theorem IsIntegral.prod {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {α : Type u_5} {s : } (f : αA) (h : xs, IsIntegral R (f x)) :
IsIntegral R (Finset.prod s fun (x : α) => f x)
theorem IsIntegral.sum {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {α : Type u_5} {s : } (f : αA) (h : xs, IsIntegral R (f x)) :
IsIntegral R (Finset.sum s fun (x : α) => f x)
theorem IsIntegral.det {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {n : Type u_5} [] [] {M : Matrix n n A} (h : ∀ (i j : n), IsIntegral R (M i j)) :
@[simp]
theorem IsIntegral.pow_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {x : A} {n : } (hn : 0 < n) :
IsIntegral R (x ^ n)
theorem IsIntegral.tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra R A] [Algebra R B] (x : A) {y : B} (h : ) :
noncomputable def normalizeScaleRoots {R : Type u_1} [] (p : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow {R : Type u_1} [] (p : ) (i : ) (hp : ) :
=
theorem normalizeScaleRoots_support {R : Type u_1} [] (p : ) :
theorem normalizeScaleRoots_degree {R : Type u_1} [] (p : ) :
theorem normalizeScaleRoots_eval₂_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [] [] (p : ) (h : ) (f : R →+* S) (x : S) :
Polynomial.eval₂ f ( * x) = ^ () *
theorem normalizeScaleRoots_monic {R : Type u_1} [] (p : ) (h : p 0) :
theorem RingHom.isIntegralElem_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) (p : ) (x : S) (h : = 0) :

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

theorem isIntegral_leadingCoeff_smul {R : Type u_1} {S : Type u_4} [] [] (p : ) (x : S) [Algebra R S] (h : () p = 0) :

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

class IsIntegralClosure (A : Type u_1) (R : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] :

IsIntegralClosure 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
instance integralClosure.isIntegralClosure (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :
IsIntegralClosure (()) R A
Equations
• =
theorem IsIntegralClosure.algebraMap_injective (A : Type u_1) (R : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] :
theorem IsIntegralClosure.isIntegral (R : Type u_1) {A : Type u_2} (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] [Algebra R A] [] (x : A) :
theorem IsIntegralClosure.isIntegral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] [Algebra R A] [] :
theorem IsIntegralClosure.noZeroSMulDivisors (R : Type u_1) {A : Type u_2} (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] [Algebra R A] [] [] :
noncomputable def IsIntegralClosure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (x : B) (hx : ) :
A

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

Equations
Instances For
@[simp]
theorem IsIntegralClosure.algebraMap_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (x : B) (hx : ) :
() () = x
@[simp]
theorem IsIntegralClosure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (h : optParam () ) :
= 1
@[simp]
theorem IsIntegralClosure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (h : optParam () ) :
= 0
theorem IsIntegralClosure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (x : B) (y : B) (hx : ) (hy : ) :
IsIntegralClosure.mk' A (x + y) = +
theorem IsIntegralClosure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] (x : B) (y : B) (hx : ) (hy : ) :
IsIntegralClosure.mk' A (x * y) = *
@[simp]
theorem IsIntegralClosure.mk'_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R B] [Algebra A B] [] [Algebra R A] [] (x : R) (h : optParam (IsIntegral R (() x)) ) :
IsIntegralClosure.mk' A (() x) h = () x
noncomputable def IsIntegralClosure.lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] {S : Type u_4} [] [Algebra R S] [Algebra S B] [] [Algebra R A] [] (h : ) :

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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem IsIntegralClosure.algebraMap_lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] {S : Type u_4} [] [Algebra R S] [Algebra S B] [] [Algebra R A] [] (h : ) (x : S) :
() (() x) = () x
noncomputable def IsIntegralClosure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] (A' : Type u_4) [CommRing A'] [Algebra A' B] [] [Algebra R A] [Algebra R A'] [] [IsScalarTower R A' B] :
A ≃ₐ[R] A'

Integral closures are all isomorphic to each other.

Equations
Instances For
@[simp]
theorem IsIntegralClosure.algebraMap_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [] [Algebra R B] [Algebra A B] [] (A' : Type u_4) [CommRing A'] [Algebra A' B] [] [Algebra R A] [Algebra R A'] [] [IsScalarTower R A' B] (x : A) :
(algebraMap A' B) (() x) = () x
theorem isIntegral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [] (A_int : ) (x : B) (hx : ) :

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.IsIntegral.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [] (hA : ) (hB : ) :

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 RingHom.IsIntegral.trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* S) (g : S →+* T) (hf : ) (hg : ) :
theorem IsIntegralClosure.tower_top {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {B : Type u_6} {C : Type u_7} [] [] [Algebra R B] [Algebra A B] [Algebra C B] [] [] (hRA : ) :

If R → A → B is an algebra tower, C is the integral closure of R in B and A is integral over R, then C is the integral closure of A in B.

theorem RingHom.isIntegral_of_surjective {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) (hf : ) :
theorem Algebra.isIntegral_of_surjective {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (h : ) :
theorem IsIntegral.tower_bot {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [] (H : Function.Injective ()) {x : A} (h : IsIntegral R (() 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 RingHom.IsIntegral.tower_bot {R : Type u_1} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* S) (g : S →+* T) (hg : ) (hfg : ) :
theorem IsIntegral.tower_bot_of_field {R : Type u_6} {A : Type u_7} {B : Type u_8} [] [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] {x : A} (h : IsIntegral R (() x)) :
theorem RingHom.isIntegralElem.of_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* S) (g : S →+* T) {x : T} (h : ) :
theorem RingHom.IsIntegral.tower_top {R : Type u_1} {S : Type u_4} {T : Type u_5} [] [] [] (f : R →+* S) (g : S →+* T) (h : ) :
theorem RingHom.IsIntegral.quotient {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {I : } (hf : ) :
theorem Algebra.IsIntegral.quotient {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] {I : } (hRA : ) :
theorem isIntegral_quotientMap_iff {R : Type u_1} {S : Type u_4} [] [] (f : R →+* S) {I : } :
theorem isField_of_isIntegral_of_isField {R : Type u_6} {S : Type u_7} [] [] [Algebra R S] (H : ) (hRS : Function.Injective ()) (hS : ) :

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

theorem isField_of_isIntegral_of_isField' {R : Type u_6} {S : Type u_7} [] [] [] [Algebra R S] (H : ) (hR : ) :
theorem Algebra.IsIntegral.isField_iff_isField {R : Type u_6} {S : Type u_7} [] [] [] [Algebra R S] (H : ) (hRS : Function.Injective ()) :
theorem integralClosure_idem {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
integralClosure (()) A =
theorem roots_mem_integralClosure {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {f : } (hf : ) {a : S} (ha : a ) :
a