hasColimit_of_hasLimit_op

Mathlib.CategoryTheory.Limits.Opposites

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem hasColimit_of_hasLimit_op (F : J ⥤ C) [HasLimit F.op] : HasColimit F :=
  HasColimit.mk
    { cocone := (limit.cone F.op).unop
      isColimit := (limit.isLimit _).unop }

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

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

Разделы

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

Аффилиация

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