Colimit of representables #
This file constructs an adjunction Presheaf.yonedaAdjunction
between (Cᵒᵖ ⥤ Type u)
and
ℰ
given a functor A : C ⥤ ℰ
, where the right adjoint restrictedYoneda
sends (E : ℰ)
to c ↦ (A.obj c ⟶ E)
, and the left adjoint (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
is a pointwise left Kan extension of A
along the Yoneda embedding, which
exists provided ℰ
has colimits)
We also 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. Two formulations are given:
colimitOfRepresentable
uses the category of elements of a functor to types;isColimitTautologicalCocone
uses the category of costructured arrows.
In the lemma isLeftKanExtension_along_yoneda_iff
, we show that
if L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ)
and α : A ⟶ yoneda ⋙ 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.
uniqueExtensionAlongYoneda
shows yoneda.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 compYonedaIsoYonedaCompLan : F ⋙ yoneda ≅ yoneda ⋙ F.op.lan
, and
show that it makes F.op.lan
a left Kan extension of F ⋙ yoneda
.
Tags #
colimit, representable, presheaf, free cocompletion
References #
- S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic
- https://ncatlab.org/nlab/show/Yoneda+extension
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 [MLM92], Chapter I, Section 5, Theorem 2.
Equations
- CategoryTheory.Presheaf.restrictedYoneda A = CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type ?u.44)).obj A.op)
Instances For
Auxiliary definition for restrictedYonedaHomEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Auxiliary definition for yonedaAdjunction
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
is a pointwise left Kan extension
of a functor A : C ⥤ ℰ
along the Yoneda embedding,
then L
is a left adjoint of restrictedYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type 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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A pointwise left Kan extension along the Yoneda embedding is an extension.
Equations
- CategoryTheory.Presheaf.isExtensionAlongYoneda A = (CategoryTheory.asIso (CategoryTheory.yoneda.leftKanExtensionUnit A)).symm
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
- CategoryTheory.Presheaf.functorToRepresentables P = (CategoryTheory.CategoryOfElements.π P).leftOp.comp CategoryTheory.yoneda
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 [MLM92], Chapter I, Section 5, Corollary 3.
Equations
- CategoryTheory.Presheaf.coconeOfRepresentable P = { pt := P, ι := { app := fun (x : P.Elementsᵒᵖ) => CategoryTheory.yonedaEquiv.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 [MLM92], Chapter I, Section 5, Corollary 3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Show that yoneda.leftKanExtension A
is the unique colimit-preserving
functor which extends A
to the presheaf category.
The second part of [MLM92], Chapter I, Section 5, Corollary 4. See Property 3 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.
Equations
- CategoryTheory.Presheaf.uniqueExtensionAlongYoneda L e = L.leftKanExtensionUnique e.hom (CategoryTheory.yoneda.leftKanExtension A) (CategoryTheory.yoneda.leftKanExtensionUnit A)
Instances For
Equations
- ⋯ = ⋯
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
- ⋯ = ⋯
F ⋙ yoneda
is naturally isomorphic to yoneda ⋙ 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 v₁) ⥤ (Dᵒᵖ ⥤ Type v₁)
, and
a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G
, this is the
(natural) morphism P ⟶ F.op ⋙ G.obj P
for all P : Cᵒᵖ ⥤ Type 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 v₁) ⥤ (Dᵒᵖ ⥤ Type v₁)
,
and a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G
, this is
the canonical natural transformation F.op.lan ⟶ G
, which is part of the
that 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₁
.
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 (compYonedaIsoYonedaCompLan F).hom
is universal, i.e. that 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₁
.
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₁
.
Equations
- ⋯ = ⋯
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 [KS06]
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 [KS06]