English
Let R ⟶ S ⟶ T be a tower of algebras with T nontrivial and torsion-free as an S-module. If T is integral over R, then S is integral over R.
Русский
Пусть R → S → T образуют цепь алгебр, T ненулевая и беззацепочная как S-модуль. Если T интегральна над R, то и S интегральна над R.
LaTeX
$$$(\\text{IsIntegral}(R,T)) \\wedge \\text{NoZeroSMulDivisors}(S,T) \\wedge \\text{Nontrivial}(T) \\wedge \\text{IsScalarTower}(R,S,T) \\Rightarrow \\text{IsIntegral}(R,S)$$$
Lean4
/-- Let `T / S / R` be a tower of algebras, `T` is non-trivial and is a torsion free `S`-module,
then if `T` is an integral `R`-algebra, then `S` is an integral `R`-algebra. -/
theorem tower_bot [Algebra R S] [Algebra R T] [Algebra S T] [NoZeroSMulDivisors S T] [Nontrivial T]
[IsScalarTower R S T] [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S where
isIntegral :=
by
apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T) (FaithfulSMul.algebraMap_injective S T)
rw [← IsScalarTower.algebraMap_eq R S T]
exact h.isIntegral
