hasPointwiseLeftKanExtensionAt_iff_of_equivalence

English

hasPointwiseLeftKanExtensionAt is invariant under equivalence of L and L' with appropriate isomorphisms.

Русский

hasPointwiseLeftKanExtensionAt инвариантно по отношению к эквивалентности L и L' с соответствующими изоморфизмами.

LaTeX

$$$\\text{hasPointwiseLeftKanExtensionAt}_L^F(Y) \\leftrightarrow \\text{hasPointwiseLeftKanExtensionAt}_{L'}^F(Y)$$$

Lean4

theorem hasPointwiseLeftKanExtensionAt_iff_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
  constructor
  · intro
    exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e
  · intro
    exact
      hasPointwiseLeftKanExtensionAt_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)

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