English
Analogous statement for D : Iᵒᵖ ⥤ C and F : Cᵒᵖ ⥤ Type: the π-component for the right-op version matches the Yoneda evaluation at op i.
Русский
Аналогичное утверждение для D : Iᵒᵖ ⥤ C и F : Cᵒᵖ ⥤ Type: компонент π для версии справа-определённой совпадает с оценкой Йонеда в op i.
LaTeX
$$$\\text{colimitYonedaHomIsoLimitRightOp } D F$ gives π: $\\lim\\_\\pi(D^{rightOp} \\to F) = ⟨f.app(op i), (\\text{colimit.ι}(D \\to yoneda) (op i)).app(op(D.obj i)) (𝟙(D.obj i))\\rangle$$$
Lean4
@[simp]
theorem colimitYonedaHomIsoLimitOp_π_apply (f : colimit (D ⋙ yoneda) ⟶ F) (i : Iᵒᵖ) :
limit.π (D.op ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitYonedaHomIsoLimitOp D F).hom f) =
⟨f.app (op (D.obj i.unop)) ((colimit.ι (D ⋙ yoneda) i.unop).app (op (D.obj i.unop)) (𝟙 (D.obj i.unop)))⟩ :=
haveI : HasColimit (D.op.unop ⋙ yoneda) := inferInstanceAs <| HasColimit (D ⋙ yoneda)
colimitYonedaHomIsoLimit_π_apply _ _ _ _
