English
There is a bijection between the properties that L has a pointwise right Kan extension at Y and L' has a pointwise right Kan extension at Y' when Y and Y' are related by an equivalence E.
Русский
Существуют эквивалентности между свойствами: наличие точного правого Кан-расширения у L в точке Y и наличие такового у L' в точке Y', когда Y и Y' связаны эквивалентностью E.
LaTeX
$$$\\text{HasPointwiseRightKanExtensionAt}(L, F, Y) \\ \\Longleftrightarrow\\t\\text{HasPointwiseRightKanExtensionAt}(L', F, Y').$$$
Lean4
theorem hasPointwiseRightKanExtensionAt_iff_of_equivalence (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D')
(e : E.functor.obj Y ≅ Y') : HasPointwiseRightKanExtensionAt L F Y ↔ HasPointwiseRightKanExtensionAt L' F Y' :=
by
constructor
· intro
exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e
· intro
exact
hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
(isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫ isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
(E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
