English
Let f_j : f(j) ⟶ T be a family of morphisms into a fixed object T from the components of a biproduct. Then the unique map from the biproduct to T determined by these components is the finite sum of the projections followed by the corresponding morphisms g_j; equivalently, the biproduct descent is the sum of the π_j followed by g_j.
Русский
Пусть имеется множество морфизмов f_j : f(j) ⟶ T. Тогда уникальный гомоморфизм из биопроизводного в T, заданный этими компонентами, равен сумме проекций π_j, последовательных к соответствующим отображениям g_j; то есть biproduct.desc = ∑_j π_f(j) ≫ g_j.
LaTeX
$$$\operatorname{biproduct.desc} \, g = \sum_{j \in J} \; \operatorname{biproduct.π} f\, j \;\gg\; g\, j$$$
Lean4
theorem desc_eq {T : C} {g : ∀ j, f j ⟶ T} : biproduct.desc g = ∑ j, biproduct.π f j ≫ g j := by
classical
ext j
simp [comp_sum, biproduct.ι_π_assoc, dite_comp]
