ker_lmap — Mathlib

English

The kernel of lmap f equals the comap of the pi-submodule of the kernels of f_i.

Русский

Ядро lmap f равно прообразу (comap) пи-подмодуля ядер каждого f_i.

LaTeX

$$$\\ker(\\mathrm{lmap}\\ f) = \\big(\\mathrm{Submodule.pi} \\big(\\mathrm{Set.univ}, i \\mapsto \\ker(f_i)\\big)\\big).\\mathrm{comap}(\\mathrm{DirectSum.coeFnLinearMap}\\,R).$$$

Lean4

theorem ker_lmap :
    LinearMap.ker (lmap f) = (Submodule.pi Set.univ (fun i ↦ LinearMap.ker (f i))).comap (DirectSum.coeFnLinearMap R) :=
  DFinsupp.ker_mapRangeLinearMap f

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