eq_bot_of_localization_maximal — Mathlib

English

If, for submodules N ≤ P, every localized inclusion N localized ≤ P localized holds, then N ≤ P.

Русский

Если локализованные включения сохраняют порядок: локализация N ≤ локализация P, то N ≤ P.

LaTeX

$$$$\forall N,P\;\bigl(N_{loc} \le P_{loc}\bigr) \Rightarrow N \le P.$$$$

Lean4

theorem eq_bot_of_localization_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized' (Rₚ P) P.primeCompl (f P) = ⊥) : N = ⊥ :=
  Submodule.eq_of_localization_maximal Rₚ Mₚ f fun P hP ↦ by simpa using h P

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