English
Let J be finite. For a family f: J → C and X ∈ C, the hom component of the right distributor is the sum of whiskered projections: (rightDistributor f X).hom = ∑ j ∈ J (biproduct.π f j ▷ X) ≫ biproduct.ι (fun j => f j ⊗ X) j.
Русский
Для конечного J, семейства f и объекта X, гом-компонента правого распределителя равна сумме проекций, от whiskerRight: (rightDistributor f X).hom = ∑ (biproduct.π f j ▷ X) ≫ biproduct.ι (fun j => f j ⊗ X) j.
LaTeX
$$$ (rightDistributor f X).hom = \\sum_{j \\in J} (biproduct.π f j \\; \\triangleright\\; X) \\;\\circ\\; \\text{biproduct.ι} (\\lambda j. f j \\otimes X) j $$$
Lean4
theorem rightDistributor_hom {J : Type} [Fintype J] (f : J → C) (X : C) :
(rightDistributor f X).hom = ∑ j : J, (biproduct.π f j ▷ X) ≫ biproduct.ι (fun j => f j ⊗ X) j := by
classical
ext
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
erw [biproduct.lift_π]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero, Finset.sum_dite_eq',
Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
