English
If R → A and S → B form a tower with A integral over R and C integral closure, then C is integral over A and B over R; the tower_top principle for integral closures.
Русский
Если R → A и S → B образуют башню, причём A интегрально над R, то C интегрально над A и B над R; принцип tower_top для интегральных замыканий.
LaTeX
$$$IsIntegralClosure C A B$$$
Lean4
/-- 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 tower_top {B C : Type*} [CommSemiring C] [CommRing B] [Algebra R B] [Algebra A B] [Algebra C B]
[IsScalarTower R A B] [IsIntegralClosure C R B] [Algebra.IsIntegral R A] : IsIntegralClosure C A B :=
⟨IsIntegralClosure.algebraMap_injective _ R _, fun hx =>
(IsIntegralClosure.isIntegral_iff).mp (isIntegral_trans (R := R) _ hx), fun hx =>
((IsIntegralClosure.isIntegral_iff (R := R)).mpr hx).tower_top⟩
