English
If M is a finite R-module, the above equivalences simplify to finite-span criteria for p ∈ Spec(R).
Русский
Если M — конечный модуль над R, вышеупомянутые эквивалентности упрощаются к конечной совокупности критериев для p ∈ Spec(R).
LaTeX
$$If Module.Finite R M, then p ∈ Supp_R(M) iff ... (finite span annihilator condition)$$
Lean4
theorem mem_support_iff_of_finite : p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal := by
classical
obtain ⟨s, hs⟩ := ‹Module.Finite R M›
refine ⟨annihilator_le_of_mem_support, fun H ↦ (mem_support_iff_of_span_eq_top hs).mpr ?_⟩
simp only [SetLike.le_def, Submodule.mem_annihilator_span_singleton] at H ⊢
contrapose! H
choose x hx hx' using Subtype.forall'.mp H
refine ⟨s.attach.prod x, ?_, ?_⟩
· rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]
intro m
obtain ⟨k, hk⟩ := Finset.dvd_prod_of_mem x (Finset.mem_attach _ m)
rw [hk, mul_comm, mul_smul, hx, smul_zero]
· exact p.asIdeal.primeCompl.prod_mem (fun x _ ↦ hx' x)
