English
If a span of vectors in M has top span, then p ∈ Supp(M) iff there exists m in the span with a certain annihilator contained in p.
Русский
Если порождающая область Span(s) равна верхней границе, тогда p ∈ Supp(M) эквивалентно существованию m в Span(s) с нужным свойством аннигилятора.
LaTeX
$$$p \in \mathrm{Supp}_R(M) \iff \exists m \in \mathrm{Span}_R(s), (R\cdot m).annihilator \le p.asIdeal$$$
Lean4
theorem mem_support_iff_of_span_eq_top {s : Set M} (hs : Submodule.span R s = ⊤) :
p ∈ Module.support R M ↔ ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal :=
by
constructor
· contrapose
rw [notMem_support_iff, LocalizedModule.subsingleton_iff_ker_eq_top, ← top_le_iff, ← hs, Submodule.span_le,
Set.subset_def]
simp_rw [SetLike.le_def, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe,
LocalizedModule.mem_ker_mkLinearMap_iff]
push_neg
simp_rw [and_comm]
exact id
· intro ⟨m, _, hm⟩
exact mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩
