English
Let M be a finite R-module. If M_p = 0 for some prime p, then there exists f not in p such that M_f = 0 (i.e., the localization away from f is trivial).
Русский
Пусть M — конечный модуль над R. Если локализация M_p равна нулю для некоторого простого p, то существует f, не лежащий в p, такой что M_f = 0 (локализация по степеням f тождественно нулевая).
LaTeX
$$$\\exists f \\notin p,\\ M_f = 0.$$$
Lean4
/-- If `M` is a finite module such that `Mₚ = 0` for some `p`,
then `M[1/f] = 0` for some `p ∈ D(f)`. -/
theorem exists_subsingleton_away (p : Ideal R) [p.IsPrime] [Subsingleton (LocalizedModule p.primeCompl M)] :
∃ f ∉ p, Subsingleton (LocalizedModule (.powers f) M) :=
by
have : ⟨p, inferInstance⟩ ∈ (Module.support R M)ᶜ := by simpa [Module.notMem_support_iff]
rw [Module.support_eq_zeroLocus, ← Set.biUnion_of_singleton (Module.annihilator R M : Set R),
PrimeSpectrum.zeroLocus_iUnion₂, Set.compl_iInter₂, Set.mem_iUnion₂] at this
obtain ⟨f, hf, hf'⟩ := this
exact
⟨f, by simpa using hf', subsingleton_iff.mpr fun m ↦ ⟨f, Submonoid.mem_powers f, Module.mem_annihilator.mp hf _⟩⟩
