mk_of_preserves_isLeftKanExtension

English

If F' is a leftKan extension of F and G preserves F' via a certain whiskering, then G preserves the left Kan extension of F along L.

Русский

Если F' является левым кан-расширением F, и G сохраняет F' через соответствующий whisker, то G сохраняет левое кан-расширение F вдоль L.

LaTeX

$$$G.PreservesLeftKanExtension F L$$$

Lean4

/-- Show that `G` preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension. -/
theorem mk_of_preserves_isLeftKanExtension (F' : C ⥤ B) (α : F ⟶ L ⋙ F') [IsLeftKanExtension F' α]
    (h : IsLeftKanExtension (F' ⋙ G) <| whiskerRight α G ≫ (Functor.associator _ _ _).hom) :
    G.PreservesLeftKanExtension F L :=
  .mk fun F'' α' h ↦
    isLeftKanExtension_of_iso (isoWhiskerRight (leftKanExtensionUnique F' α F'' α') G)
      (whiskerRight α G ≫ (Functor.associator _ _ _).hom) (whiskerRight α' G ≫ (Functor.associator _ _ _).hom)
      (by ext x; simp [← G.map_comp])

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