biproduct_ι_comp_rightDistributor_inv

English

For finite J, f: J → C, X ∈ C, and j ∈ J, the projection bis (biproduct.ι f j) composed with the inverse of the right distributor equals the left whiskered projection: biproduct.ι f j ≫ (rightDistributor f X).inv = biproduct.ι (fun j => f j ⊗ X) j ▷ X.

Русский

Для конечного J, f: J → C, X ∈ C, j ∈ J: biproduct.ι f j ≫ (rightDistributor f X).inv = biproduct.ι (f j ⊗ X) j ▷ X.

LaTeX

$$$ \\text{biproduct.ι } f j \\;\\circ\\; (rightDistributor f X)^{-1} = (\\text{biproduct.ι } f j) \\;\\triangleright\\; X $$$

Lean4

@[reassoc (attr := simp)]
theorem biproduct_ι_comp_rightDistributor_inv {J : Type} [Finite J] (f : J → C) (X : C) (j : J) :
    biproduct.ι _ j ≫ (rightDistributor f X).inv = biproduct.ι _ j ▷ X := by
  classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp]

Похожие утверждения