English
A complex coherence identity between left Distributor, associator, and biproduct maps, expressing that the canonical isomorphisms commute with the distributive structure and biproducts.
Русский
Сложное когерентное тождество между левым распределителем, ассоциатором и отображениями биопродукта, выражающее совместимость изоморфизмов с распределительным строением.
LaTeX
$$$ (\\mathrm{Id}_X \\otimes \\mathrm{leftDistributor}(Y,f)) \\circ \\mathrm{leftDistributor}(X,f) = \\alpha_{X,Y,\\oplus f}^{-1} \\circ \\mathrm{leftDistributor}(X \\otimes Y,f) \\circ \\mathrm{biproduct.mapIso}(\\lambda x. \\alpha_{X,Y,f(x)}) $$$
Lean4
theorem leftDistributor_assoc {J : Type} [Finite J] (X Y : C) (f : J → C) :
(asIso (𝟙 X) ⊗ᵢ leftDistributor Y f) ≪≫ leftDistributor X _ =
(α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun _ => α_ X Y _ :=
by
classical
cases nonempty_fintype J
ext
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom, asIso_hom, comp_zero,
comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum, id_tensor_comp, tensorIso_hom,
leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel,
Finset.sum_dite_eq', Finset.sum_const_zero]
simp_rw [← id_tensorHom]
simp only [← id_tensor_comp, biproduct.ι_π]
simp only [id_tensor_comp, tensor_dite, comp_dite]
simp
