# Colimit of representables #

This file constructs an adjunction yonedaAdjunction 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. This result is also known as the density theorem, the co-Yoneda lemma and the Ninja Yoneda lemma.

Further, the left adjoint colimitAdj.extendAlongYoneda : (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 extendAlongYonedaIsoKan.

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

We also give a direct pedestrian proof that every presheaf is a colimit of representables. This version of the proof is valid for any category C, even if it is not small.

## Tags #

colimit, representable, presheaf, free cocompletion

## References #

• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
• https://ncatlab.org/nlab/show/Yoneda+extension
@[simp]
theorem CategoryTheory.ColimitAdj.restrictedYoneda_obj_obj {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) (X : Cᵒᵖ) :
().obj X = (A.obj X.unop X✝)
@[simp]
theorem CategoryTheory.ColimitAdj.restrictedYoneda_obj_map {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
∀ {X_1 Y : Cᵒᵖ} (f : X_1 Y) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ().map f a = CategoryTheory.CategoryStruct.comp (A.map f.unop) a
@[simp]
theorem CategoryTheory.ColimitAdj.restrictedYoneda_map_app {C : Type u₁} {ℰ : Type u₂} [] (A : ) :
∀ {X Y : } (f : X Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ().app X_1 a =
def CategoryTheory.ColimitAdj.restrictedYoneda {C : Type u₁} {ℰ : Type u₂} [] (A : ) :

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.

Equations
• = CategoryTheory.yoneda.comp (().obj A.op)
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.ColimitAdj.restrictYonedaHomEquiv {C : Type u₁} {ℰ : Type u₂} [] (A : ) (P : ) (E : ) {c : CategoryTheory.Limits.Cocone (.leftOp.comp A)} :
(c.pt E) (P )

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural {C : Type u₁} {ℰ : Type u₂} [] (A : ) (P : ) (E₁ : ) (E₂ : ) (g : E₁ E₂) {c : CategoryTheory.Limits.Cocone (.leftOp.comp A)} (k : c.pt E₁) :

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

noncomputable def CategoryTheory.ColimitAdj.extendAlongYoneda {C : Type u₁} {ℰ : Type u₂} [] (A : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj {C : Type u₁} {ℰ : Type u₂} [] (A : ) (P : ) :
theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj.hom_ext {C : Type u₁} {ℰ : Type u₂} [] (A : ) {X : } {P : } {f : X} {f' : X} (w : ∀ (j : P.Elementsᵒᵖ), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (.leftOp.comp A) j) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (.leftOp.comp A) j) f') :
f = f'
theorem CategoryTheory.ColimitAdj.extendAlongYoneda_map {C : Type u₁} {ℰ : Type u₂} [] (A : ) {X : } {Y : } (f : X Y) :
noncomputable def CategoryTheory.ColimitAdj.yonedaAdjunction {C : Type u₁} {ℰ : Type u₂} [] (A : ) :

Show extendAlongYoneda is left adjoint to restrictedYoneda.

The construction of [MM92], Chapter I, Section 5, Theorem 2.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.ColimitAdj.Elements.initial {C : Type u₁} (A : C) :
(CategoryTheory.yoneda.obj A).Elements

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

Equations
Instances For

Show that Elements.initial A is initial in the category of elements for the yoneda functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.ColimitAdj.isExtensionAlongYoneda {C : Type u₁} {ℰ : Type u₂} [] (A : ) :
CategoryTheory.yoneda.comp A

extendAlongYoneda A is an extension of A to the presheaf category along the yoneda embedding. uniqueExtensionAlongYoneda shows it is unique among functors preserving colimits with this property (up to isomorphism).

The first part of [MM92], Chapter I, Section 5, Corollary 4. See Property 1 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance CategoryTheory.ColimitAdj.instPreservesColimitsFunctorOppositeTypeExtendAlongYoneda {C : Type u₁} {ℰ : Type u₂} [] (A : ) :

See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations
@[simp]
theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp_inv {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
=
@[simp]
theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp_hom {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
noncomputable def CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
((CategoryTheory.lan CategoryTheory.yoneda).obj A).obj X

Show that the images of X after extendAlongYoneda and Lan yoneda are indeed isomorphic. This follows from CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan_hom_app {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
@[simp]
theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan_inv_app {C : Type u₁} {ℰ : Type u₂} [] (A : ) (X : ) :
X =
noncomputable def CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan {C : Type u₁} {ℰ : Type u₂} [] (A : ) :
(CategoryTheory.lan CategoryTheory.yoneda).obj A

Verify that extendAlongYoneda is indeed the left Kan extension along the yoneda embedding.

Equations
Instances For
noncomputable def CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan {C : Type u₁} {D : Type u₁} (F : ) :

extending F ⋙ yoneda along the yoneda embedding is isomorphic to Lan F.op.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan_hom_app {C : Type u₁} {D : Type u₁} (F : ) (X : ) :
X = (((CategoryTheory.Coyoneda.fullyFaithful.whiskeringRight ()ᵒᵖ).isoEquiv.symm (().leftAdjointsCoyonedaEquiv ((CategoryTheory.ColimitAdj.yonedaAdjunction (F.comp CategoryTheory.yoneda)).ofNatIsoRight (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' (().obj F.op))))).hom.app { unop := X }).unop
@[simp]
theorem CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan_inv_app_app {C : Type u₁} {D : Type u₁} (F : ) (X : ) (x : Dᵒᵖ) :
∀ (a : CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram F.op { unop := X }.unop x)), ( X).app x a = CategoryTheory.Limits.colimit.desc () { pt := (CategoryTheory.Limits.colimit (.leftOp.comp (F.comp CategoryTheory.yoneda))).obj x, ι := { app := fun (i : ) => CategoryTheory.CategoryStruct.comp (((((CategoryTheory.ColimitAdj.yonedaAdjunction (F.comp CategoryTheory.yoneda)).ofNatIsoRight (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' (().obj F.op))).homEquiv X (CategoryTheory.Limits.colimit (.leftOp.comp (F.comp CategoryTheory.yoneda)))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (.leftOp.comp (F.comp CategoryTheory.yoneda))))).app i.left) ((CategoryTheory.Limits.colimit (.leftOp.comp (F.comp CategoryTheory.yoneda))).map i.hom), naturality := } } a
@[simp]
theorem CategoryTheory.compYonedaIsoYonedaCompLan_inv_app_app {C : Type u₁} {D : Type u₁} (F : ) (X : C) (X : Dᵒᵖ) :
∀ (a : ((CategoryTheory.yoneda.comp ()).obj X✝).obj X), (.app X✝).app X a = ((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (F.comp CategoryTheory.yoneda)).hom.app X✝).app X (CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram F.op (CategoryTheory.yoneda.obj X✝) X) { pt := (CategoryTheory.Limits.colimit ((CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp.comp (F.comp CategoryTheory.yoneda))).obj X, ι := { app := fun (i : ) => CategoryTheory.CategoryStruct.comp (((((CategoryTheory.ColimitAdj.yonedaAdjunction (F.comp CategoryTheory.yoneda)).ofNatIsoRight (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' (().obj F.op))).homEquiv (CategoryTheory.yoneda.obj X✝) (CategoryTheory.Limits.colimit ((CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp.comp (F.comp CategoryTheory.yoneda)))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit ((CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp.comp (F.comp CategoryTheory.yoneda))))).app i.left) ((CategoryTheory.Limits.colimit ((CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp.comp (F.comp CategoryTheory.yoneda))).map i.hom), naturality := } } a)
@[simp]
theorem CategoryTheory.compYonedaIsoYonedaCompLan_hom_app_app {C : Type u₁} {D : Type u₁} (F : ) (X : C) (X : Dᵒᵖ) :
∀ (a : ((F.comp CategoryTheory.yoneda).obj X✝).obj X), (.app X✝).app X a = (((CategoryTheory.Coyoneda.fullyFaithful.whiskeringRight ()ᵒᵖ).isoEquiv.symm (().leftAdjointsCoyonedaEquiv ((CategoryTheory.ColimitAdj.yonedaAdjunction (F.comp CategoryTheory.yoneda)).ofNatIsoRight (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' (().obj F.op))))).hom.app { unop := CategoryTheory.yoneda.obj X✝ }).unop.app X (((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (F.comp CategoryTheory.yoneda)).inv.app X✝).app X a)
noncomputable def CategoryTheory.compYonedaIsoYonedaCompLan {C : Type u₁} {D : Type u₁} (F : ) :
F.comp CategoryTheory.yoneda CategoryTheory.yoneda.comp ()

F ⋙ yoneda is naturally isomorphic to yoneda ⋙ Lan F.op.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Since extendAlongYoneda A is adjoint to restrictedYoneda A, if we use A = yoneda then restrictedYoneda A is isomorphic to the identity, and so extendAlongYoneda A is as well.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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). coconeOfRepresentable gives a cocone for this functor which is a colimit and has point P.

Equations
• = .leftOp.comp CategoryTheory.yoneda
Instances For
noncomputable def CategoryTheory.coconeOfRepresentable {C : Type u₁} (P : ) :

This is a cocone with point P for the functor functorToRepresentables P. It is shown in colimitOfRepresentable 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.

Equations
• = (CategoryTheory.extendAlongYonedaYoneda.hom.app P)
Instances For
@[simp]
theorem CategoryTheory.coconeOfRepresentable_pt {C : Type u₁} (P : ) :
theorem CategoryTheory.coconeOfRepresentable_ι_app {C : Type u₁} (P : ) (j : P.Elementsᵒᵖ) :
.app j = CategoryTheory.yonedaEquiv.symm j.unop.snd

An explicit formula for the legs of the cocone coconeOfRepresentable.

theorem CategoryTheory.coconeOfRepresentable_naturality {C : Type u₁} {P₁ : } {P₂ : } (α : P₁ P₂) (j : P₁.Elementsᵒᵖ) :
= .app (.obj j)

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

noncomputable def CategoryTheory.colimitOfRepresentable {C : Type u₁} (P : ) :

The cocone with point P given by coconeOfRepresentable 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.

Equations
• = let_fun this := ;
Instances For
noncomputable def CategoryTheory.natIsoOfNatIsoOnRepresentables {C : Type u₁} {ℰ : Type u₂} [] (L₁ : ) (L₂ : ) (h : CategoryTheory.yoneda.comp L₁ CategoryTheory.yoneda.comp L₂) :
L₁ L₂

Given two functors L₁ and L₂ which preserve colimits, if they agree when restricted to the representable presheaves then they agree everywhere.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.uniqueExtensionAlongYoneda {C : Type u₁} {ℰ : Type u₂} [] (A : ) (L : ) (hL : CategoryTheory.yoneda.comp L A) :

Show that extendAlongYoneda is the unique colimit-preserving functor which extends A to the presheaf category.

The second part of [MM92], Chapter I, Section 5, Corollary 4. See Property 3 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.adjunctionOfPreservesColimitsAux {C : Type u₁} {ℰ : Type u₂} [] (L : ) :

Auxiliary definition for isLeftAdjointOfPreservesColimits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.isLeftAdjointOfPreservesColimits {C : Type u₁} {ℰ : Type u₂} [] (L : ) :

If L preserves colimits and ℰ has them, then it is a left adjoint. Note this is a (partial) converse to leftAdjointPreservesColimits.

@[simp]
theorem CategoryTheory.tautologicalCocone_pt {C : Type u₁} [] (P : ) :
@[simp]
theorem CategoryTheory.tautologicalCocone_ι_app {C : Type u₁} [] (P : ) (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) :
.app X = X.hom
def CategoryTheory.tautologicalCocone {C : Type u₁} [] (P : ) :
CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P).comp CategoryTheory.yoneda)

For a presheaf P, consider the forgetful functor from the category of representable presheaves over P to the category of presheaves. There is a tautological cocone over this functor whose leg for a natural transformation V ⟶ P with V representable is just that natural transformation.

Equations
Instances For

The tautological cocone with point P is a colimit cocone, exhibiting P as a colimit of representables.

Proposition 2.6.3(i) in [Kashiwara2006]

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.final_toCostructuredArrow_comp_pre {C : Type u₁} [] {I : Type v₁} (F : ) {c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)} (hc : ) :
(c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre F CategoryTheory.yoneda c.pt)).Final

Given a functor F : I ⥤ C, a cocone c on F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v₁ induces a functor I ⥤ CostructuredArrow yoneda c.pt which maps i : I to the leg yoneda.obj (F.obj i) ⟶ c.pt. If c is a colimit cocone, then that functor is final.

Proposition 2.6.3(ii) in [Kashiwara2006]