mathlib3 documentation


Limit properties relating to the (co)yoneda embedding. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We calculate the colimit of Y ↦ (X ⟶ Y), which is just punit. (This is used in characterising cofinal functors.)

We also show the (co)yoneda embeddings preserve limits and jointly reflect them.

The colimit cocone over coyoneda.obj X, with cocone point punit.

theorem category_theory.coyoneda.colimit_cocone_ι_app {C : Type v} [category_theory.small_category C] (X : Cᵒᵖ) (X_1 : C) (ᾰ : (category_theory.coyoneda.obj X).obj X_1) :
(category_theory.coyoneda.colimit_cocone X).ι.app X_1 = id (λ (ᾰ : (category_theory.coyoneda.obj X).obj X_1), id (λ (X : Cᵒᵖ) (X_1 : C) (ᾰ : opposite.unop X X_1), X X_1 ᾰ)
@[protected, instance]

The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v for X : C preserves limits.

@[protected, instance]

The coyoneda embedding coyoneda.obj X : C ⥤ Type v for X : Cᵒᵖ preserves limits.