opCoproductIsoProduct' — Mathlib

English

The canonical isomorphism from the opposite of a coproduct to the corresponding product in the opposite category relates the colimit cocone to the limit cone via IsColimit and IsLimit data.

Русский

Каноническое изоморфизмop(копроизведение) к произведению в противоположной категории соотносит колимитный кокон с пределом через IsColimit и IsLimit.

LaTeX

$$$\\text{opCoproductIsoProduct'}\\; (hc: IsColimit c)\\; (hf: IsLimit f) : op(c.pt) \\cong f.pt$$$

Lean4

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

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