English
Let N and N' be submodules. If their localized inclusions hold at every maximal ideal, then N ≤ N'.
Русский
Если локализованные включения S N и N' верны во всех максимальных идеалах, тогда N ⊆ N'.
LaTeX
$$$\\forall P [P.IsMaximal], N.localized_0 P.primeCompl (f P) \\le N'.localized_0 P.primeCompl (f P) \\Rightarrow N \\le N'.$$$
Lean4
theorem mem_of_localization_maximal (m : M) (N : Submodule R M)
(h : ∀ (P : Ideal R) [P.IsMaximal], f P m ∈ N.localized₀ P.primeCompl (f P)) : m ∈ N :=
by
let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)
suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_
obtain ⟨a, ha, s, e⟩ := h P
rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e
obtain ⟨t, ht⟩ := e
simp_rw [smul_smul] at ht
exact (t * s).2 (le <| by apply ht ▸ smul_mem _ _ ha)
