rightDistributor_hom_comp_biproduct_π

English

Same as 77147: for finite J, f, X, the right distributor's hom component is the sum ∑ (biproduct.π f j ▷ X) ≫ biproduct.ι (f j ⊗ X).

Русский

То же, что и в 77147: для конечного J, f, X, гом-компонента правого распределителя равна сумме ∑ (biproduct.π f j ▷ X) ≫ biproduct.ι (f j ⊗ X).

LaTeX

$$$ (rightDistributor f X).hom = \\sum_{j \\in J} (biproduct.π f j \\triangleright X) \\circ \\text{biproduct.ι} (f j \\otimes X) j $$$

Lean4

@[reassoc (attr := simp)]
theorem rightDistributor_hom_comp_biproduct_π {J : Type} [Finite J] (f : J → C) (X : C) (j : J) :
    (rightDistributor f X).hom ≫ biproduct.π _ j = biproduct.π _ j ▷ X := by
  classical
  cases nonempty_fintype J
  simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

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