pointwiseRightKanExtensionCompIsoOfPreserves

Lean4

/-- Extract an isomorphism
`L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G)` when `G` preserves
right Kan extensions. -/
def pointwiseRightKanExtensionCompIsoOfPreserves [PreservesPointwiseRightKanExtension G F L]
    [L.HasPointwiseRightKanExtension F] : L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G) :=
  rightKanExtensionUnique (L.pointwiseRightKanExtension F ⋙ G)
    ((Functor.associator _ _ _).inv ≫ whiskerRight (L.pointwiseRightKanExtensionCounit F) G)
    (L.pointwiseRightKanExtension <| F ⋙ G) (L.pointwiseRightKanExtensionCounit <| F ⋙ G)

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