English
Given L: C ⥤ D, L' : C ⥤ D' with an equivalence E : D ≅ D' and iso L → L'. Then if F: C ⥤ H has a pointwise left Kan extension along L, the transformed data along L' yields a left Kan extension along L'.
Русский
При эквивалентности D ≅ D' и L: C ⥤ D, L': C ⥤ D', существует левое каноново расширение вдоль L' если оно существует вдоль L.
LaTeX
$$$\\text{HasPointwiseLeftKanExtensionAt }(L,F,Y) \\Rightarrow \\text{HasPointwiseLeftKanExtensionAt }(L',F,Y').$$$
Lean4
/-- `HasPointwiseLeftKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
theorem hasPointwiseLeftKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
HasPointwiseLeftKanExtensionAt L F Y ↔ HasPointwiseLeftKanExtensionAt L' F Y :=
by
revert L L' e
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y], HasPointwiseLeftKanExtensionAt L' F Y
from fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
intro L L' e _
let Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso _ e.symm
let e' : CostructuredArrow.proj L' Y ⋙ F ≅ Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F := Iso.refl _
exact hasColimit_of_iso e'
