colimitCoyonedaIso

Mathlib.CategoryTheory.Limits.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Coyoneda.colimitCoyonedaIso

Lean4

/-- The colimit of `coyoneda.obj X` is isomorphic to `PUnit`.
-/
noncomputable def colimitCoyonedaIso (X : Cᵒᵖ) : colimit (coyoneda.obj X) ≅ PUnit := by
  apply
    colimit.isoColimitCocone
      { cocone := _
        isColimit := colimitCoconeIsColimit X }

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

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

Разделы

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

Аффилиация

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