English
For a ring R, module M, and f ∈ R, Subsingleton of the localization M[(powers f)] is equivalent to a disjointness condition between the basic open of f and the supports of M.
Русский
Для кольца R, модуля M и элемента f ∈ R, свойство локализации M[(powers f)] быть единичным (subsingleton) эквивалентно тому, что множество базовой открытой части f и поддержка M не пересекаются.
LaTeX
$$$\\text{Subsingleton}(\\mathrm{LocalizedModule}(\\langle f \\rangle^\\text{powers}, M)) \\iff \\mathrm{Disjoint}(\\text{basicOpen}(f), \\mathrm{Module.support}\\ R M)$$$
Lean4
/-- `M[1/f] = 0` if and only if `D(f) ∩ Supp M = 0`. -/
theorem subsingleton_iff_disjoint {f : R} :
Subsingleton (LocalizedModule (.powers f) M) ↔ Disjoint ↑(PrimeSpectrum.basicOpen f) (Module.support R M) := by
rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, disjoint_compl_left_iff,
Set.le_iff_subset]
