hasColimit_op_of_hasLimit

Mathlib.CategoryTheory.Limits.Opposites

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

← 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

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

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

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

Разделы

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

Аффилиация

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