Documentation

Mathlib.RingTheory.IntegralClosure

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.

def RingHom.IsIntegralElem {R : Type u_1} {A : Type u_3} [CommRing R] [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

Instances For
    def RingHom.IsIntegral {R : Type u_1} {A : Type u_3} [CommRing R] [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

    Instances For
      def IsIntegral (R : Type u_1) {A : Type u_3} [CommRing R] [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

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

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

        Instances For
          theorem RingHom.is_integral_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) {x : R} :
          theorem isIntegral_algebraMap {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {x : R} :
          IsIntegral R (↑(algebraMap R A) x)
          theorem isIntegral_of_noetherian {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (H : IsNoetherian R A) (x : A) :
          theorem isIntegral_of_submodule_noetherian {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (H : IsNoetherian R { x // x Subalgebra.toSubmodule S }) (x : A) (hx : x S) :
          theorem isIntegral_of_finite (K : Type u_1) {A : Type u_2} [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] (e : A) :
          theorem Algebra.isIntegral_of_finite (K : Type u_1) (A : Type u_2) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] :

          A field extension is integral if it is finite.

          theorem map_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [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] [IsScalarTower R A B] [Algebra A C] [IsScalarTower R A C] {b : B} [AlgHomClass F A B C] (f : F) (hb : IsIntegral R b) :
          IsIntegral R (f b)
          theorem isIntegral_map_of_comp_eq_of_isIntegral {R : Type u_5} {S : Type u_6} {T : Type u_7} {U : Type u_8} [CommRing R] [CommRing S] [CommRing T] [CommRing U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U) (h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)) {a : S} (ha : IsIntegral R a) :
          IsIntegral T (ψ a)
          theorem isIntegral_algHom_iff {R : Type u_1} [CommRing R] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} :
          IsIntegral R (f x) IsIntegral R x
          @[simp]
          theorem isIntegral_algEquiv {R : Type u_1} [CommRing R] {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) IsIntegral R x
          theorem isIntegral_of_isScalarTower {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] {x : B} (hx : IsIntegral R x) :
          theorem map_isIntegral_int {B : Type u_5} {C : Type u_6} {F : Type u_7} [Ring B] [Ring C] {b : B} [RingHomClass F B C] (f : F) (hb : IsIntegral b) :
          IsIntegral (f b)
          theorem isIntegral_ofSubring {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (T : Subring R) (hx : IsIntegral { x // x T } x) :
          theorem IsIntegral.algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] {x : A} (h : IsIntegral R x) :
          IsIntegral R (↑(algebraMap A B) x)
          theorem isIntegral_algebraMap_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] {x : A} (hAB : Function.Injective ↑(algebraMap A B)) :
          IsIntegral R (↑(algebraMap A B) x) IsIntegral R x
          theorem isIntegral_iff_isIntegral_closure_finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {r : A} :
          theorem FG_adjoin_singleton_of_integral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : A) (hx : IsIntegral R x) :
          Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {x}))
          theorem FG_adjoin_of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} (hfs : Set.Finite s) (his : ∀ (x : A), x sIsIntegral R x) :
          Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R s))
          theorem isNoetherian_adjoin_finset {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] (s : Finset A) (hs : ∀ (x : A), x sIsIntegral R x) :
          IsNoetherian R { x // x Algebra.adjoin R s }
          theorem isIntegral_of_mem_of_FG {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) (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_smul_mem_submodule {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors A M] (N : Submodule R M) (hN : N ) (hN' : Submodule.FG N) (x : A) (hx : ∀ (n : M), n Nx 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} [CommRing R] [CommRing S] {f : R →+* S} (h : RingHom.Finite f) :

          finite = integral + finite type

          theorem Algebra.IsIntegral.finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Algebra.IsIntegral R A) [h' : Algebra.FiniteType R A] :
          theorem Algebra.IsIntegral.of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [h : Module.Finite R A] :

          finite = integral + finite type

          theorem RingHom.is_integral_of_mem_closure {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} {z : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) (hz : z Subring.closure {x, y}) :
          theorem isIntegral_of_mem_closure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} {z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z Subring.closure {x, y}) :
          theorem RingHom.is_integral_zero {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) :
          theorem isIntegral_zero {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :
          theorem RingHom.is_integral_one {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) :
          theorem isIntegral_one {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :
          theorem RingHom.is_integral_add {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :
          theorem isIntegral_add {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
          IsIntegral R (x + y)
          theorem RingHom.is_integral_neg {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} (hx : RingHom.IsIntegralElem f x) :
          theorem isIntegral_neg {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (hx : IsIntegral R x) :
          theorem RingHom.is_integral_sub {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :
          theorem isIntegral_sub {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
          IsIntegral R (x - y)
          theorem RingHom.is_integral_mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :
          theorem isIntegral_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
          IsIntegral R (x * y)
          theorem isIntegral_smul {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra S A] [Algebra R S] [IsScalarTower R S A] {x : A} (r : R) (hx : IsIntegral S x) :
          IsIntegral S (r x)
          theorem isIntegral_of_pow {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {n : } (hn : 0 < n) (hx : IsIntegral R (x ^ n)) :
          def integralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :

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

          Instances For
            theorem mem_integralClosure_iff_mem_FG (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] {r : A} :
            r integralClosure R A M, Submodule.FG (Subalgebra.toSubmodule M) r M
            theorem adjoin_le_integralClosure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (hx : IsIntegral R x) :
            theorem le_integralClosure_iff_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} :
            theorem isIntegral_sup {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} :
            Algebra.IsIntegral R { x // x S T } Algebra.IsIntegral R { x // x S } Algebra.IsIntegral R { x // x T }
            theorem integralClosure_map_algEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

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

            theorem integralClosure.isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : { x // x integralClosure R A }) :
            theorem RingHom.isIntegral_of_isIntegral_mul_unit {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (x : S) (y : S) (r : R) (hr : f r * y = 1) (hx : RingHom.IsIntegralElem f (x * y)) :
            theorem isIntegral_of_isIntegral_mul_unit {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} {r : R} (hr : ↑(algebraMap R A) r * y = 1) (hx : IsIntegral R (x * y)) :
            theorem isIntegral_of_mem_closure' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (G : Set A) (hG : ∀ (x : A), x GIsIntegral R x) (x : A) :

            Generalization of isIntegral_of_mem_closure bootstrapped up from that lemma

            theorem isIntegral_of_mem_closure'' {R : Type u_1} [CommRing R] {S : Type u_5} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ (x : S), x GRingHom.IsIntegralElem f x) (x : S) :
            theorem IsIntegral.pow {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (h : IsIntegral R x) (n : ) :
            IsIntegral R (x ^ n)
            theorem IsIntegral.nsmul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (h : IsIntegral R x) (n : ) :
            IsIntegral R (n x)
            theorem IsIntegral.zsmul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (h : IsIntegral R x) (n : ) :
            IsIntegral R (n x)
            theorem IsIntegral.multiset_prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ (x : A), x sIsIntegral R x) :
            theorem IsIntegral.multiset_sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ (x : A), x sIsIntegral R x) :
            theorem IsIntegral.prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : αA) (h : ∀ (x : α), x sIsIntegral R (f x)) :
            IsIntegral R (Finset.prod s fun x => f x)
            theorem IsIntegral.sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : αA) (h : ∀ (x : α), x sIsIntegral R (f x)) :
            IsIntegral R (Finset.sum s fun x => f x)
            theorem IsIntegral.det {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {n : Type u_5} [Fintype n] [DecidableEq n] {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} [CommRing R] [CommRing A] [Algebra R A] {x : A} {n : } (hn : 0 < n) :
            theorem IsIntegral.tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (x : A) {y : B} (h : IsIntegral R y) :
            noncomputable def normalizeScaleRoots {R : Type u_1} [CommRing R] (p : Polynomial R) :

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

            Instances For
              theorem RingHom.isIntegralElem_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (p : Polynomial R) (x : S) (h : Polynomial.eval₂ f x p = 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} [CommRing R] [CommRing S] (p : Polynomial R) (x : S) [Algebra R S] (h : ↑(Polynomial.aeval x) 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) [CommRing R] [CommSemiring A] [CommRing B] [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) [CommRing R] [CommRing A] [Algebra R A] :
                theorem IsIntegralClosure.isIntegral (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : A) :
                theorem IsIntegralClosure.isIntegral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] :
                noncomputable def IsIntegralClosure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :
                A

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

                Instances For
                  @[simp]
                  theorem IsIntegralClosure.algebraMap_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :
                  ↑(algebraMap A B) (IsIntegralClosure.mk' A x hx) = x
                  @[simp]
                  theorem IsIntegralClosure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : optParam (IsIntegral R 1) (_ : IsIntegral R 1)) :
                  @[simp]
                  theorem IsIntegralClosure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : optParam (IsIntegral R 0) (_ : IsIntegral R 0)) :
                  theorem IsIntegralClosure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
                  theorem IsIntegralClosure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
                  @[simp]
                  theorem IsIntegralClosure.mk'_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : R) (h : optParam (IsIntegral R (↑(algebraMap R B) x)) (_ : IsIntegral R (↑(algebraMap R ((fun x => B) x)) x))) :
                  IsIntegralClosure.mk' A (↑(algebraMap R B) x) h = ↑(algebraMap R A) x
                  noncomputable def IsIntegralClosure.lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] (h : Algebra.IsIntegral R 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.

                  Instances For
                    @[simp]
                    theorem IsIntegralClosure.algebraMap_lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] (h : Algebra.IsIntegral R S) (x : S) :
                    ↑(algebraMap A B) (↑(IsIntegralClosure.lift A B h) x) = ↑(algebraMap S B) x
                    noncomputable def IsIntegralClosure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] :
                    A ≃ₐ[R] A'

                    Integral closures are all isomorphic to each other.

                    Instances For
                      @[simp]
                      theorem IsIntegralClosure.algebraMap_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] (x : A) :
                      ↑(algebraMap A' B) (↑(IsIntegralClosure.equiv R A B A') x) = ↑(algebraMap A B) x
                      theorem isIntegral_trans_aux {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra A B] [Algebra R B] (x : B) {p : Polynomial A} (pmonic : Polynomial.Monic p) (hp : ↑(Polynomial.aeval x) p = 0) :
                      theorem isIntegral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (A_int : Algebra.IsIntegral R A) (x : B) (hx : IsIntegral 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.isIntegral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (hA : Algebra.IsIntegral R A) (hB : Algebra.IsIntegral 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 RingHom.isIntegral_trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hf : RingHom.IsIntegral f) (hg : RingHom.IsIntegral g) :
                      theorem isIntegral_tower_bot_of_isIntegral {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (H : Function.Injective ↑(algebraMap A B)) {x : A} (h : IsIntegral R (↑(algebraMap 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 RingHom.isIntegral_tower_bot_of_isIntegral {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hg : Function.Injective g) (hfg : RingHom.IsIntegral (RingHom.comp g f)) :
                      theorem isIntegral_tower_bot_of_isIntegral_field {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R (↑(algebraMap A B) x)) :
                      theorem RingHom.isIntegralElem_of_isIntegralElem_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) {x : T} (h : RingHom.IsIntegralElem (RingHom.comp g f) x) :
                      theorem RingHom.isIntegral_tower_top_of_isIntegral {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (h : RingHom.IsIntegral (RingHom.comp g f)) :
                      theorem isIntegral_tower_top_of_isIntegral {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] {x : B} (h : IsIntegral R x) :

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

                      theorem isIntegral_quotient_of_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} (hRA : Algebra.IsIntegral R A) :
                      theorem isField_of_isIntegral_of_isField {R : Type u_6} {S : Type u_7} [CommRing R] [Nontrivial R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hRS : Function.Injective ↑(algebraMap R S)) (hS : IsField S) :

                      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} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hR : IsField R) :
                      theorem integralClosure_idem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :
                      theorem roots_mem_integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : Polynomial.Monic f) {a : S} (ha : a Polynomial.aroots f S) :