English
Let E be an equivalence between categories D and D', together with a pair of compatible functors L : C → D and L' : C → D' linked by the given equivalence. If L has a pointwise right Kan extension at Y with respect to F, then L' has a pointwise right Kan extension at Y' with respect to F (where Y' corresponds to Y under the equivalence).
Русский
Пусть E: D ≃ D' дана эквивалентностью между категориями D и D', и связанные с ней функторы L : C → D, L' : C → D'; если у L существует точечное правое Каново продолжение относительно F в точке Y, тогда у L' существует точное правое каново продолжение относительно F в точке Y', причём Y' соответствует Y через эквивалентность E.
LaTeX
$$$\\text{HasPointwiseRightKanExtensionAt}(L', F, Y') \\quad\\text{при условии} \\quad E : D \\simeq D',\\ e_L : L \\circ E.functor \\cong L',\\ e : E.functor.obj(Y) \\cong Y',\\ [\\text{HasPointwiseRightKanExtensionAt}(L, F, Y)].$$$
Lean4
theorem hasPointwiseRightKanExtensionAt_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
rw [← hasPointwiseRightKanExtensionAt_iff_of_natIso F eL, hasPointwiseRightKanExtensionAt_iff_of_iso _ F e.symm]
let Φ := StructuredArrow.post Y L E.functor
have : HasLimit ((asEquivalence Φ).functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
(inferInstance : HasPointwiseRightKanExtensionAt L F Y)
exact hasLimit_of_equivalence_comp (asEquivalence Φ)
