opProductIsoCoproduct' — Mathlib

English

There exists a canonical isomorphism between the opposite of the product and the coproduct in the opposite category, built from a limit and a colimit.

Русский

Существует канонический изоморфизм между противоположностью произведения и копродукта в противоположной категории, построенный из предела и колимита.

LaTeX

$$$op f.p t \cong c.p t$ where $f$ is a limit cone on $Z$ and $c$ is a colimit cocone on $Z$$$

Lean4

/-- The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct
in the opposite category.
-/
def opProductIsoCoproduct' {f : Fan Z} {c : Cofan (op <| Z ·)} (hf : IsLimit f) (hc : IsColimit c) : op f.pt ≅ c.pt :=
  IsColimit.coconePointUniqueUpToIso (Fan.IsLimit.op hf) hc

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