English
There is an instance asserting that the left Kan extension functor along the opposite Yoneda construction gives a left Kan extension for the composite morphism.
Русский
Существует экземпляр, утверждающий, что левое Kan-расширение вдоль противоположного Yoneda-расширения задаёт левое Kan-расширение для композитного отображения.
LaTeX
$$$$ F.op.lan.IsLeftKanExtension (compULiftYonedaIsoULiftYonedaCompLan F).hom $$$$
Lean4
/-- Given a functor `F : I ⥤ C`, a cocone `c` on `F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v₁` induces a
functor `I ⥤ CostructuredArrow yoneda c.pt` which maps `i : I` to the leg
`yoneda.obj (F.obj i) ⟶ c.pt`. If `c` is a colimit cocone, then that functor is
final.
Proposition 2.6.3(ii) in [Kashiwara2006] -/
theorem final_toCostructuredArrow_comp_pre {c : Cocone (F ⋙ yoneda)} (hc : IsColimit c) :
Functor.Final (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) :=
by
apply Functor.final_of_isTerminal_colimit_comp_yoneda
suffices
IsTerminal
(colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
by
apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
apply IsTerminal.ofIso this
refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
apply HasColimit.isoOfNatIso
exact Functor.isoWhiskerLeft _ (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse
apply IsTerminal.ofIso Over.mkIdTerminal
let isc : IsColimit ((Over.forget _).mapCocone _) :=
isColimitOfPreserves _
(colimit.isColimit
((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
exact Over.isoMk (hc.coconePointUniqueUpToIso isc) (hc.hom_ext fun i => by simp)
