English
If IsLocalization (Algebra.algebraMapSubmonoid A S) A_s holds, then IsLocalizedModule S (IsScalarTower.toAlgHom R A A_s).toLinearMap holds.
Русский
Если выполняется локализация IsLocalization (Algebra.algebraMapSubmonoid A S) A_s, то существует структура локализации модуля для линейного отображения, соответствующая IsScalarTower.
LaTeX
$$$\\IsLocalization\\big(\\mathsf{algebraMapSubmonoid}\\,A\\,S\\big) A_s \\Rightarrow \\IsLocalizedModule S\\big(\\IsScalarTower.toAlgHom R A A_s\\big).toLinearMap.$$$
Lean4
instance [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] :
IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap :=
isLocalizedModule_iff_isLocalization.mpr ‹_›
