leftKanExtensionObjIsoColimit

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.leftKanExtensionObjIsoColimit

Lean4

/-- If a left Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a colimit. -/
noncomputable def leftKanExtensionObjIsoColimit [HasLeftKanExtension L F] (X : D) :
    (L.leftKanExtension F).obj X ≅ colimit (proj L X ⋙ F) :=
  LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit (F := F)
    (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X)

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

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

Разделы

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

Аффилиация

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