biproduct_ι_comp_rightDistributor_hom

English

For all j ∈ J, the composite (biproduct.ι f j) ▷ X ≫ (rightDistributor f X).hom equals biproduct.ι (fun j => f j ⊗ X) j.

Русский

Для каждого j из J композиция (biproduct.ι f j) ▷ X затем (rightDistributor f X).hom равна biproduct.ι (f j ⊗ X) j.

LaTeX

$$$ (biproduct.ι f j \\; \\triangleright\\; X) \\;\\circ\\; (rightDistributor f X).hom = \\text{biproduct.ι} (\\lambda j. f j \\otimes X) j $$$

Lean4

@[reassoc (attr := simp)]
theorem biproduct_ι_comp_rightDistributor_hom {J : Type} [Finite J] (f : J → C) (X : C) (j : J) :
    (biproduct.ι _ j ▷ X) ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j := by
  classical
  cases nonempty_fintype J
  simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π, dite_whiskerRight,
    dite_comp]

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