English
The inverse of the right distributor equals the sum of biproduct projections followed by the whiskering of injections by X: (rightDistributor f X).inv = ∑ j ∈ J biproduct.π f j ≫ (biproduct.ι f j ▷ X).
Русский
Обратная правому распределителю сумма проекций биопродукта, затем штрихование инъекций X: (rightDistributor f X).inv = ∑ biproduct.π f j ≫ (biproduct.ι f j ▷ X).
LaTeX
$$$ (rightDistributor f X).inv = \\sum_{j\\in J} \\text{biproduct.π } f j \\;\\circ\\; (\\text{biproduct.ι } f j \\triangleright X) $$$
Lean4
theorem rightDistributor_inv {J : Type} [Fintype J] (f : J → C) (X : C) :
(rightDistributor f X).inv = ∑ j : J, biproduct.π _ j ≫ (biproduct.ι f j ▷ X) := by
classical
ext
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
simp only [biproduct.ι_desc, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp, Finset.sum_dite_eq,
Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
