instPreservesColimitFunctorOppositeTypeObjCoyonedaOpYoneda

English

For any functor F, F preserves the colimit of coyoneda of yoneda X.

Русский

Для любого функторa F сохраняется колимитCoyoneda(yoneda X).

LaTeX

$$$\mathrm{PreservesColimit}\; F\; (\mathrm{coyoneda}.\mathrm{obj} (\mathrm{yoneda.obj} X))$$$

Lean4

noncomputable instance {X : C} : PreservesColimit F (coyoneda.obj (op (yoneda.obj X))) :=
  by
  suffices IsIso (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) from preservesColimit_of_isIso_post _ _
  suffices
    colimit.post F (coyoneda.obj (op (yoneda.obj X))) =
      (colimitObjIsoColimitCompEvaluation _ _).inv ≫ ((yonedaYonedaColimit F).app (op X)).inv
    from this ▸ inferInstance
  rw [yonedaYonedaColimit_app_inv, Iso.inv_hom_id_assoc]

Похожие утверждения