annihilator_dfinsupp — Mathlib

English

The annihilator of the DFinsupp of modules equals the infimum (intersection) of the annihilators of each component.

Русский

Аннигилятор DFinsupp модулей равен пересечению аннигиляторов по всем компонентам.

LaTeX

$$$ \\operatorname{Ann}_R\\Big(\\Pi_0 i, M_i\\Big) = \\bigcap_i \\operatorname{Ann}_R(M_i). $$$

Lean4

theorem annihilator_dfinsupp : annihilator R (Π₀ i, M i) = ⨅ i, annihilator R (M i) :=
  by
  ext r; simp only [mem_annihilator, Ideal.mem_iInf]
  constructor <;> intro h
  · intro i m
    classical simpa using DFunLike.congr_fun (h (DFinsupp.single i m)) i
  · intro m; ext i; exact h i _

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