# mathlib3documentation

category_theory.limits.yoneda

# 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.

Equations
@[simp]
@[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
@[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]

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