English
If we have a finite index J and another finite K with biproducts, the lift through a matrix of morphisms x_j and a matrix m_jk interacts with the matrix of morphisms to yield the reshaped lift: lifting x then applying the matrix is the same as lifting the componentwise sums.
Русский
Если есть матрица из morphisms x_j и матрица m_{j k}, то композиция lift x с biproduct.matrix m равна lift функции, суммирующей по k соответствующие x_j и m_{j k}.
LaTeX
$$$\operatorname{biproduct.lift} x \\; ≫ \\; \operatorname{biproduct.matrix} m = \\; \operatorname{biproduct.lift} (\lambda k, \sum_j x_j \,\gg\; m_{j k})$$$
Lean4
@[reassoc]
theorem lift_matrix {K : Type} [Finite K] [HasFiniteBiproducts C] {f : J → C} {g : K → C} {P} (x : ∀ j, P ⟶ f j)
(m : ∀ j k, f j ⟶ g k) : biproduct.lift x ≫ biproduct.matrix m = biproduct.lift fun k => ∑ j, x j ≫ m j k :=
by
ext
simp [biproduct.lift_desc]
