range_lmap — Mathlib

English

The range of lmap f equals the comap of the pi-submodule of the ranges of f_i.

Русский

Образ lmap f равен прообразу пи-подмодуля диапазонов f_i.

LaTeX

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

Lean4

theorem range_lmap :
    LinearMap.range (lmap f) =
      (Submodule.pi Set.univ (fun i ↦ LinearMap.range (f i))).comap (DirectSum.coeFnLinearMap R) :=
  DFinsupp.range_mapRangeLinearMap f

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