range_map — Mathlib

English

For f_i, the range of DirectSum.map f equals the comap of the pi-range data: image is those tuples whose i-th component is in range(f_i).

Русский

Образ DirectSum.map f равен прообразу пи-образов: каждое i-тое слагаемое лежит в образе f_i.

LaTeX

$$$\\mathrm{range}(DirectSum.map f) = \\mathrm{comap}(\\mathrm{DirectSum.coeFnAddMonoidHom} N)(\\mathrm{AddSubgroup.pi}(\\mathrm{Set.univ}, i \\mapsto \\mathrm{range}(f_i))).$$$

Lean4

theorem range_map [∀ i, AddCommGroup (M i)] [∀ i, AddCommGroup (N i)] (f : ∀ i, M i →+ N i) :
    (map f).range = (AddSubgroup.pi Set.univ (f · |>.range)).comap (DirectSum.coeFnAddMonoidHom N) :=
  DFinsupp.range_mapRangeAddMonoidHom f

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