English
There is a coherence relation between the left distributor, the associator, and the biproduct structure: the natural isomorphisms relating X, Y, and the finite family f commute in a specified way with left distributors and biproduct maps.
Русский
Существует когерентность между левым распределителем, ассоциатором и структурой двупроизводных: натуральные изоморфизмы для X, Y и конечной семьи f совместимы с левым распределителем и биопродуктовыми отображениями.
LaTeX
$$$ (\\mathrm{Id}_X \\otimes \\text{leftDistributor}(Y,f)) \;\\circ \\text{leftDistributor}(X,f) = \\alpha^{-1}_{X,Y,\\oplus f} \\circ \\text{leftDistributor}(X\\otimes Y,f) \\circ \\mathrm{biproduct.mapIso}(\\lambda j. \\alpha_{X,Y,f(j)}) $$$
Lean4
theorem sum_tensor {P Q R S : C} {J : Type*} (s : Finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) :
(∑ j ∈ s, g j) ⊗ₘ f = ∑ j ∈ s, g j ⊗ₘ f := by
simp only [tensorHom_def, sum_whiskerRight, Preadditive.sum_comp]
-- In a closed monoidal category, this would hold because
-- `tensorLeft X` is a left adjoint and hence preserves all colimits.
-- In any case it is true in any preadditive category.
