English
In a preadditive monoidal category with finite biproducts, the interaction of the left distributor with the right distributor and the associator yields a coherent equality expressing how distributing on the left and then on the right corresponds to first distributing and then applying the associator, up to the biproduct map on the shape ⨁f.
Русский
В преводимой монодной категории с конечными двупродуктами взаимодействие левого и правого распределителей и ассоциатора даёт согласованное равенство: распределение слева затем справа эквивалентно распределению и применению ассоциатора, с учётом отображения biproduct.
LaTeX
$$$$\\Big(\\mathrm{leftDistributor}(X,f) \\otimes \\mathrm{id}_Y\\Big) \\;\\xrightarrow{\\; }\\; \\mathrm{rightDistributor}\\_Y \\;=\\; \\alpha_X^{(\\oplus f),Y} \\;\\circ\\; \\mathrm{rightDistributor}(f, X\\otimes Y) \\circ \\mathrm{biproduct.mapIso}(\\alpha_{-,X,Y}^{-1}) \\;,$$$
Lean4
theorem leftDistributor_rightDistributor_assoc {J : Type _} [Finite J] (X : C) (f : J → C) (Y : C) :
(leftDistributor X f ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
α_ X (⨁ f) Y ≪≫
(asIso (𝟙 X) ⊗ᵢ rightDistributor _ Y) ≪≫ leftDistributor X _ ≪≫ biproduct.mapIso fun _ => (α_ _ _ _).symm :=
by
classical
cases nonempty_fintype J
ext
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom, asIso_hom, comp_zero,
comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor, tensor_sum, comp_tensor_id, tensorIso_hom,
leftDistributor_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π,
Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]
simp_rw [← tensorHom_id, ← id_tensorHom]
simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite, dite_comp, tensor_dite,
dite_tensor]
simp
