English
There is a consistent scalar tower linking R_p, S_p and T_p under prime-compliment localizations.
Русский
Существует согласованный каскад скалярных торов, связывающий R_p, S_p и T_p под локализациями primeCompl.
LaTeX
$$$\text IsScalarTower (R_p) (S_p) (T_p)$$$
Lean4
instance : IsScalarTower Rₚ Sₚ L :=
by
refine IsScalarTower.of_algebraMap_eq' <| IsLocalization.ringHom_ext P.primeCompl ?_
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq R Rₚ Sₚ, IsScalarTower.algebraMap_eq R S Sₚ, ←
RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq S Sₚ L, IsScalarTower.algebraMap_eq Rₚ K L, RingHom.comp_assoc, ←
IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
