isLimitEquivIsColimitOp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A pullback cone is a limit cone if and only if the corresponding pushout cocone
in the opposite category is a colimit cocone. -/
def isLimitEquivIsColimitOp {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : IsLimit c ≃ IsColimit c.op :=
  (IsLimit.equivIsoLimit c.opUnop).symm.trans c.op.isColimitEquivIsLimitUnop.symm

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