English
The hom component of the colimit-Hom iso with Yoneda yields a π-map: (colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ yoneda) i = coyoneda.map (colimit.ι F ⟨i⟩).op.
Русский
Гом-компонента изоморфизма colimitHomIsoLimitYoneda' с Yoneda даёт отображение π: (colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (...) i = coyoneda.map (...).op.
LaTeX
$$$(\operatorname{colimitHomIsoLimitYoneda'} F A).{\rm hom} \\; \; \circ \; \operatorname{limit}.\pi (F.rightOp \circ yoneda) i = \operatorname{coyoneda.map}(\operatorname{colimit.ι} F \langle i \rangle).op$$$
Lean4
@[reassoc (attr := simp)]
theorem colimitHomIsoLimitYoneda'_hom_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
(colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ 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_π]
