desc_op_comp_opCoproductIsoProduct_hom

English

For each b, the inverse composed with the b-th opposite injection equals the b-th projection.

Русский

Для каждого b обратное после b-й противоположной инъекции равно b-й проекции.

LaTeX

$$$(\mathrm{opCoproductIsoProduct}'(hc, hf))^{-1} \circ (c_{\mathrm{inj}}(b))^{\mathrm{op}} = f_{\mathrm{proj}}(b)$$$

Lean4

theorem desc_op_comp_opCoproductIsoProduct_hom [HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X) :
    (Sigma.desc π).op ≫ (opCoproductIsoProduct Z).hom = Pi.lift (fun a ↦ (π a).op) :=
  by
  convert desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·)) (Cofan.mk _ π)
  · simp [Sigma.desc, coproductIsCoproduct]
  · simp [Pi.lift, productIsProduct]

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