English
If the base algebra map a: R → S is injective, then the induced algebra map from the localized algebra R_m to S_m is also injective.
Русский
Если отображение алгебраических структур a: R → S инъективно, то индукцированное отображение после локализации R_m → S_m также инъективно.
LaTeX
$$$\\text{If } \\mathrm{algebraMap}\\; R\\; S\\text{ is injective, then }\\operatorname{algebraMap}_{R_m S_m}(\\text{localizationAlgebra}(M,S))\\text{ is injective.}$$$
Lean4
/-- Injectivity of the underlying `algebraMap` descends to the algebra induced by localization. -/
theorem localizationAlgebra_injective (hRS : Function.Injective (algebraMap R S)) :
Function.Injective (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) :=
have : IsLocalization (M.map (algebraMap R S)) Sₘ := i
IsLocalization.map_injective_of_injective _ _ _ hRS
