ranObjObjIsoLimit

Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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

Lean4

/-- If a right Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a limit. -/
noncomputable def ranObjObjIsoLimit (F : C ⥤ H) [HasPointwiseRightKanExtension L F] (X : D) :
    (L.ran.obj F).obj X ≅ limit (StructuredArrow.proj X L ⋙ F) :=
  RightExtension.IsPointwiseRightKanExtensionAt.isoLimit (F := F) (isPointwiseRightKanExtensionRanCounit L F X)

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

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

Разделы

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

Аффилиация

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