English
The lift at Y is described by a limit lift along the structured arrow cone.
Русский
Подъем в точке Y задается через предел над структурированным конусом стрелок.
LaTeX
$$$((\text{pointwiseRightKanExtension }L F).\text{liftOfIsRightKanExtension}(\text{pointwiseRightKanExtensionCounit }L F) G \alpha).\mathrm{app} Y = \operatorname{limit.lift} _ (\mathrm{structuredArrowMapCone} L F G \alpha Y)$$$
Lean4
@[simp]
theorem pointwiseRightKanExtension_lift_app (G : D ⥤ H) (α : L ⋙ G ⟶ F) (Y : D) :
((pointwiseRightKanExtension L F).liftOfIsRightKanExtension (pointwiseRightKanExtensionCounit L F) G α |>.app Y) =
limit.lift _ (structuredArrowMapCone L F G α Y) :=
by
let β : G ⟶ L.pointwiseRightKanExtension F := { app := fun Y ↦ limit.lift _ (structuredArrowMapCone L F G α Y) }
have h : (pointwiseRightKanExtension L F).liftOfIsRightKanExtension (pointwiseRightKanExtensionCounit L F) G α = β :=
by
apply hom_ext_of_isRightKanExtension (α := pointwiseRightKanExtensionCounit L F)
aesop
exact NatTrans.congr_app h Y
