colimitRightOpIsoUnopLimit — Mathlib

English

The colimit of F.rightOp is the opposite of the limit of F.

Русский

Колимит F.rightOp есть противоположность пределу F.

LaTeX

$$$$\\text{colimitRightOpIsoUnopLimit } F : \\text{colimit } F^{rightOp} \\cong op(\\text{limit } F). $$$$

Lean4

/-- The colimit of `F.rightOp` is the opposite of `limit F`. -/
def colimitRightOpIsoUnopLimit (F : Jᵒᵖ ⥤ C) [HasLimit F] : colimit F.rightOp ≅ op (limit F) :=
  colimit.isoColimitCocone ⟨_, isColimitCoconeRightOpOfCone _ (limit.isLimit _)⟩

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