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