free_of_isLocalizedModule — Mathlib

English

If a module base change along a localization is free after localization, then the original module is free over the localized ring.

Русский

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

LaTeX

$$$\\text{If } M \\text{ is free over } R, \\text{ then } M_\\mathrm{S} \\text{ is free over } R_\\mathrm{S}$ (via base change).$$$

Lean4

theorem free_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.Free R M] :
    Module.Free Rₛ Mₛ :=
  Free.of_equiv (IsLocalizedModule.isBaseChange S Rₛ f).equiv

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