English
The leftOp version of the Coyoneda colimit iso yields a π-apply formula: limit.π (D.leftOp ⋙ F) (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))⟩.
Русский
Левопов версия Coyoneda колимита даёт тождество π: limit.π (D.leftOp ⋙ F) (op i) ((colimitCoyonedaHomIsoLimitLeftOp D F).hom f) = ⟨f.app (D.obj i).unop ...⟩.
LaTeX
$$$\operatorname{limit.\pi}(D.leftOp \circ F \circ \mathrm{uliftFunctor})\{ unop := i \} \bigl(((\text{colimitCoyonedaHomIsoLimitLeftOp } D F).hom f)\bigr) = \langle f.app (D.obj i).unop (\cdot) \rangle$$$
Lean4
@[simp]
theorem colimitYonedaHomIsoLimit_π_apply (f : colimit (D.unop ⋙ yoneda) ⟶ F) (i : Iᵒᵖ) :
limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitYonedaHomIsoLimit D F).hom f) =
⟨f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) i.unop).app (D.obj i) (𝟙 (D.obj i).unop))⟩ :=
by
change ((colimitYonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _
simp only [colimitYonedaHomIsoLimit, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]
dsimp [yonedaLemma]
rfl
