English
If N localizations at all maximal ideals are zero, then N is zero.
Русский
Если локализации N по всем максимальным идеалам равны нулю, то N равен нулю.
LaTeX
$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N localized^{P} = 0 \Rightarrow N = 0.$$$$
Lean4
theorem mem_of_isLocalized_span {m : M} {N : Submodule R M} (h : ∀ r : s, f r m ∈ N.localized₀ (.powers r.1) (f r)) :
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
by_contra! ne
have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
let r : s := ⟨r, hrs⟩
obtain ⟨a, ha, t, e⟩ := h r
rw [← IsLocalizedModule.mk'_one (.powers r.1), IsLocalizedModule.mk'_eq_mk'_iff] at e
have ⟨u, hu⟩ := e
simp_rw [smul_smul] at hu
exact Set.disjoint_right.mp disj (u * t).2 (by apply hu ▸ smul_mem _ _ ha)
