π_comp_colimitOpIsoOpLimit_inv

Mathlib.CategoryTheory.Limits.Opposites

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$$\\mathrm{HasColimit } F.leftOp$$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_colimitOpIsoOpLimit_inv (F : J ⥤ C) [HasLimit F] (j : J) :
    (limit.π F j).op ≫ (colimitOpIsoOpLimit F).inv = colimit.ι F.op (op j) := by simp [Iso.comp_inv_eq]

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

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

Разделы

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

Аффилиация

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