rightKanExtensionCompIsoOfPreserves

Mathlib.CategoryTheory.Functor.KanExtension.Preserves

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

Lean4

/-- Extract an isomorphism `rightKanExtension L F ⋙ G ≅ rightKanExtension L (F ⋙ G)` when `G`
preserves right Kan extensions. -/
def rightKanExtensionCompIsoOfPreserves [PreservesRightKanExtension G F L] [L.HasRightKanExtension F] :
    L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G) :=
  rightKanExtensionUnique (L.rightKanExtension F ⋙ G)
    ((Functor.associator _ _ _).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G) (L.rightKanExtension <| F ⋙ G)
    (L.rightKanExtensionCounit <| F ⋙ G)

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

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

Разделы

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

Аффилиация

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