instFinitePresentationLocalizationLocalizedModule

English

Let R be a commutative ring and M an R-module which is finitely presented. For any localization S of R, the localized module LocalizedModule S M is a finitely presented module over Localization S.

Русский

Пусть R — коммутативная кольцевая, M — R-модуль, конечной презентации. При любой локализации S модуля R локализованный модуль LocalizedModule S M является локализованным модулем над Localization S и имеет конечную презентацию.

LaTeX

$$$$ \text{If } M \text{ is a finitely presented } R\text{-module, then } \mathrm{LocalizedModule}_S(M) \text{ is a finitely presented } \mathrm{Localization}(S)\text{-module}.$$$$

Lean4

instance (S : Submonoid R) [Module.FinitePresentation R M] :
    Module.FinitePresentation (Localization S) (LocalizedModule S M) :=
  FinitePresentation.of_isBaseChange (LocalizedModule.mkLinearMap S M)
    ((isLocalizedModule_iff_isBaseChange S _ _).mp inferInstance)

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