isLeftKanExtensionAlongEquivalence

English

If α is an isomorphism F₀ ≅ L.functor ⋙ F₁ with L an equivalence, then F₁ is left Kan extension of α.hom along F₀.

Русский

Если α является изоморфизмом F₀ ≅ L.functor ⋙ F₁ с L эквивалентностью, то F₁ является левым каноновым расширением α.hom вдоль F₀.

LaTeX

$$$F_1.IsLeftKanExtension\\ α.hom$$$

Lean4

instance isLeftKanExtensionAlongEquivalence (α : F₀ ≅ L.functor ⋙ F₁) : F₁.IsLeftKanExtension α.hom :=
  by
  refine ⟨⟨?_⟩⟩
  apply LeftExtension.isUniversalPostcomp₁Equiv (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
  refine IsInitial.ofUniqueHom (fun y ↦ StructuredArrow.homMk <| α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ?_
  intro y m
  ext x
  simpa using α.inv.app x ≫= congr_app m.w.symm x

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