English
Variant of the Yoneda-colimit π-apply for op-structures: the π-component is given by evaluation at D.obj i with the corresponding ι-index.
Русский
Вариант применения π для колиметы в Opposite-структуре: компонент π задаётся оценкой на D.obj i с соответствующим ι.
LaTeX
$$$\\text{colimitYonedaHomIsoLimit'_π_apply } D F\\ (f)\\ i = ⟨f.app(D.obj i) ( (\\text{colimit.ι}(D.op ⋯) i).app(D.obj i) (𝟙(D.obj i)) )\\rangle$$$
Lean4
@[simp]
theorem colimitCoyonedaHomIsoLimit'_π_apply (f : colimit (D.op ⋙ coyoneda) ⟶ F) (i : I) :
limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitCoyonedaHomIsoLimit' D F).hom f) =
⟨f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) ⟨i⟩).app (D.obj i) (𝟙 (D.obj i)))⟩ :=
by
change ((colimitCoyonedaHomIsoLimit' D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _
simp only [colimitCoyonedaHomIsoLimit', Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]
dsimp [coyonedaLemma]
rfl
