English
Assuming PreservesRightKanExtension G F L and L HasRightKanExtension F, the hom-fac of the preserving iso commutes with counits via associator and whiskerRight as stated.
Русский
Пусть G сохраняет правое Кан-расширение F вдоль L, и у L есть правое Кан-расширение F. Соотношение гом-фактора сохраняющего изоморфизма commute с counit через ассоциатор и whiskerRight.
LaTeX
$$$[PreservesRightKanExtension G F L] \\land [L.HasRightKanExtension F] \\Rightarrow\\ \\text{whiskerLeft } L (rightKanExtensionCompIsoOfPreserves G F L)^{\\mathrm{hom}} \\circ (L.rightKanExtensionCounit (F \\cdot G)) = (Functor.associator _ _ _).\\mathrm{inv} \\circ \\mathrm{whiskerRight}(L.rightKanExtensionCounit F, G).$$$
Lean4
@[reassoc (attr := simp)]
theorem rightKanExtensionCompIsoOfPreserves_hom_fac :
whiskerLeft L (rightKanExtensionCompIsoOfPreserves G F L).hom ≫ (L.rightKanExtensionCounit <| F ⋙ G) =
(Functor.associator _ _ _).inv ≫ whiskerRight (L.rightKanExtensionCounit F) G :=
by simp [rightKanExtensionCompIsoOfPreserves]
