English
If G preserves right Kan extensions and L has a right Kan extension for F, then the inverse iso of the preserving component interacts correctly with counits to give the counit for the composed functor F ⋙ G.
Русский
Если G сохраняет правые Кан-расширения, и у L есть правое Кан-расширение F, то обратная изоморфизм сохраняющего компонента корректно взаимодействует с counit-образами, давая counit для композиции F ⋙ G.
LaTeX
$$$[PreservesRightKanExtension G F L] \\land [L.HasRightKanExtension F] \\Rightarrow\\ Eq\\Big( L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).inv \\circ (L.associator (L.rightKanExtension F) G).inv \\circ (L.whiskerRight (L.rightKanExtensionCounit F) G) , L.rightKanExtensionCounit (F \\cdot G) \\Big).$$$
Lean4
@[reassoc (attr := simp)]
theorem rightKanExtensionCompIsoOfPreserves_inv_fac :
whiskerLeft L (rightKanExtensionCompIsoOfPreserves G F L).inv ≫
((Functor.associator _ _ _).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G) =
(L.rightKanExtensionCounit <| F ⋙ G) :=
by simp [rightKanExtensionCompIsoOfPreserves]
