English
Let R be a commutative semiring, S a submonoid of R, and A a semiring with an R-algebra structure. After localizing R at S we may view elements of Localization(S,R) and Localization(S,A). Then the R-algebra structure is compatible with localization in the sense that the algebra map applied to the localization of a is the same as localizing the image of a in A: algebraMap(Localization S of R to Localization S of A) (Localization.mk a s) = Localization.mk (algebraMap_R^A a) s.
Русский
Пусть R — коммутативное полукольцо, S — подмонойд множителей в R, A — полукольцо с R-алгеброй. После локализации по S и элементы Localization(S,R), Localization(S,A). Тогда структура R-алгебры совместима с локализацией: применяя алгебраическое отображение к локализации a/s в Localization S(R) получается локализация алгебраического изображения a в A: algebraMap(Localization S) (Localization.mk a s) = mk (algebraMap_R^A a) s.
LaTeX
$$$\\operatorname{algebraMap}_{\\mathrm{Localization}(S)\\to\\mathrm{Localization}(S)}\\big(\\mathrm{Localization.mk}\\;a\\;s\\big) = \\mathrm{mk}\\big(\\operatorname{algebraMap}_{R\\to A}(a)\\big,\\;s\\)$$$
Lean4
theorem algebraMap_mk {A : Type*} [Semiring A] [Algebra R A] (a : R) (s : S) :
algebraMap _ _ (Localization.mk a s) = mk (algebraMap R A a) s :=
by
rw [Localization.mk_eq_mk']
exact algebraMap_mk' ..
