English
Let f: J → C and g: K → C be families of objects in a category with finite biproducts. For every matrix m with entries m_{j,k}: f(j) → g(k), the composite from the j-th summand into the target biproduct equals the j-th row of m collected into a biproduct, i.e. biproduct.ι f j ≫ biproduct.matrix m = biproduct.lift (λ k, m j k).
Русский
Пусть f: J → C и g: K → C — семейства объектов в категории с конечными биопродуктами. Для любой матрицы m с элементами m_{j,k}: f(j) → g(k) композит из инъекции j-го сомножителя в биопродукт по марице равен j-ой строке матрицы, собранной в биопродукт: biproduct.ι f j ≫ biproduct.matrix m = biproduct.lift (λ k, m j k).
LaTeX
$$$ \\operatorname{biproduct.\\iota} f\\, j \\; \\circ \\operatorname{biproduct.matrix} m = \\operatorname{biproduct.lift} \\big( \\lambda k \\mapsto m\\, j\\, k \\big) $$$
Lean4
@[reassoc (attr := simp)]
theorem ι_matrix (m : ∀ j k, f j ⟶ g k) (j : J) :
biproduct.ι f j ≫ biproduct.matrix m = biproduct.lift fun k => m j k := by simp [biproduct.matrix]
