English
For R, M, N with finite presentation, and a localization S, the map IsLocalizedModule.mapExtendScalars S f g R_s is localized.
Русский
Для R, M, N с конечной презентацией и локализации S отображение IsLocalizedModule.mapExtendScalars S f g R_s является локализованным модулем.
LaTeX
$$$$ \\mathrm{IsLocalizedModule}.mapExtendScalars(S)\\; f\\; g \\; \\text{is localized over } R_s.$$$$
Lean4
instance isLocalizedModule_mapExtendScalars (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N']
[IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] [Module.FinitePresentation R M] :
IsLocalizedModule S (IsLocalizedModule.mapExtendScalars S f g Rₛ) :=
IsLocalizedModule.of_linearEquiv _ _ _