English
Same principle as above: the subsingleton condition for LocalizedModule at powers of f corresponds to a subset condition for the support.
Русский
Повторение принципа: подпространство subsingleton для LocalizedModule на степенях f эквивалентно подмножественному условию опоры.
LaTeX
$$Subsingleton(LocalizedModule(Submonoid.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus{f}$$
Lean4
theorem subsingleton_iff_support_subset {f : R} :
Subsingleton (LocalizedModule (.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus { f } :=
by
rw [LocalizedModule.subsingleton_iff]
constructor
· rintro H x hx' f rfl
obtain ⟨m, hm⟩ := Module.mem_support_iff_exists_annihilator.mp hx'
obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m
exact Ideal.IsPrime.mem_of_pow_mem inferInstance n (hm ((Submodule.mem_annihilator_span_singleton _ _).mpr e))
· intro H m
by_cases h : (Submodule.span R { m }).annihilator = ⊤
· rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
exact ⟨1, one_mem _, by simpa using h⟩
obtain ⟨n, hn⟩ : f ∈ (Submodule.span R { m }).annihilator.radical :=
by
rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
rintro p ⟨hp, hp'⟩
simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)
exact ⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩
