English
There is an equivalence between morphisms from the colimit of F ⋙ yoneda to G and the limit of F.op ⋙ G.
Русский
Существует эквиваленция между гомоморфизмами от колимита F ⋙ yoneda к G и пределами F.op ⋙ G.
LaTeX
$$$\text{colimitYonedaHomEquiv }\; F\; G : (\mathrm{colimit}(F \cdot \mathrm{yoneda}) \to G) \simeq \mathrm{limit}(F^{op} \cdot G)$$$
Lean4
/-- Variant of `colimitYonedaHomIsoLimitOp`: natural transformations with domain
`colimit (F ⋙ yoneda)` are equivalent to a limit in a lower universe. -/
noncomputable def colimitYonedaHomEquiv : (colimit (F ⋙ yoneda) ⟶ G) ≃ limit (F.op ⋙ G) :=
Equiv.symm <|
Equiv.ulift.symm.trans <|
Equiv.symm <|
Iso.toEquiv <|
calc
(colimit (F ⋙ yoneda) ⟶ G) ≅ limit (F.op ⋙ G ⋙ uliftFunctor.{u}) := colimitYonedaHomIsoLimitOp _ _
_ ≅ limit ((F.op ⋙ G) ⋙ uliftFunctor.{u}) := (HasLimit.isoOfNatIso (Functor.associator _ _ _).symm)
_ ≅ uliftFunctor.{u}.obj (limit (F.op ⋙ G)) := (preservesLimitIso _ _).symm
