English
The inverse side of the Yoneda colimit iso satisfies an inverse-π identity with the right Op Yoneda: (colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F ⟨i⟩).op).app A = limit.π (F.rightOp ⋙ yoneda.obj A) i.
Русский
Обратная сторона изоморфизма Yoneda-колимита удовлетворяет идентификации inverse-π: (colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F ⟨i⟩).op).app A = limit.π (F.rightOp ⋙ yoneda.obj A) i.
LaTeX
$$$(\operatorname{colimitHomIsoLimitYoneda'} F A)^{-1} \; \circ \; (\mathrm{coyoneda.map} (\mathrm{colimit.ι} F \langle i \rangle).op)^{\mathrm{app}} = \operatorname{limit.π}(F.rightOp \circ \mathrm{yoneda.obj} A) i$$$
Lean4
@[reassoc (attr := simp)]
theorem colimitHomIsoLimitYoneda'_inv_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
(colimitHomIsoLimitYoneda' F A).inv ≫ (coyoneda.map (colimit.ι F ⟨i⟩).op).app A =
limit.π (F.rightOp ⋙ yoneda.obj A) i :=
by rw [← colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc, Iso.inv_hom_id, Category.id_comp]
