English
Let J be finite and X ∈ C, f: J → C. The hom component of the left distributor is the sum of left whiskered biproducts, i.e., (leftDistributor X f).hom = ∑_{j∈J} (X ◁ biproduct.π f j) ≫ biproduct.ι (fun j ⇒ X ⊗ f j) j.
Русский
Пусть J конечен, X ∈ C и f: J → C. Гом-компонента левостоя распределителя равна сумме левых восхождений через биопродукт: (leftDistributor X f).hom = ∑ (X ◁ biproduct.π f j) ≫ biproduct.ι (fun j ⇒ X ⊗ f j) j.
LaTeX
$$$ (leftDistributor\, X\, f).hom = \\sum_{j\\in J} (X \\triangleleft \\text{biproduct.π } f j) \\;\\circ\\; \\text{biproduct.ι} (\\lambda j. X \\otimes f j) j $$$
Lean4
theorem leftDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) :
(leftDistributor X f).hom = ∑ j : J, (X ◁ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j := by
classical
ext
dsimp [leftDistributor, 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, ite_true, eqToHom_refl, Category.comp_id]
