support_subset_of_injective — Mathlib

English

If M is finite, the support is characterized by a finite family of annihilators corresponding to spans of single elements.

Русский

Если M конечен, опора задаётся конечной семейством аннигиляторов элементов модуля, связанных с подпроствостями.

LaTeX

$$For Module.Finite M: p ∈ Supp_R(M) ⇔ ∃ m ∈ M, (R ∙ m).annihilator ≤ p$$

Lean4

@[stacks 00L3 "(2)"]
theorem support_subset_of_injective (hf : Function.Injective f) : Module.support R M ⊆ Module.support R N :=
  by
  simp_rw [Set.subset_def, mem_support_iff']
  rintro x ⟨m, hm⟩
  exact ⟨f m, fun r hr ↦ by simpa using hf.ne (hm r hr)⟩

Похожие утверждения