mathlib documentation

category_theory.limits.yoneda

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

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.

Equations
@[simp]
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), punit.star) X X_1 ᾰ)
@[instance]

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

Equations
@[instance]

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

Equations