hasPointwiseLeftKanExtensionAt_of_equivalence

English

Under equivalence E, substitution of L by an equivalent functor preserves the left Kan extension property for F.

Русский

При эквивалентности E замена L на эквивалентный функтор сохраняет свойство левого канонического расширения для F.

LaTeX

$$$\\text{hasPointwiseLeftKanExtensionAt}$ invariance under equivalence$$

Lean4

theorem hasPointwiseLeftKanExtensionAt_of_equivalence (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D')
    (e : E.functor.obj Y ≅ Y') [HasPointwiseLeftKanExtensionAt L F Y] : HasPointwiseLeftKanExtensionAt L' F Y' :=
  by
  rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso F eL, hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]
  let Φ := CostructuredArrow.post L E.functor Y
  have : HasColimit ((asEquivalence Φ).functor ⋙ CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
  exact hasColimit_of_equivalence_comp (asEquivalence Φ)

Похожие утверждения