of_isLocalization — Mathlib

English

If S is a submonoid of R and A is an IsLocalization of S, then M is invertible as an A-module after base change.

Русский

Пусть S — подмножество R, и A — локализация H(S). После смены оснований M становится обратимым модулем над A.

LaTeX

$$Module.Invertible.of_isLocalization ...$$

Lean4

theorem of_isLocalization (S : Submonoid R) [IsLocalization S A] (f : M →ₗ[R] N) [IsLocalizedModule S f] [Module A N]
    [IsScalarTower R A N] : Module.Invertible A N :=
  .congr (IsLocalizedModule.isBaseChange S A f).equiv

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