English
The app component of the descent map for the left Kan extension coincides with the colimit description of the constructed cocone.
Русский
Компоненту применения спуска для левого кан-расширения соответствует описание через колимитный кокон.
LaTeX
$$$\big((L\text{pointwiseLeftKanExtension }F).\text{descOfIsLeftKanExtension}(L\text{leftKanExtensionUnit}F)G\alpha\big).\mathrm{app}Y = \operatorname{colimit.desc} _ (\mathrm{costructuredArrowMapCocone} L F G \alpha Y)$$$
Lean4
@[simp]
theorem pointwiseLeftKanExtension_desc_app (G : D ⥤ H) (α : F ⟶ L ⋙ G) (Y : D) :
((pointwiseLeftKanExtension L F).descOfIsLeftKanExtension (pointwiseLeftKanExtensionUnit L F) G α |>.app Y) =
colimit.desc _ (costructuredArrowMapCocone L F G α Y) :=
by
let β : L.pointwiseLeftKanExtension F ⟶ G := { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }
have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension (pointwiseLeftKanExtensionUnit L F) G α = β :=
by
apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
aesop
exact NatTrans.congr_app h Y
