ι_comp_colimitOpIsoOpLimit_hom

Mathlib.CategoryTheory.Limits.Opposites

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

← MathLib Explorer

English

If F: Jᵒᵖ ⥤ C has a limit, then F.rightOp has a colimit.

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem ι_comp_colimitOpIsoOpLimit_hom (F : J ⥤ C) [HasLimit F] (j : Jᵒᵖ) :
    colimit.ι F.op j ≫ (colimitOpIsoOpLimit F).hom = (limit.π F j.unop).op := by simp [colimitOpIsoOpLimit]

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

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

Разделы

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

Аффилиация

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