English
In tilde localization, a nonzero divisor condition on a stalk implies that multiplication by a nonzero element cannot annihilate nonzero sections; i.e., smul by a nonzero divisor is injective on stalks.
Русский
В локализации tilde условие, что элемент не является делителем нуля в стэке, означает, что умножение на него не уничтожает ненулевые секции на стэках; т.е. умножение на ненулевой делитель буюет инъективно на стэках.
LaTeX
$$$\forall x:\Pr\imeSpectrum.Top R,\; r \text{ primeCompl},\; st \text{ stalk},\; r.1 • st = 0 \Rightarrow st = 0$$$
Lean4
theorem smul_stalk_no_nonzero_divisor {x : PrimeSpectrum R} (r : x.asIdeal.primeCompl)
(st : (tildeInModuleCat M).stalk x) (hst : r.1 • st = 0) : st = 0 :=
by
refine
Limits.Concrete.colimit_no_zero_smul_divisor _ _ _
⟨op ⟨PrimeSpectrum.basicOpen r.1, r.2⟩, fun U i s hs ↦ Subtype.eq <| funext fun pt ↦ ?_⟩ _ hst
apply LocalizedModule.eq_zero_of_smul_eq_zero _ (i.unop pt).2 _ (congr_fun (Subtype.ext_iff.1 hs) pt)
