mathlib3 documentation


Colimit of representables #

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

This file constructs an adjunction yoneda_adjunction between (Cᵒᵖ ⥤ Type u) and given a functor A : C ⥤ ℰ, where the right adjoint sends (E : ℰ) to c ↦ (A.obj c ⟶ E) (provided has colimits).

This adjunction is used to show that every presheaf is a colimit of representables.

Further, the left adjoint colimit_adj.extend_along_yoneda : (Cᵒᵖ ⥤ Type u) ⥤ ℰ satisfies yoneda ⋙ L ≅ A, that is, an extension of A : C ⥤ ℰ to (Cᵒᵖ ⥤ Type u) ⥤ ℰ through yoneda : C ⥤ Cᵒᵖ ⥤ Type u. It is the left Kan extension of A along the yoneda embedding, sometimes known as the Yoneda extension, as proved in extend_along_yoneda_iso_Kan.

unique_extension_along_yoneda shows extend_along_yoneda is unique amongst cocontinuous functors with this property, establishing the presheaf category as the free cocompletion of a small category.

Tags #

colimit, representable, presheaf, free cocompletion

References #

theorem category_theory.colimit_adj.restricted_yoneda_map_app {C : Type u₁} [category_theory.small_category C] {ℰ : Type u₂} [category_theory.category ℰ] (A : C ℰ) (_x _x_1 : ℰ) (f : _x _x_1) (X : Cᵒᵖ) (ᾰ : (category_theory.yoneda.obj _x).obj (A.op.obj X)) :

The functor taking (E : ℰ) (c : Cᵒᵖ) to the homset (A.obj C ⟶ E). It is shown in L_adjunction that this functor has a left adjoint (provided E has colimits) given by taking colimits over categories of elements. In the case where ℰ = Cᵒᵖ ⥤ Type u and A = yoneda, this functor is isomorphic to the identity.

Defined as in [MM92], Chapter I, Section 5, Theorem 2.

theorem category_theory.colimit_adj.restricted_yoneda_obj_map {C : Type u₁} [category_theory.small_category C] {ℰ : Type u₂} [category_theory.category ℰ] (A : C ℰ) (X : ℰ) (_x _x_1 : Cᵒᵖ) (f : _x _x_1) (ᾰ : (category_theory.yoneda.obj X).obj (A.op.obj _x)) :

The functor restricted_yoneda is isomorphic to the identity functor when evaluated at the yoneda embedding.


(Implementation). The equivalence of homsets which helps construct the left adjoint to colimit_adj.restricted_yoneda. It is shown in restrict_yoneda_hom_equiv_natural that this is a natural bijection.


(Implementation). Show that the bijection in restrict_yoneda_hom_equiv is natural (on the right).

The left adjoint to the functor restricted_yoneda (shown in yoneda_adjunction). It is also an extension of A along the yoneda embedding (shown in is_extension_along_yoneda), in particular it is the left Kan extension of A through the yoneda embedding.

Instances for category_theory.colimit_adj.extend_along_yoneda

The initial object in the category of elements for a representable functor. In is_initial it is shown that this is initial.

theorem category_theory.comp_yoneda_iso_yoneda_comp_Lan_inv_app_app {C : Type u₁} [category_theory.small_category C] {D : Type u₁} [category_theory.small_category D] (F : C D) (X : C) (X_1 : Dᵒᵖ) (ᾰ : ((category_theory.yoneda category_theory.Lan F.op).obj X).obj X_1) :

A functor to the presheaf category in which everything in the image is representable (witnessed by the fact that it factors through the yoneda embedding). cocone_of_representable gives a cocone for this functor which is a colimit and has point P.


This is a cocone with point P for the functor functor_to_representables P. It is shown in colimit_of_representable P that this cocone is a colimit: that is, we have exhibited an arbitrary presheaf P as a colimit of representables.

The construction of [MM92], Chapter I, Section 5, Corollary 3.


The legs of the cocone cocone_of_representable are natural in the choice of presheaf.

The cocone with point P given by the_cocone is a colimit: that is, we have exhibited an arbitrary presheaf P as a colimit of representables.

The result of [MM92], Chapter I, Section 5, Corollary 3.