eq_bot_of_localization₀_maximal

English

Let N be a submodule of M. If, for every maximal ideal P of R, the localization of N at P is the zero submodule, then N is the zero submodule.

Русский

Пусть N будет подмодулем M. Если для каждого максимального идеала P кольца R локализация N по P равна нулю, то N = {0}.

LaTeX

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

Lean4

/-- A submodule is trivial if its localization at every maximal ideal is trivial. -/
theorem eq_bot_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

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