hasColimit_of_hasLimit_unop

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasColimit_of_hasLimit_unop

← MathLib Explorer

English

If F: J^op ⥤ C^op has a limit, then F.unop has a colimit.

Русский

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

LaTeX

$$$$\\mathrm{HasColimit } F^{unop}$$$$

Lean4

theorem hasColimit_of_hasLimit_unop (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasLimit F.unop] : HasColimit F :=
  HasColimit.mk
    { cocone := coconeOfConeUnop (limit.cone F.unop)
      isColimit := isColimitCoconeOfConeUnop _ (limit.isLimit _) }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru