π_comp_opProductIsoCoproduct_hom

English

The first component of the opposite product-coproduct is the opposite of the first projection into the product.

Русский

Первая компонента противоположного произведения и копродукта равна противоположности первой проекции.

LaTeX

$$$(opProdIsoCoprod A B).hom.unop \circ prod.fst = coprod.inl.unop$$

Lean4

theorem π_comp_opProductIsoCoproduct_hom [HasProduct Z] (b : α) :
    (Pi.π Z b).op ≫ (opProductIsoCoproduct Z).hom = Sigma.ι (op <| Z ·) b :=
  proj_comp_opProductIsoCoproduct'_hom _ _ b

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