isLimitEquivIsColimitUnop — Mathlib

English

A pullback cone is a limit cone iff the corresponding pushout cocone in the unop category is a colimit cone.

Русский

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

LaTeX

$$$$\mathrm{IsLimit}(c) \simeq \mathrm{IsColimit}(c^{\mathrm{unop}}).$$$$

Lean4

/-- A pullback cone is a limit cone in `Cᵒᵖ` if and only if the corresponding pushout cocone
in `C` is a colimit cocone. -/
def isLimitEquivIsColimitUnop {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    IsLimit c ≃ IsColimit c.unop :=
  (IsLimit.equivIsoLimit c.unopOp).symm.trans c.unop.isColimitEquivIsLimitOp.symm

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