English
Let M be a multiplicative submonoid of R, and S an R-algebra. After localizing R at M and S appropriately, the canonical algebra map from the localized base to the localized target coincides with the map induced by localizing the base algebra map R → S.
Русский
Пусть M — подмономиод в R, S — алгебра над R. После локализации R по M и соответствующей локализации S задаётся каноническое алгебраическое отображение между локализациями, которое совпадает с отображением, полученным путём локализации базового отображения R → S.
LaTeX
$$$\\operatorname{algebraMap}_{R_m S_m}(\\mathrm{localizationAlgebra}(M,S)) = \\mathrm{map}_{S_m}(\\operatorname{algebraMap}_R^S, \\, \\text{proof})$$$
Lean4
theorem localizationAlgebraMap_def :
@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S) =
map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :=
rfl
