English
If P is stable under base change, then a localization map is preserved under base change and localization.
Русский
Если P стабильно при базовом изменении, то локализационная карта сохраняется при базовом изменении и локализации.
LaTeX
$$$\\text{IsStableUnderBaseChange }P \\Rightarrow \\text{IsLocalization map under base change}$$$
Lean4
/-- Let `S` be an `R`-algebra and `Sᵣ` and `Rᵣ` be the respective localizations at a submonoid
`M` of `R`. If `P` is stable under base change and `P` holds for `algebraMap R S`, then
`P` holds for `algebraMap Rᵣ Sᵣ`. -/
theorem of_isLocalization [Algebra R S] [Algebra R Sᵣ] [Algebra Rᵣ Sᵣ] [IsScalarTower R S Sᵣ] [IsScalarTower R Rᵣ Sᵣ]
(M : Submonoid R) [IsLocalization M Rᵣ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ]
(h : P (algebraMap R S)) : P (algebraMap Rᵣ Sᵣ) :=
letI : Algebra.IsPushout R S Rᵣ Sᵣ := Algebra.isPushout_of_isLocalization M Rᵣ S Sᵣ
hP R S Rᵣ Sᵣ h
