tower_top — Mathlib

English

Let T/S/R be a tower of algebras; if T is integral over R, then T is integral over S.

Русский

Пусть T/S/R образуют башню алгебр; если T интегральна над R, то T интегральна над S.

LaTeX

$$$[\\text{Algebra R S}]\\,[\\text{Algebra R T}]\\,[\\text{Algebra S T}]\\,[\\text{IsScalarTower } R S T] \\;\\&\\; (\\text{Algebra.IsIntegral } R T) \\Rightarrow (\\text{Algebra.IsIntegral } S T)$$$

Lean4

/-- Let `T / S / R` be a tower of algebras, `T` is an integral `R`-algebra, then it is integral
  as an `S`-algebra. -/
theorem tower_top [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [h : Algebra.IsIntegral R T] :
    Algebra.IsIntegral S T where
  isIntegral := by
    apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)
    rw [← IsScalarTower.algebraMap_eq R S T]
    exact h.isIntegral

Похожие утверждения