limitRightOpIsoOpColimit — Mathlib

English

Inverse relation for limit left-op unop colimit iso with projection.

Русский

Обратная зависимость для лимита левыйOp-unop колимитного изоморфизма с проекцией.

LaTeX

$$$$ (\\text{limitLeftOpIsoUnopColimit}(F)).inv \\circ \\text{limit.\\pi} F^{leftOp} (op\\, j) = (\\operatorname{colimit.\\ι} F j.unop).unop $$$$

Lean4

/-- The limit of `F.rightOp` is the opposite of `colimit F`. -/
def limitRightOpIsoOpColimit (F : Jᵒᵖ ⥤ C) [HasColimit F] : limit F.rightOp ≅ op (colimit F) :=
  limit.isoLimitCone ⟨_, isLimitConeRightOpOfCocone _ (colimit.isColimit _)⟩

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