English
There is a canonical isomorphism CoyonedaHomIsoLimitUnop relating colimits and coyoneda for unop scenarios, with the π-component described by colimitCoyonedaHomIsoLimitUnop_π_apply.
Русский
Существует каноническое изоморфизм CoyonedaHomIsoLimitUnop, связывающее колимиты иCoyoneda в несопряжённых случаях, π-компонента описывается в colimitCoyonedaHomIsoLimitUnop_π_apply.
LaTeX
$$$\operatorname{colimitCoyonedaHomIsoLimitUnop} \; D \; F \text{ is an isomorphism with } \operatorname{limit}\text{.π applied as in }\text{π_apply}$$$
Lean4
@[simp]
theorem colimitCoyonedaHomIsoLimit_π_apply (f : colimit (D.rightOp ⋙ coyoneda) ⟶ F) (i : I) :
limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) (op i) ((colimitCoyonedaHomIsoLimit D F).hom f) =
⟨f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i))))⟩ :=
by
change ((colimitCoyonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) (op i))) f = _
simp only [colimitCoyonedaHomIsoLimit, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]
dsimp [coyonedaLemma, types_comp_apply]
rfl
