opProductIsoCoproduct_inv_comp_lift

English

The coprod.inl, composed with the inverse of opProdIsoCoprod, equals prod.fst.op in the opposite category.

Русский

Копрод.inl после обратного opProdIsoCoprod равен prod.fst.op в противоположной категории.

LaTeX

$$coprod.inl \circ (opProdIsoCoprod A B).inv = prod.fst.op$$

Lean4

theorem opProductIsoCoproduct_inv_comp_lift [HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) :
    (opProductIsoCoproduct Z).inv ≫ (Pi.lift π).op = Sigma.desc (fun a ↦ (π a).op) :=
  by
  convert opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z) (coproductIsCoproduct (op <| Z ·)) (Fan.mk _ π)
  · simp [Pi.lift, productIsProduct]
  · simp [Sigma.desc, coproductIsCoproduct]

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