eq_top_of_localization₀_maximal

English

Let N be a submodule of M. If for every maximal P the localization of N is the whole localized module, then N is the whole module.

Русский

Пусть N — подмодуль M. Если для каждого максимального идеала P локализация N равна всей локализованной модули, то N равняется всему M.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N_{\mathrm{local}}^{P} = M_{\mathrm{local}}^{P} \Rightarrow N = M.$$$$

Lean4

theorem eq_top_of_localization₀_maximal (N : Submodule R M)
    (h : ∀ (P : Ideal R) [P.IsMaximal], N.localized₀ P.primeCompl (f P) = ⊤) : N = ⊤ :=
  Submodule.eq_of_localization₀_maximal Mₚ f fun P hP ↦ by simpa using h P

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