isLocalizedModule_mapExtendScalars

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 _ _ _

Похожие утверждения