English
Let J be finite. For X ∈ C and f: J → C, the inverse left distributor composed with the projection equals the projection in the left biproduct: (leftDistributor X f).inv ∘ (X ◁ biproduct.π f j) = biproduct.π (fun j => X ⊗ f j) j.
Русский
Пусть J конечен. Тогда обратный левому распределителю, композиционный с проекцией, даёт проекцию левополупроизводного биопродукта: (leftDistributor X f).inv ∘ (X ◁ biproduct.π f j) = biproduct.π (fun j => X ⊗ f j) j.
LaTeX
$$$ (leftDistributor\\; X\\; f)^{-1} \\;\\circ\\; (X \\triangleleft \\text{biproduct.π } f j) = \\text{biproduct.π} (\\lambda j. X \\otimes f j) j $$$
Lean4
@[reassoc (attr := simp)]
theorem leftDistributor_inv_comp_biproduct_π {J : Type} [Finite J] (X : C) (f : J → C) (j : J) :
(leftDistributor X f).inv ≫ (X ◁ biproduct.π _ j) = biproduct.π _ j := by
classical
cases nonempty_fintype J
simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp, biproduct.ι_π, whiskerLeft_dite, comp_dite]
