Colimit of representables #
In this file, We show that every presheaf of types on a category C (with Category.{v₁} C)
is a colimit of representables. This result is also known as the density theorem,
the co-Yoneda lemma and the Ninja Yoneda lemma. Three formulations are given:
colimitOfRepresentableuses the category of elements of a functor to types;isColimitTautologicalCoconeuses the category of costructured arrows foryoneda : C ⥤ Cᵒᵖ ⥤ Type v₁;isColimitTautologicalCocone'uses the category of costructured arrows foruliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁, when the presheaf has values inType (max w v₁);
In this file, we also study the left Kan extensions of functors A : C ⥤ ℰ
along the Yoneda embedding uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂
(when Category.{v₂} ℰ and w is an auxiliary universe). In particular,
the definition uliftYonedaAdjunction shows that such a pointwise left Kan
extension (which exists when ℰ has colimits) is a left adjoint to the
functor restrictedULiftYoneda : ℰ ⥤ Cᵒᵖ ⥤ Type (max w v₁ v₂).
In the lemma isLeftKanExtension_along_uliftYoneda_iff, we show that
if L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ and α : A ⟶ uliftYoneda ⋙ L, then
α makes L the left Kan extension of L along yoneda if and only if
α is an isomorphism (i.e. L extends A) and L preserves colimits.
uniqueExtensionAlongULiftYoneda shows uliftYoneda.leftKanExtension A is
unique amongst functors preserving colimits with this property, establishing the
presheaf category as the free cocompletion of a category.
Given a functor F : C ⥤ D, we also show construct an isomorphism
compULiftYonedaIsoULiftYonedaCompLan : F ⋙ uliftYoneda ≅ uliftYoneda ⋙ F.op.lan, and
show that it makes F.op.lan a left Kan extension of F ⋙ uliftYoneda.
Tags #
colimit, representable, presheaf, free cocompletion
References #
- [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
- https://ncatlab.org/nlab/show/Yoneda+extension
Given a functor A : C ⥤ ℰ (with Category.{v₂} ℰ) and a auxiliary universe w,
this is the functor ℰ ⥤ Cᵒᵖ ⥤ Type (max w v₂) which sends (E : ℰ) (c : Cᵒᵖ)
to the homset A.obj C ⟶ E (considered in the higher universe max w v₂).
Under the existence of a suitable pointwise left Kan extension, it is shown in
uliftYonedaAdjunction that this functor has a left adjoint.
Defined as in [MM92], Chapter I, Section 5, Theorem 2.
Equations
- CategoryTheory.Presheaf.restrictedULiftYoneda A = CategoryTheory.uliftYoneda.{?u.38, ?u.36, ?u.34}.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type (max ?u.38 ?u.36))).obj A.op)
Instances For
Auxiliary definition for restrictedULiftYonedaHomEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for uliftYonedaAdjunction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If L : (Cᵒᵖ ⥤ Type max v₁ v₂) ⥤ ℰ is a pointwise left Kan extension
of a functor A : C ⥤ ℰ along the Yoneda embedding,
then L is a left adjoint of restrictedULiftYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type max v₁ v₂
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any left Kan extension along the Yoneda embedding preserves colimits.
See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
A pointwise left Kan extension along the Yoneda embedding is an extension.
Equations
Instances For
Given P : Cᵒᵖ ⥤ Type max w v₁, this is the functor from the opposite category
of the category of elements of X which sends an element in P.obj (op X) to the
presheaf represented by X. The definitioncoconeOfRepresentable
gives a cocone for this functor which is a colimit and has point P.
Equations
Instances For
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.Presheaf.coconeOfRepresentable P = { pt := P, ι := { app := fun (x : P.Elementsᵒᵖ) => CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd, naturality := ⋯ } }
Instances For
The legs of the cocone coconeOfRepresentable are natural in the choice of presheaf.
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
- One or more equations did not get rendered due to their size.
Instances For
Show that uliftYoneda.leftKanExtension A 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
If L preserves colimits and ℰ has them, then it is a left adjoint. Note this is a (partial)
converse to leftAdjointPreservesColimits.
Equations
- One or more equations did not get rendered due to their size.
Given F : C ⥤ D and X : C, yoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type _ is the
left Kan extension of yoneda.obj X : Cᵒᵖ ⥤ Type _ along F.op.
Equations
- One or more equations did not get rendered due to their size.
Given F : C ⥤ D and X : C, uliftYoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type (max w v₁ v₂) is the
left Kan extension of uliftYoneda.obj X : Cᵒᵖ ⥤ Type (max w v₁ v₂) along F.op.
F ⋙ uliftYoneda is naturally isomorphic to uliftYoneda ⋙ F.op.lan.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for presheafHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ (Dᵒᵖ ⥤ Type max w v₁ v₂),
and a natural transformation φ : F ⋙ uliftYoneda ⟶ uliftYoneda ⋙ G, this is the
(natural) morphism P ⟶ F.op ⋙ G.obj P for all P : Cᵒᵖ ⥤ Type max w v₁ v₂ that is
determined by φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ (Dᵒᵖ ⥤ Type max w v₁ v₂),
and a natural transformation φ : F ⋙ uliftYoneda ⟶ uliftYoneda ⋙ G, this is
the canonical natural transformation F.op.lan ⟶ G, which is part of the
fact that F.op.lan : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂
is the left Kan extension of F ⋙ uliftYoneda : C ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂
along uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a functor F : C ⥤ D, this definition is part of the verification that
Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom
is universal, i.e. that F.op.lan : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂
is the left Kan extension of F ⋙ uliftYoneda : C ⥤ Dᵒᵖ ⥤ Type max w v₁ v₂
along uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Given a functor F : C ⥤ D, F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the
left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.
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. (In this version, we allow the presheaf P to have values in
a larger universe.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
The tautological cocone with point P is a colimit cocone, exhibiting P as a colimit of
representables. (In this version, we allow the presheaf P to have values in
a larger universe.)
Proposition 2.6.3(i) in [Kashiwara2006]
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- CategoryTheory.Presheaf.tautologicalCocone P = { pt := P, ι := { app := fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) => X.hom, naturality := ⋯ } }
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
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]
Alias of CategoryTheory.Presheaf.restrictedULiftYoneda.
Given a functor A : C ⥤ ℰ (with Category.{v₂} ℰ) and a auxiliary universe w,
this is the functor ℰ ⥤ Cᵒᵖ ⥤ Type (max w v₂) which sends (E : ℰ) (c : Cᵒᵖ)
to the homset A.obj C ⟶ E (considered in the higher universe max w v₂).
Under the existence of a suitable pointwise left Kan extension, it is shown in
uliftYonedaAdjunction that this functor has a left adjoint.
Defined as in [MM92], Chapter I, Section 5, Theorem 2.
Instances For
Alias of CategoryTheory.Presheaf.isExtensionAlongULiftYoneda.
A pointwise left Kan extension along the Yoneda embedding is an extension.
Equations
Instances For
Alias of CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff.
Alias of CategoryTheory.Presheaf.uliftYonedaAdjunction.
If L : (Cᵒᵖ ⥤ Type max v₁ v₂) ⥤ ℰ is a pointwise left Kan extension
of a functor A : C ⥤ ℰ along the Yoneda embedding,
then L is a left adjoint of restrictedULiftYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type max v₁ v₂
Instances For
Alias of CategoryTheory.Presheaf.uniqueExtensionAlongULiftYoneda.
Show that uliftYoneda.leftKanExtension A 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.