subsingleton_of_localization_maximal

English

A restatement variant: if all localizations of N are zero, then N is zero.

Русский

Повторное утверждение: если все локализации N равны нулю, то N равен нулю.

LaTeX

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

Lean4

theorem subsingleton_of_localization_maximal (h : ∀ (P : Ideal R) [P.IsMaximal], Subsingleton (Mₚ P)) :
    Subsingleton M := by
  rw [subsingleton_iff_forall_eq 0]
  intro x
  exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

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