English
A canonical inverse of the Yoneda–colimit comparison is given by a specified composite.
Русский
Задан канонический обратный пределу–колимиту элемент через заданное композиционное отображение.
LaTeX
$$$\big((\mathrm{yonedaYonedaColimit} F).\mathrm{app}(\mathrm{op} X)\big).\mathrm{inv} = (\mathrm{colimitObjIsoColimitCompEvaluation}\ _\ _).\mathrm{hom} \circ (\mathrm{colimit.post} F (\mathrm{coyoneda.obj}(\mathrm{op}(\mathrm{yoneda.obj} X))))$$$
Lean4
theorem yonedaYonedaColimit_app_inv {X : C} :
((yonedaYonedaColimit F).app (op X)).inv =
(colimitObjIsoColimitCompEvaluation _ _).hom ≫ (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) :=
by
dsimp [yonedaYonedaColimit]
simp only [Iso.cancel_iso_hom_left]
apply colimit.hom_ext
intro j
rw [colimit.ι_post, ι_colimMap_assoc]
simp only [← CategoryTheory.Functor.assoc, comp_evaluation]
rw [ι_preservesColimitIso_inv_assoc, ← Functor.map_comp_assoc]
simp only [← comp_evaluation]
rw [colimitObjIsoColimitCompEvaluation_ι_inv, whiskerLeft_app]
ext η Y f
simp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, FunctorToTypes.colimit.map_ι_apply, map_yonedaEquiv]
