isRightKanExtensionAlongEquivalence

English

If α : L.functor ⋙ F₁ ≅ F₀ with L an equivalence, then F₁.IsRightKanExtension α.hom.

Русский

Если α : L.functor ⋙ F₁ ≅ F₀ и L — эквивалентность, то F₁.IsRightKanExtension α.hom.

LaTeX

$$$F_1.IsRightKanExtension\\alpha.hom$$$

Lean4

instance isRightKanExtensionAlongEquivalence (α : L.functor ⋙ F₁ ≅ F₀) : F₁.IsRightKanExtension α.hom :=
  by
  refine ⟨⟨?_⟩⟩
  apply RightExtension.isUniversalPostcomp₁Equiv (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun
  refine IsTerminal.ofUniqueHom (fun y ↦ CostructuredArrow.homMk <| y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ?_
  intro y m
  ext x
  simpa using congr_app m.w x =≫ α.inv.app x

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