English
For a diagram F and A object of C, the hom component of the Yoneda-based isomorphism from colimit to Yoneda equals the coyoneda-map of the colimit injections, observed through the right op evaluation.
Русский
Для диаграммы F и объекта A конпользование гом-части изоморфизма, связывающего колимит с Yoneda, равняется отображению coyoneda от инъекций колимита после применения F.rightOp.
LaTeX
$$$ (\text{colimitHomIsoLimitYoneda}(F,A)).hom \circ \mathrm{limit}.π( F.op \circ Coyoneda.obj A, i ) = (\mathrm{coyoneda}.map(\mathrm{colimit}.ι F i).op).app A. $$$
Lean4
@[reassoc (attr := simp)]
theorem colimitHomIsoLimitYoneda_hom_comp_π [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) :
(colimitHomIsoLimitYoneda F A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) ⟨i⟩ = (coyoneda.map (colimit.ι F i).op).app A :=
by
simp only [colimitHomIsoLimitYoneda, Iso.trans_hom, Iso.app_hom, Category.assoc]
erw [limitObjIsoLimitCompEvaluation_hom_π]
change ((coyonedaOpColimitIsoLimitCoyoneda F).hom ≫ _).app A = _
rw [coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π]
