biproduct_ι_comp_leftDistributor_inv

English

For fixed J, X, f: J → C and j ∈ J, the comparison (X ◁ biproduct.ι f j) ≫ (leftDistributor X f).hom equals biproduct.ι (fun j => X ⊗ f j) j.

Русский

Для фиксированного J, X, f: J → C и j ∈ J выполнено (X ◁ biproduct.ι f j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j.

LaTeX

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

Lean4

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

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