module Cat.Functor.Hom.Coyoneda {o h} (C : Precategory o h) where
The Coyoneda Lemmaπ
The Coyoneda lemma is, like its dual, a statement about presheaves. It states that βevery presheaf is a colimit of representablesβ, which, in less abstract terms, means that every presheaf arises as some way of gluing together a bunch of (things isomorphic to) hom functors!
module _ (P : Functor (C ^op) (Sets h)) where private module P = Functor P open El C P open Element open Element-hom
We start by fixing some presheaf , and constructing a colimit whose coapex is . This involves a clever choice of diagram category: specifically, the category of elements of . This may seem like a somewhat odd choice, but recall that the data contained in is the same data as , just melted into a soup of points. The colimit we construct will then glue all those points back together into .
coyoneda : is-colimit (γ Fβ Οβ) P _ coyoneda = to-is-colimit colim where
This is done by projecting out of into via the canonical projection, and then embedding into the category of presheaves over via the yoneda embedding. Concretely, what this diagram gives us is a bunch of copies of the hom functor, one for each . Then, to construct the injection map, we can just use the (contravariant) functorial action of to take a and a to a . This map is natural by functoriality of .
open make-is-colimit module β« = Precategory β« colim : make-is-colimit (γ Fβ Οβ) P colim .Ο x .Ξ· y f = P.Fβ f (x .section) colim .Ο x .is-natural y z f = funext (Ξ» g β happly (P.F-β f g) (x .section)) colim .commutes {x = x} {y = y} f = Nat-path Ξ» z β funext Ξ» g β P.Fβ (f .hom β g) (y .section) β‘β¨ happly (P.F-β g (f .hom)) (y .section) β©β‘ P.Fβ g (P.Fβ (f .hom) (y .section)) β‘β¨ ap (P.Fβ g) (f .commute) β©β‘ P.Fβ g (x .section) β
Now that weβve constructed a cocone, all that remains is to see that
this is a colimiting cocone. Intuitively, it makes sense that
Reassemble
should be colimiting:
all weβve done is taken all the data associated with
and glued it back together. However, proving this does involve futzing
about with various naturality + cocone commuting conditions.
We start by constructing the universal map from into the coapex of some other cocone . The components of this natural transformation are obtained in a similar manner to the yoneda lemma; we bundle up the data to construct an object of , and then apply the function we construct to the identity morphism. Naturality follows from the fact that is a cocone, and the components of are natural.
colim .universal eps _ .Ξ· x px = eps (elem x px) .Ξ· x id colim .universal {Q} eps comm .is-natural x y f = funext Ξ» px β eps (elem y (P.Fβ f px)) .Ξ· y id β‘Λβ¨ (Ξ» i β comm (induce f px) i .Ξ· y id) β©β‘Λ eps (elem x px) .Ξ· y (f β id) β‘β¨ ap (eps (elem x px) .Ξ· y) id-comm β©β‘ eps (elem x px) .Ξ· y (id β f) β‘β¨ happly (eps (elem x px) .is-natural x y f) id β©β‘ Fβ Q f (eps (elem x px) .Ξ· x id) β
Next, we need to show that this morphism factors each of the
components of
.
The tricky bit of the proof here is that we need to use induce to regard f
as a
morphism in the category of elements.
colim .factors {o} eps comm = Nat-path Ξ» x β funext Ξ» f β eps (elem x (P.Fβ f (o .section))) .Ξ· x id β‘Λβ¨ (Ξ» i β comm (induce f (o .section)) i .Ξ· x id) β©β‘Λ eps o .Ξ· x (f β id) β‘β¨ ap (eps o .Ξ· x) (idr f) β©β‘ eps o .Ξ· x f β
Finally, uniqueness: This just follows by the commuting conditions on
Ξ±
.
colim .unique eps comm Ξ± p = Nat-path Ξ» x β funext Ξ» px β Ξ± .Ξ· x px β‘Λβ¨ ap (Ξ± .Ξ· x) (happly P.F-id px) β©β‘Λ Ξ± .Ξ· x (P.Fβ id px) β‘β¨ happly (p _ Ξ·β x) id β©β‘ eps (elem x px) .Ξ· x id β
And thatβs it! The important takeaway here is not the shuffling around of natural transformations required to prove this lemma, but rather the idea that, unlike Humpty Dumpty, if a presheaf falls off a wall, we can put it back together again.
An important consequence of being able to disassemble presheaves into colimits of representables is that representables generate , in that if a pair of natural transformations that agrees on all representables, then all along.
module _ {Y} (f : P => Y) where private module Y = Functor Y open Cocone
The first thing we prove is that any map
of presheaves expresses
as a cocone over
.
The special case Reassemble
above
is this procedure for the identity map β whence we see that coyoneda is essentially a restatement of the
fact that
is initial the coslice category under
.
Mapβcocone-under : Cocone (γ Fβ Οβ) Mapβcocone-under .coapex = Y Mapβcocone-under .Ο (elem ob sect) .Ξ· x i = f .Ξ· x (P.β i sect) Mapβcocone-under .Ο (elem ob sect) .is-natural x y h = funext Ξ» a β f .Ξ· _ (P.β (a β h) sect) β‘β¨ happly (f .is-natural _ _ _) _ β©β‘ Y.β (a β h) (f .Ξ· _ sect) β‘β¨ happly (Y.F-β _ _) _ β©β‘ Y.β h (Y.β a (f .Ξ· _ sect)) β‘Λβ¨ ap (Y .Fβ h) (happly (f .is-natural _ _ _) _) β©β‘Λ Y.β h (f .Ξ· _ (P.β a sect)) β Mapβcocone-under .commutes {x} {y} o = Nat-path Ξ» i β funext Ξ» a β ap (f .Ξ· _) $ P.β (o .hom β a) (y .section) β‘β¨ happly (P.F-β _ _) _ β©β‘ P.β a (P.β (o .hom) (y .section)) β‘β¨ ap (P.Fβ _) (o .commute) β©β‘ P.β a (x .section) β
module _ {X Y : Functor (C ^op) (Sets h)} where private module PSh = Cat.Reasoning (Cat[ C ^op , Sets h ]) module P = Functor X module Y = Functor Y open Cocone-hom open El.Element open Initial open Cocone
We can now prove that, if are two maps such that, for every map with representable domain , , then . The quantifier structure of this sentence is a bit funky, so watch out for the formalisation below:
Representables-generate-presheaf : {f g : X => Y} β (β {A : Ob} (h : γβ A => X) β f PSh.β h β‘ g PSh.β h) β f β‘ g
A map can be seen as a βgeneralised elementβ of , so that the precondition for can be read as β and agree for all generalised elements with domain any representableβ. The proof is deceptively simple: Since is a colimit, it is an initial object in the category of cocones under .
The construction Mapβcocone-under lets us express as a cocone under in a way that becomes a cocone homomorphism ; The condition that agrees with on all generalised elements with representable domains ensures that is also a cocone homomorphism ; But is initial, so !
Representables-generate-presheaf {f} {g} sep = ap hom $ is-contrβis-prop (is-colimitβis-initial-cocone _ (coyoneda X) (Mapβcocone-under X f)) fβ² gβ² where fβ² : Cocone-hom (γ Fβ El.Οβ C X) _ (Mapβcocone-under X f) fβ² .hom = f fβ² .commutes o = Nat-path (Ξ» _ β refl) gβ² : Cocone-hom (γ Fβ El.Οβ C X) _ (Mapβcocone-under X f) gβ² .hom = g gβ² .commutes o = Nat-path Ξ» x β sym (sep $ NT (Ξ» i a β P.β a (o .section)) Ξ» x y h β funext Ξ» a β P.F-β _ _ $β o .section) Ξ·β x
An immediate consequence is that, since any pair of maps in extend to maps , and the functor is fully faithful, two maps in are equal iff. they agree on all generalised elements:
private module _ where private γ-cancelr : β {X Y : Ob} {f g : Hom X Y} β (β {Z} (h : Hom Z X) β f β h β‘ g β h) β f β‘ g γ-cancelr sep = fully-faithfulβfaithful {F = γ} γ-is-fully-faithful $ Representables-generate-presheaf Ξ» h β Nat-path Ξ» x β funext Ξ» a β sep (h .Ξ· x a)
However note that we have eliminated a mosquito using a low-orbit ion cannon:
γ-cancelr : β {X Y : Ob} {f g : Hom X Y} β (β {Z} (h : Hom Z X) β f β h β‘ g β h) β f β‘ g γ-cancelr sep = sym (idr _) β sep id β idr _