hasLimit_of_hasColimit_leftOp — Mathlib

English

The limit of F.op is the opposite of the colimit of F; equivalently, lim F.op ≅ op(colim F).

Русский

Предел F.op равен противоположному колимиту F; эквивалентно lim F.op ≅ op(colim F).

LaTeX

$$$$ \\lim (F^{\\mathrm{op}}) \\cong (\\mathrm{colim} F)^{\\mathrm{op}} $$$$

Lean4

/-- If `F.leftOp : Jᵒᵖ ⥤ C` has a colimit, we can construct a limit for `F : J ⥤ Cᵒᵖ`.
-/
theorem hasLimit_of_hasColimit_leftOp (F : J ⥤ Cᵒᵖ) [HasColimit F.leftOp] : HasLimit F :=
  HasLimit.mk
    { cone := coneOfCoconeLeftOp (colimit.cocone F.leftOp)
      isLimit := isLimitConeOfCoconeLeftOp _ (colimit.isColimit _) }

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