eq_of_localization_maximal — Mathlib

English

If every localized module M_p is a singleton, then the global module M is a singleton.

Русский

Если каждый локализованный модуль M_p является синглетоном, то глобальный модуль M — тоже синглетон.

LaTeX

$$$$\bigl(\forall P\,[P^{{\mathrm{Max}}],\; \operatorname{Subsingleton}(M_p)\bigr) \Rightarrow \operatorname{Subsingleton}(M).$$$$

Lean4

theorem eq_of_localization_maximal {N₁ N₂ : Submodule R M}
    (h :
      ∀ (P : Ideal R) [P.IsMaximal],
        N₁.localized' (Rₚ P) P.primeCompl (f P) = N₂.localized' (Rₚ P) P.primeCompl (f P)) :
    N₁ = N₂ :=
  eq_of_localization₀_maximal Mₚ f fun P _ ↦ congr(restrictScalars _ $(h P))

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