English
A precise projection formula expresses the i-th component of colimitYonedaHomEquiv(η) in terms of η.
Русский
Точнаe формула проекции выражает i-й компонент colimitYonedaHomEquiv(η) через η.
LaTeX
$$$\forall F,G,\eta, i:\, \mathrm{limit}.\pi\,(F^{op}\cdot G)\; i\; (\mathrm{colimitYonedaHomEquiv}\ F\ G\ \eta) = \eta.{\rm app}(\mathrm{op}(F.{\rm obj}(i).unop))\Big( (\mathrm{colimit}.ι(F\cdot \ yoneda)\ i.{\rm unop}).{\rm app} _ (\mathbf{1})\Big)$$$
Lean4
@[simp]
theorem colimitYonedaHomEquiv_π_apply (η : colimit (F ⋙ yoneda) ⟶ G) (i : Iᵒᵖ) :
limit.π (F.op ⋙ G) i (colimitYonedaHomEquiv F G η) =
η.app (op (F.obj i.unop)) ((colimit.ι (F ⋙ yoneda) i.unop).app _ (𝟙 _)) :=
by
simp only [Functor.comp_obj, Functor.op_obj, colimitYonedaHomEquiv, uliftFunctor_obj, Iso.trans_def, Iso.trans_assoc,
Iso.toEquiv_comp, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.trans_apply, Iso.toEquiv_fun, Iso.symm_hom,
Equiv.ulift_apply]
have (a : _) := congrArg ULift.down (congrFun (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)
dsimp at this
rw [this, ← types_comp_apply (HasLimit.isoOfNatIso _).hom (limit.π _ _), HasLimit.isoOfNatIso_hom_π]
simp
