ranCompIsoOfPreserves — Mathlib

Lean4
/-- Commuting a functor that preserves right Kan extensions with the `ran` functor. -/
@[simps!]
def ranCompIsoOfPreserves [G.PreservesRightKanExtensions L] [∀ F : A ⥤ B, HasRightKanExtension L F]
    [∀ F : A ⥤ D, HasRightKanExtension L F] :
    L.ran ⋙ (whiskeringRight _ _ _).obj G ≅ (whiskeringRight _ _ _).obj G ⋙ L.ran :=
  NatIso.ofComponents (fun F ↦ rightKanExtensionCompIsoOfPreserves _ _ _)
    (fun {F F'} η ↦
      by
      apply hom_ext_of_isRightKanExtension (L.rightKanExtension <| F' ⋙ G) (L.rightKanExtensionCounit <| F' ⋙ G)
      dsimp [ran]
      ext
      simp only [comp_obj, Category.assoc, rightKanExtensionCompIsoOfPreserves_hom_fac, NatTrans.comp_app,
        whiskerLeft_app, whiskerRight_app, associator_inv_app, Category.id_comp, liftOfIsRightKanExtension_fac,
        rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, ← G.map_comp]
      simp)
Похожие утверждения