# mathlibdocumentation

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.

def category_theory.coyoneda.colimit_cocone {C : Type v} (X : Cᵒᵖ) :

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

Equations
@[simp]
theorem category_theory.coyoneda.colimit_cocone_X {C : Type v} (X : Cᵒᵖ) :
@[simp]
theorem category_theory.coyoneda.colimit_cocone_ι_app {C : Type v} (X : Cᵒᵖ) (X_1 : C) (ᾰ : X_1) :
= id (λ (ᾰ : X_1), id (λ (X : Cᵒᵖ) (X_1 : C) (ᾰ : X_1), punit.star) X X_1 ᾰ)

The proposed colimit cocone over coyoneda.obj X is a colimit cocone.

Equations
@[simp]
@[protected, instance]
noncomputable def category_theory.coyoneda.colimit_coyoneda_iso {C : Type v} (X : Cᵒᵖ) :

The colimit of coyoneda.obj X is isomorphic to punit.

Equations
@[protected, instance]
def category_theory.yoneda_preserves_limits {C : Type u} (X : C) :

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

Equations
@[protected, instance]

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

Equations
def category_theory.yoneda_jointly_reflects_limits {C : Type u} (J : Type w) (K : J Cᵒᵖ) (t : Π (X : C), ) :

The yoneda embeddings jointly reflect limits.

Equations
def category_theory.coyoneda_jointly_reflects_limits {C : Type u} (J : Type w) (K : J C) (t : Π (X : Cᵒᵖ), ) :

The coyoneda embeddings jointly reflect limits.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations