mker_map — Mathlib

English

The kernel of the direct-sum map DirectSum.map f is the comap of the pi-submonoid of ker f_i.

Русский

Ядро отображения DirectSum.map f равно прообразу (comap) прямой суммы по единице pi от ядер каждого f_i.

LaTeX

$$$\\ker(DirectSum.map f) = \\mathrm{comap}\\big(\\mathrm{DirectSum.coeFnAddMonoidHom}\\,M\\big)\\Big(\\mathrm{AddSubmonoid.pi}\\big(\\mathrm{Set.univ}, i \\mapsto \\ker(f_i)\\big)\\Big).$$$

Lean4

theorem mker_map :
    AddMonoidHom.mker (map f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mker (f i))).comap (coeFnAddMonoidHom M) :=
  DFinsupp.mker_mapRangeAddMonoidHom f

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