English
A coherence relation holds between the left distributor, the associator, and the biproduct map for finite families, expressing that the natural isomorphisms commute in a coherent way with tensoring and biproducts.
Русский
Существует когерентное тождество между левым распределителем, ассоциатором и отображениями биопродукта для конечных семей, выражающее совместимость свойств тензорирования и биопродуктов.
LaTeX
$$$ (\\mathrm{Id}_X \\otimes \\alpha) \\circ (\\mathrm{leftDistributor}\\, X\\, f) = \\cdot \\text{(coherent composition with associator and biproduct maps)} $$$
Lean4
@[reassoc (attr := simp)]
theorem leftDistributor_hom_comp_biproduct_π {J : Type} [Finite J] (X : C) (f : J → C) (j : J) :
(leftDistributor X f).hom ≫ biproduct.π _ j = X ◁ biproduct.π _ j := by
classical
cases nonempty_fintype J
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
