range_mapRangeAddMonoidHom — Mathlib

English

Similarly for ranges: the range of the global mapRange AddMonoidHom equals the comap of coordinate-wise ranges.

Русский

Аналогично для образов: образ глобального mapRange.addMonoidHom равен комапу по координатным образам.

LaTeX

$$$\\mathrm{range}(\\mathrm{mapRange.addMonoidHom}\\; f) = \\mathrm{AddSubgroup.comap}\\; (\\mathrm{coeFnAddMonoidHom})\\; (\\mathrm{AddSubgroup.pi}\\; \\mathrm{Set.univ} \\; (\\mathrm{range}\\; f_i))$$$

Lean4

theorem range_mapRangeAddMonoidHom [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommGroup (β₂ i)] (f : ∀ i, β₂ i →+ β₁ i) :
    (mapRange.addMonoidHom f).range = (AddSubgroup.pi Set.univ (f · |>.range)).comap coeFnAddMonoidHom :=
  AddSubgroup.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom f

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