mapBiproduct_hom_desc — Mathlib

English

The hom component of the mapped biproduct followed by biproduct.desc of the mapped maps equals the image under F of biproduct.desc of the original maps.

Русский

Гомоморфизм состава отображения би-производного через biprod.desc совпадает с образом F от исходного biproduct.desc.

LaTeX

$$$(F.mapBiproduct f).hom \\;\\circ\\; \\mathrm{biprod.desc}(F\\!\\!f)(F\\!\\!g) = F(\\mathrm{biproduct.desc} \\; f \\; g)$$$

Lean4

theorem mapBiproduct_hom_desc (g : ∀ j, f j ⟶ W) :
    ((F.mapBiproduct f).hom ≫ biproduct.desc fun j => F.map (g j)) = F.map (biproduct.desc g) := by
  rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]

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