hasColimit_of_hasLimit_leftOp — Mathlib

English

If F.leftOp: J^op → C has a limit, then F : J → C^op has a colimit.

Русский

Если F.leftOp: J^op → C имеет предел, то F : J → C^op имеет колимит.

LaTeX

$$$$\\text{HasColimit } F \\quad\\text{because } \\text{coconeLeftOp}(\\text{cone}(F.leftOp))\\text{ is a colimit cocone.}$$$$

Lean4

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

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