English
For D : I ⥤ C and F : Cᵒᵖ ⥤ Type, with HasColimit (D ⋙ coyoneda) and HasLimitsOfShape (Iᵒᵖ), the π-component of the limit along D.leftOp yields the evaluation f.app at D.obj i with the corresponding ι map.
Русский
Для D : I ⥤ C и F : Cᵒᵖ ⥤ Type, имея HasColimit (D ⋙ coyoneda) и HasLimitsOfShape (Iᵒᵖ), компоненту π предела вдоль D.leftOp отображает оценку f.app на D.obj i с соответствующим отображением ι.
LaTeX
$$$\\text{colimitCoyonedaHomIsoLimitLeftOp } D F$ gives π-apply: $\\lim\\_\\pi(D^{op} \\to F) = ⟨f.app(D.obj i).unop, (\\text{colimit.ι}(D \\to coyoneda) i).app(D.obj i) (𝟙(D.obj i)) \\rangle$$$
Lean4
@[simp]
theorem colimitCoyonedaHomIsoLimitLeftOp_π_apply (f : colimit (D ⋙ coyoneda) ⟶ F) (i : I) :
limit.π (D.leftOp ⋙ F ⋙ uliftFunctor.{u₁}) (op i) ((colimitCoyonedaHomIsoLimitLeftOp D F).hom f) =
⟨f.app (D.obj i).unop ((colimit.ι (D ⋙ coyoneda) i).app (D.obj i).unop (𝟙 (D.obj i).unop))⟩ :=
haveI : HasColimit (D.leftOp.rightOp ⋙ coyoneda) := inferInstanceAs <| HasColimit (D ⋙ coyoneda)
colimitCoyonedaHomIsoLimit_π_apply _ _ _ _
