English
If R → A → B is an algebra tower and x is integral over R, then x is integral over A.
Русский
Если R → A → B — алгебраическая башня и x интегрально над R, то x интегрально над A.
LaTeX
$$$\\text{IsIntegral}_R(x) \\Rightarrow \\text{IsIntegral}_A(x)$$$
Lean4
/-- If `R → A → B` is an algebra tower,
then if the entire tower is an integral extension so is `A → B`. -/
theorem tower_top [Algebra A B] [IsScalarTower R A B] {x : B} (hx : IsIntegral R x) : IsIntegral A x :=
let ⟨p, hp, hpx⟩ := hx
⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩
/- If `R` and `T` are isomorphic commutative rings and `S` is an `R`-algebra and a `T`-algebra in
a compatible way, then an element `a ∈ S` is integral over `R` if and only if it is integral
over `T`. -/
