English
For finite J, f: J → C, and X ∈ C, the inverse of the right distributor composed with the projection equals the projection in the right biproduct: (rightDistributor f X).inv ∘ biproduct.π f j ▷ X = biproduct.π (fun j => f j ⊗ X) j.
Русский
Для конечного J, f: J → C и X ∈ C, обратная справа распределителя после проекции равна проекции: (rightDistributor f X).inv ∘ biproduct.π f j ▷ X = biproduct.π (f j ⊗ X) j.
LaTeX
$$$ (rightDistributor f X).inv \\circ (\\text{biproduct.π } f j \\triangleright X) = \\text{biproduct.π} (\\lambda j. f j \\otimes X) j $$$
Lean4
@[reassoc (attr := simp)]
theorem rightDistributor_inv_comp_biproduct_π {J : Type} [Finite J] (f : J → C) (X : C) (j : J) :
(rightDistributor f X).inv ≫ (biproduct.π _ j ▷ X) = biproduct.π _ j := by
classical
cases nonempty_fintype J
simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_whiskerRight, biproduct.ι_π, dite_whiskerRight, comp_dite]
