English
If finite biproducts exist, the map induced by a family of arrows h_j : f(j) ⟶ g(j) yields a matrix-like morphism from the biproduct of f to the biproduct of g, computed by composing with injections and projections along the factorwise maps.
Русский
Если существуют конечные бипродукты, отображение, заданное семейством гомоморфизмов h_j : f(j) ⟶ g(j), образует отображение между биопродуктами с помощью композиций с инъекциями и проекциями по каждому компоненту.
LaTeX
$$$\operatorname{biproduct.map} \; h = \sum_{j \in J} \; \operatorname{biproduct.π} f j \,\gg\; h j \,\gg\; \operatorname{biproduct.ι} g j$$$
Lean4
theorem map_eq [HasFiniteBiproducts C] {f g : J → C} {h : ∀ j, f j ⟶ g j} :
biproduct.map h = ∑ j : J, biproduct.π f j ≫ h j ≫ biproduct.ι g j := by
classical
ext
simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, dite_comp]
