projective_of_isLocalizedModule — Mathlib

English

If a module M over R becomes projective after a base change along a localization, then the localized module is projective.

Русский

Если модуль над R становится проективным после базового превращения по локализации, то локализованный модуль проективен.

LaTeX

$$$M \\text{ projective over } R \\Rightarrow M_S \\text{ projective over } R_S$ (via base change).$$$

Lean4

theorem projective_of_isLocalizedModule {Rₛ Mₛ} [AddCommGroup Mₛ] [Module R Mₛ] [CommRing Rₛ] [Algebra R Rₛ]
    [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S) (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f]
    [Module.Projective R M] : Module.Projective Rₛ Mₛ :=
  Projective.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv

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