English
Let C be a preadditive category, J a finite index set, and f: J → C. For T a fixed object and a family of maps g_j : T → f(j), the canonical map lifting g into the biproduct ⨁ f(j) is equal to the finite sum of the components g_j followed by the injections into the biproduct; i.e. lifting is the sum of g_j composed with the corresponding injections.
Русский
Пусть C — прeддобавитная категория, J — конечное множество индексов, f : J → C. Для фиксированного объекта T и семейства морфизмов g_j : T → f(j) средний биодепозитной конструкции ⨁ f(j) равен сумме компонентов, каждая из которых состоит из g_j последовательно с включением в бипроизводное. То есть lift g равен сумме g_j ≫ ι_f(j).
LaTeX
$$$\operatorname{biproduct.lift} \, g = \sum_{j \in J} \; g(j) \;\gg\; \operatorname{biproduct.ι}\ f\, j$$$
Lean4
theorem lift_eq {T : C} {g : ∀ j, T ⟶ f j} : biproduct.lift g = ∑ j, g j ≫ biproduct.ι f j := by
classical
ext j
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero, Finset.sum_dite_eq',
Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]
