English
Let G: B ⥤ D, F: A ⥤ B, and L: A ⥤ C. If there exists a right Kan extension F' → F along L given by α: L ∘ F' ⟶ F, and if (F' ∘ G) equipped with the associator-corrected whiskerRight α G is also a right Kan extension, then G preserves right Kan extensions of F along L.
Русский
Пусть G: B ⥤ D, F: A ⥤ B и L: A ⥤ C. Если существует правое Кан-расширение F' ⟶ F вдоль L, заданное α: L ∘ F' ⟶ F, и если (F' ∘ G), снабжённое соответствующим whiskerRight-отображением α G через ассоциатор, также является правым Кан-расширением, тогда G сохраняет правые Кан-расширения F вдоль L.
LaTeX
$$$\\exists F', \\alpha:\\, L \\circ F' \\longrightarrow F \\quad[IsRightKanExtension(F', \\alpha)] \\land\\ [IsRightKanExtension\\big((F' \\circ G) \\big| (\\. associate^{-1} \\circ whiskerRight \\alpha \\ G)\\big)] \\Rightarrow G \\text{ preserves right Kan extensions } F \\text{ along } L.$$$
Lean4
/-- Show that `G` preserves right Kan extensions if it maps some right Kan extension to a right
Kan extension. -/
theorem mk_of_preserves_isRightKanExtension (F' : C ⥤ B) (α : L ⋙ F' ⟶ F) [IsRightKanExtension F' α]
(h : IsRightKanExtension (F' ⋙ G) <| (Functor.associator _ _ _).inv ≫ whiskerRight α G) :
G.PreservesRightKanExtension F L :=
.mk fun F'' α' h ↦
isRightKanExtension_of_iso (isoWhiskerRight (rightKanExtensionUnique F' α F'' α') G)
((Functor.associator _ _ _).inv ≫ whiskerRight α G) ((Functor.associator _ _ _).inv ≫ whiskerRight α' G)
(by ext x; simp [← G.map_comp])
