closedPoint_mem_support — Mathlib

English

Let R be local and M a nontrivial module. Then the closed point of Spec(R) belongs to the support of M.

Русский

Пусть R локальное и M не тождественно нуль-область; тогда закрытая точка спектра Spec(R) лежит в поддержке модуля M.

LaTeX

$$$\\text{ClosedPoint}(R) \\in \\mathrm{Module.support}\\ R\\ M$$$

Lean4

theorem closedPoint_mem_support [IsLocalRing R] [Nontrivial M] : IsLocalRing.closedPoint R ∈ Module.support R M :=
  by
  obtain ⟨p, hp⟩ := (Module.nonempty_support_iff (R := R)).mpr ‹_›
  exact Module.mem_support_mono le_top hp

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