English
Let C be a preadditive monoidal category with finite biproducts. The canonical right distributivity morphisms interact with the associator to produce a coherent equality between the two ways of re‑grouping and distributing, namely the composite of the right distributor with an identity on Y and the right distributor on Y, and the associator followed by the right distributor on X⊗Y, up to the induced biproduct map.
Русский
Пусть C — преводимая абелева категория с монойдальной структурой и конечными двупродуктами. Канонические правые распределители взаимодействуют с ассоциатором так, чтобы получить согласованное равенство между двумя способами перераспределения и перераспределения частичных сумм: композиция правого распределителя с тождественным оператором на Y и правого распределителя на Y должна совпасть с композициями через ассоциатор и biproduct.mapIso (посредством обратного изоморфизма ассоциатора).
LaTeX
$$$\\Big(\\mathrm{rightDistributor}(f,X) \\otimes \\mathrm{id}_Y\\Big) \\;\\xrightarrow{\\; }\\; \\mathrm{rightDistributor} _ Y \;=\\; \\alpha_{(\\bigoplus f),X,Y} \\;\\circ\\; \\mathrm{rightDistributor}\\, f\\,(X\\otimes Y) \\circ \\mathrm{biproduct.mapIso}\\Big( \\lambda x. (\\alpha_{x,X,Y})^{-1} \\Big) \\;,$$$
Lean4
theorem rightDistributor_assoc {J : Type} [Finite J] (f : J → C) (X Y : C) :
(rightDistributor f X ⊗ᵢ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun _ => (α_ _ X Y).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, comp_tensor_id, tensorIso_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]
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
simp
