instHasColimitObjOppositeFunctorTypeCoyoneda

English

For any X in Cᵒᵖ, the functor coyoneda.obj X has a colimit in Type: HasColimit (coyoneda.obj X).

Русский

Для любого X в Cᵒᵖ уFunctorCoyoneda.obj X существует колимит в Type: HasColimit (coyoneda.obj X).

LaTeX

$$$\\forall X:\\text{Opposite}(C),\\; \\mathrm{HasColimit}(\\mathrm{coyoneda.obj} X)$$$

Lean4

instance (X : Cᵒᵖ) : HasColimit (coyoneda.obj X) :=
  HasColimit.mk
    { cocone := _
      isColimit := colimitCoconeIsColimit X }

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