nLab
free cocompletion

Contents

Idea

Passing from a category CC to its presheaf category PSh(C):=[C op,Set]PSh(C) := [C^{op},Set] may be regarded as the operation of “freely adjoining colimits to CC”.

The precise version of this statement is that the Yoneda embedding

Y:CPSh(C) Y : C \hookrightarrow PSh(C)

is the free cocompletion of CC.

The universal property of the Yoneda embedding is expressed in terms of the Yoneda extension of any functor F:CDF : C \to D to a category DD with colimits.

Technical details

The Yoneda embedding

y S:SSet S opy_S: S \to Set^{S^{op}}

of a small category SS into the category Set S opSet^{S^{op}} of presheaves on SS is universal among functors from SS into cocomplete categories, in the sense that given a functor F:SDF: S \to D where DD is cocomplete, there exists a unique (up to isomorphism) cocontinuous extension

F^:Set S opD,\hat{F}: Set^{S^{op}} \to D,

called the Yoneda extension, meaning that F^y SF\hat{F} y_S \cong F and F^\hat{F} preserves small colimits. Indeed, the desired F^\hat{F} is left adjoint to the functor

DSet S op:dhom D(F,d)D \to Set^{S^{op}}: d \mapsto \hom_D(F-, d)

An explicit formula for the left adjoint is given by the weighted colimit or coend formula

F^(X)=X SF= s:SX(s)F(s)\hat{F}(X) = X \otimes_S F = \int^{s: S} X(s) \cdot F(s)

where SdS \cdot d is notation for copowering (or tensoring) an object dd of DD by a set SS (in this case, a coproduct of an SS-indexed set of copies of DD). This formula recurs frequently throughout this wiki; see also nerve, Day convolution.

This “free cocompletion” property generalizes to enriched category theory. If VV is complete, cocomplete, symmetric monoidal closed, and SS is a small VV-enriched category, then the enriched presheaf category V S opV^{S^{op}} is a free VV-cocompletion of SS. The explicit meaning is analogous to the case where V=SetV = Set, where all ordinary category concepts are replaced by their VV-enriched analogues; in particular, the notion of “VV-cocontinuous functor” referes to preservation of enriched weighted colimits (not just ordinary conical colimits).

If CC is not small, then its free cocompletion still exists, but it is not the category of all presheaves on CC. Rather, it is the category of small presheaves on CC, i.e. presheaves that are small colimits of representables.

Gentle explanation

This section is a slightly new sort of experiment. Here John Baez would like to explain this remark to Mike Stay:

In the case where C=SetC = Set and SS is small, an important general principle is that the category of CC-valued presheaves on SS and natural transformations between them is the free cocompletion of SS.

The idea is that I’ll write some stuff, then Mike will write some questions, and so on. Other people are welcome to join, but only if they keep it simple. Please: no showing off! In particular, Mike does not yet understand coends or Kan extensions, so part of my job is to explain these, not just use them.

First, let me state the above result precisely.

Given a small category AA, let A^\hat{A} be our short name for Set A opSet^{A^{op}}, the category of presheaves on AA and natural transformations between them.

The Yoneda lemma gives an embedding Y:AA^Y : A \to \hat{A} – the Yoneda embedding.

The result says:

Theorem

Given any cocomplete category BB, and any functor F:ABF : A \to B, there is a cocontinuous functor F^:A^B\widehat{F} : \hat{A} \to B making this triangle commute up to natural isomorphism:

A F B Y F^ A^ \array{ A &\stackrel{F}{\to}& B \\ \downarrow^Y & \nearrow_{\widehat{F}} \\ \widehat{A} }

Moreover, F^\widehat{F} is unique up to natural isomorphism.

Our job is to understand how to construct this F^\widehat{F}.

But before we do that:

Why do we care?

There are many reasons why this theorem is important. Mike Stay needs it to convert between two equivalent descriptions of profunctors from a category AA to a category BB. On the one hand, we can think of them as functors

G:AB^ G : A \to \widehat{B}

On the other hand, we can think of them as cocontinuous functors

G^:A^B^ \widehat{G} : \widehat{A} \to \widehat{B}

Getting from GG to G^\widehat{G} here is a special case of the above Theorem. Getting from G^\widehat{G} to GG is vastly easier, so I’ll leave that as a little exercise:

Exercise. Given a cocontinuous functor A^B^\widehat{A} \to \widehat{B}, explain how to get a functor AB^A \to \widehat{B}.

Mike Stay: Precompose with YY.

John Baez: Right. So, going back — the hard part, which is what the Theorem lets us do — is a bit like trying to find an ‘inverse’ to precomposition with YY. And that’s exactly what Kan extensions are all about. So the theorem asserts that a certain Kan extension exists.

But don’t worry: I’m only mentioning this to intimidate you… err, I mean: to start getting you used to Kan extensions. They’re ‘best possible approximations to the perhaps impossible task of finding an inverse to precomposition with a functor’. But never mind!

Mike Stay: So the real content of the Theorem is saying that there’s always a “best” one; I can imagine that in other situations, you might have a bunch of inequivalent approximations, none of which is better than all the others, and would need to make an arbitrary choice.

John Baez: Yeah, for starters. However, I must admit: the Theorem actually says a lot more than the existence of a certain Kan extension. A Kan extension would merely ‘do its best’ to make a triangle commute up to natural isomorphism. In this particular case it actually succeeds! But never mind! I’m just trying to sneak certain ideas into your brain, so they’ll quietly take root: I don’t want to actually talk about them yet.

Now, try these exercises:

Exercise. Using the Theorem, show that going from a functor AB^A \to \widehat{B} to a cocontinuous functor A^B^\widehat{A} \to \widehat{B} and then precomposing with YY to get a functor AB^A \to \widehat{B} gets you back where you started—at least up to natural isomorphism.

Mike Stay: Well, given any functor F:AB^F:A \to \widehat{B}, you get from the Theorem a cocontinuous functor F^:A^B^\widehat{F}:\widehat{A} \to \widehat{B} such that F^Y\widehat{F} \circ Y is naturally isomorphic to FF.

John Baez: Right, so we’re back where we started, at least up to natural isomorphism.

Exercise. Also show that going from a cocontinuous functor A^B^\widehat{A} \to \widehat{B} to a functor AB^A \to \widehat{B} and then using the Theorem to turn that back into a cocontinuous functor A^B^\widehat{A} \to \widehat{B} gets you back where you started—at least up to natural isomorphism.

Mike Stay: Call our given functor F^:A^B^\widehat{F}: \widehat{A} \to \widehat{B}. Precompose with YY to get F^Y:AB^\widehat{F} \circ Y: A \to \widehat{B}. Then the theorem gives us a cocontinuous functor G:A^B^G: \widehat{A} \to \widehat{B} such that GYG \circ Y is the best approximation to F^Y\widehat{F} \circ Y. But this is F^\widehat{F} itself–at least up to natural isomorphism.

John Baez: I don’t think that’s a proof. First, I find the hand-waving about ‘best approximations’ a bit distracting—that’s the kind of talk we use in explaining stuff, not proving stuff. And it’s not good to call the functor we start with F^\widehat{F}, since it’s just any cocontinuous functor that someone handed us, not one we got from the Theorem. If we fix these problems, we get something like this:

Start with any cocontinuous functor G:A^B^G: \widehat{A} \to \widehat{B}. Precompose with YY to get GY:AB^G \circ Y: A \to \widehat{B}. Then go back using the Theorem, obtaining a cocontinuous functor G^:A^B^\widehat{G}: \widehat{A} \to \widehat{B} such that G^Y\widehat{G} \circ Y is naturally isomorphic to GYG \circ Y. We need to show that we got back where we started, up to natural isomorphism. So, we need to show that G^\widehat{G} is natural isomorphic to GG. What next?

(Hint: don’t be afraid to get stuck and realize that you could get out of being stuck if you knew a certain Lemma which might also be useful for other things we’re talking about below.)

Mike Stay: Well, we need to show that GYG^YGG^G \circ Y \cong \widehat{G} \circ Y \Rightarrow G \cong \widehat{G}; is YY an epimorphism?

John Baez: That would suffice, but it’s radically overoptimistic.

To see why, consider the second decategorified analogue below, where y:AA˜y: A \to \widetilde{A} is the inclusion of a set in the vector space having that set as a basis. Is this yy an epimorphism? In other words: is it onto? No! The vector space A˜\widetilde{A} is vastly larger than AA.

What does this mean? It means: it’s not true that given any vector space BB and function F:ABF : A \to B, there is a unique function F˜:A˜B\tilde{F} : \tilde{A} \to B making this triangle commute:

A F B y F˜ A˜ \array{ A &\stackrel{F}{\to}& B \\ \downarrow^y & \nearrow_{\tilde{F}} \\ \tilde{A} }

But this is okay: we don’t want a unique function F˜\tilde{F} making this diagram commute: we want a unique linear function making it commute. And that’s obviously true.

Having gained some intuition from the decategorified analogue, let’s go back to the situation we’re really interested in. If AA is the category with one object and one morphism, A^\widehat{A} is vastly larger than AA: it’s the category Set\Set. So, the Yoneda embedding Y:AA˜Y : A \to \widetilde{A} is far from being onto in any sense.

In particular, it’s not true that given any cocomplete BB and functor F:ABF : A \to B, there is an essentially unique functor F^:A^B\widehat{F} : \widehat{A} \to B making this triangle commute:

A F B Y F^ A^ \array{ A &\stackrel{F}{\to}& B \\ \downarrow^Y & \nearrow_{\widehat{F}} \\ \widehat{A} }

But this is okay: we don’t want a unique functor F^\widehat{F} making this diagram commute: we want a unique cocontinuous functor making it commute.

And this too should be obviously true, once we know what’s going on. What lemma would help?

Mike Stay: Oh! It would help to know this:

Lemma: Every object in A^\widehat{A} is a colimit of objects in the image of AA.

John Baez: Right. Given that, here’s how we tackle the Exercise:

Exercise. Show that going from a cocontinuous functor G:A^B^G : \widehat{A} \to \widehat{B} to a functor GY:AB^G \circ Y : A \to \widehat{B} and then using the Theorem to turn that back into a cocontinuous functor G^:A^B^\widehat{G}: \widehat{A} \to \widehat{B} gets you back where you started—at least up to natural isomorphism.

Proof - By the Theorem, G^\widehat{G} satisfies GYG^YG \circ Y \cong \widehat{G} \circ Y. We wish to show GG^G \cong \widehat{G}. We’re assuming GG preserves colimits, and the Theorem says that G^\widehat{G} does too. We know they agree on objects in the image of YY, and every object is a colimit of those, by the Lemma, so they agree.

Now for one more exercise:

Exercise. What is the hole in the above proof?

Mike Stay: I don’t know. Something about naturality?

How should we think about this, intuitively?

When we say A^\widehat{A} is the ‘free cocompletion’ of the category AA, it means we’re freely throwing in colimits (and thus wrecking the old colimits AA may have had). Since colimits are generalized ‘sums’, we can consider a decategorified analogue:

Decategorified Theorem. Given any set AA, let A˜\tilde{A} be the free commutative monoid on AA, and let y:AA˜y : A \to \tilde{A} be the obvious inclusion. If BB is a commutative monoid, given any function F:ABF : A \to B, there is a monoid homomorphism F˜:A˜B\tilde{F} : \tilde{A} \to B making this triangle commute:

A F B y F˜ A˜ \array{ A &\stackrel{F}{\to}& B \\ \downarrow^y & \nearrow_{\tilde{F}} \\ \tilde{A} }

Proof. The proof here is easy. Elements of A˜\tilde{A} are formal sums of elements of AA, like

x=a i x = \sum a_i

So, F˜\tilde{F} is determined by the fact that it preserves addition and acts like FF on guys in AA:

F˜(x)=F˜(a i)=F˜(a i)=F(a i)\tilde{F}(x) = \tilde{F} (\sum a_i) = \sum \tilde{F}(a_i) = \sum F(a_i)

Lo and behold — now we have a formula for F˜\tilde{F}. So, we just need to check some stuff. Check that F˜\tilde{F} is well-defined. Check that it’s a monoid homomorphism. Check that it makes the diagram commute. Check that it’s unique. All this is follow-your-nose stuff.

David Corfield: In the above Decategorified Theorem, shouldn’t you say commutative monoid AA, and then A˜\tilde{A} is the free commutative monoid on the underlying set of AA?

John Baez: No! We’re taking a set AA and freely throwing in sums to get the commutative monoid A˜\tilde{A}. This is like taking a category AA and freely throwing in colimits to get the cocomplete category A^\widehat{A}. See? There may be other fun things to do when our set was already a commutative monoid, but they’re not relevant to the analogy here.

David Corfield: Oh I see. Though I wonder if prettier category theory would have you talk about the underlying sets of A˜\tilde{A} and BB, and of commutative monoid morphism.

John Baez: You’re right: in some gold-plated treatment it would be good to carefully distinguish between commutative monoids and their underlying categories, or cocomplete categories and their underlying categories. That would be especially nice if we wanted to see ‘free commutative monoid’ or ‘free cocompletion’ as some sort of monad. But let’s prove the Theorem first and gold-plate it later, in the section below called Free cocompletion as a pseudomonad.

Proving the theorem

Okay, now let’s stop fiddling around and try to prove the bloody Theorem:

Theorem

Given any cocomplete category BB, and any functor F:ABF : A \to B, there is a cocontinuous functor F^:A^B\widehat{F} : \hat{A} \to B making this triangle commute up to natural isomorphism:

A F B Y F^ A^ \array{ A &\stackrel{F}{\to}& B \\ \downarrow^Y & \nearrow_{\widehat{F}} \\ \widehat{A} }

Moreover, F^\widehat{F} is unique up to natural isomorphism.

There are probably lots of ways to prove it, but let’s take a simple-minded approach that mimics the obvious proof of the Decategorified Theorem. We proved the Decategorified Theorem by finding a formula for the map we needed. So let’s try to write a formula for F^\widehat{F}, based on three ideas:

  1. Since the triangle commutes, we know what F^\widehat{F} should do to guys in the image of YY. Namely:
    F^(Y(x))=F(x)\widehat{F}(Y(x)) = F(x)

    (The triangle could just commute up to natural isomorphism, but let’s not worry about that yet — that’s just a nuance.)

  2. We know that F^\widehat{F} preserves colimits.
  3. We know that every object in A^\widehat{A} is a colimit of guys in the image of YY. (Such guys are called representable.)

Maybe you don’t actually know fact 3, but it’s true. If you don’t know why, don’t worry — you’ll soon find out!

These three facts are already enough to determine F^\widehat{F} on objects.

Exercise: Why?

So F^\widehat{F} is well on its way to being unique.

But why does F^\widehat{F} exist? For this it will really be good to have a formula expressing every object in A^\widehat{A} as a colimit of guys in the image of YY. As a side-effect this will prove fact 3. But even better: thanks to fact 2, this formula will yield a formula for F^\widehat{F}. And a formula is the best way to prove existence.

Mike Stay: Given categories A,BA, B and a functor F:AB^F: A \to \hat{B}, the fact that all objects in B^\hat{B} can be written as a sum over representables says that

F:A B^ a bBF(a)(b)×hom(,b)\array{F:A &\to& \hat{B}\\ a &\mapsto& \int_{b \in B} F(a)(b) \; \times \; hom(-, b)}

In a similar way, the Yoneda embedding says

Y:A A^ a aAY(a)(a)×hom(,a) = aAhom(a,a)×hom(,a) =hom(,a)\array{Y:A &\to& \hat{A}\\ a &\mapsto& \int_{a' \in A} Y(a)(a') \; \times \; hom(-, a')\\&&= \int_{a' \in A} hom(a', a) \; \times \; hom(-, a')\\&&= hom(-, a)}

That is, the set of morphisms from - to aa is the set of morphisms from - to an intermediate object aa' times the morphisms from aa' to aa, where aa' ranges over all possible objects in AA.

Doing the same for an arbitrary cocontinuous functor G:A^B^G:\hat{A} \to \hat{B} says

c= aAc(a)×hom(,a)c = \int_{a \in A} c(a) \; \times \; hom(-, a)

maps to

G(c)= aA( bBG(a)(b)×hom(a,b))×c(a)×hom(,a)G(c) = \int_{a \in A} \left(\int_{b \in B} G(a)(b) \; \times \; hom(a, b) \right) \; \times \; c(a) \; \times \; hom(-, a)

which simplifies to

G(c)= bB aAG(a)(b)×c(a)×hom(,b)G(c) = \int_{b \in B} \int_{a \in A} G(a)(b) \; \times \; c(a) \; \times \; hom(-, b)

by taking aa as the midpoint between - and bb. So GG is completely determined (up to isomorphism) by its values on the embedding of AA.

John Baez: Very good! But let me ask a few questions, starting with this. You say

“Given categories A,BA, B and a functor F:AB^F: A \to \hat{B}, the fact that all objects in BB can be written as a sum over representables says that

F:A B^ a bBF(a)(b)×hom(,b)\array{F:A &\to& \hat{B}\\ a &\mapsto& \int_{b \in B} F(a)(b) \; \times \; hom(-, b)}

I feel funny about this, because you say “all objects of BB can be written as a sum over representables”, but this doesn’t really make sense. It’s true that “all objects of B^\widehat{B} can be written as a colimit of representables” — is that what you meant? But even if so, how does this fact “say that

F:A B^ a bBF(a)(b)×hom(,b)?\array{F:A &\to& \widehat{B}\\ a &\mapsto& \int_{b \in B} F(a)(b) \; \times \; hom(-, b)?}

And I’d like us to write up a proof of the Theorem, so try to fit what you’ve written into a proof.

Mike Stay. Yes, I was being sloppy when I said “sum”. As for how it’s a colimit, consider two functors F:C opSet,G:CSet.F:C^{op} \to Set, \; G:C \to Set. Then

cCF(c)×G(c)\int_{c \in C} F(c) \; \times \; G(c)

is a colimit: for each f:ccf:c \to c' in CC, we get a diagram

F(c)×G(c) F(f)×G(c) F(c)×G(c) F(c)×G(f) F(c)×G(c)\array{F(c) \;\times\; G(c) & \stackrel{F(f) \;\times\; G(c)}{\leftarrow} & F(c') \;\times\; G(c) & \stackrel{F(c') \;\times\; G(f)}{\to} & F(c') \;\times\; G(c')}

and the colimit of all these is the “integral” above.

If I do a “search and replace” on the decategorified proofs, I get this:

Proof. The proof here is easy. Objects of A^\widehat{A} are colimits of objects of Y(A)=hom(,A)Y(A) = hom(-, A), like

x= aAx(a)×hom(,a) x = \int_{a \in A} x(a) \;\times\; hom(-, a)

with some “coefficients” x(a).x(a). So, F^\widehat{F} is determined by the fact that it preserves colimits and acts like FF on guys in hom(,A)hom(-, A):

F^(x)=F^( aAx(a)×hom(,a))= aAx(a)×F^(hom(,a))= aAx(a)×F(hom(,a))\widehat{F}(x) = \widehat{F} (\int_{a \in A} x(a) \;\times\; hom(-, a)) = \int_{a \in A} x(a) \;\times\; \widehat{F}(hom(-, a)) = \int_{a \in A} x(a) \;\times\; F(hom(-, a))

Lo and behold — now we have a formula for F^\widehat{F}. So, we just need to check some stuff. Check that F^\widehat{F} is well-defined. Check that it preserves colimits. Check that it makes the diagram commute up to natural isomorphism. Check that it’s unique up to natural isomorphism. All this is follow-your-nose stuff.“

But I bet you want me to actually follow my nose this time.

Free cocompletion as a pseudomonad

David Corfield: So is this ‘free cocompletion’ part of an adjunction between the category of categories and the category of cocomplete categories (modulo size worries?). Or should we think of it as part of a pseudoadjunction between 2-categories? (I would start a page on that, but how are naming conventions going in this area?)

John Baez: Equations between functors tends to hold only up to natural isomorphism. So, your first guess should not be that there’s an adjunction between the categories CatCat and CocompleteCatCocompleteCat, but rather, a pseudoadjunction between the 2-categories CatCat and CocompleteCatCocompleteCat.

If this were true, what would it mean? It would mean that there’s a forgetful 2-functor:

U:CocompleteCatCat U: CocompleteCat \to Cat

together with a ‘free cocompletion’ 2-functor, which right now we’ve been calling ‘hat’:

F:CatCocompleteCat F: Cat \to CocompleteCat
F:CC^=Set C op F: C \mapsto \widehat{C} = Set^{C^{op}}

And, it would mean there’s an equivalence of categories

hom CocompleteCat(FC,D)hom Cat(C,UD) hom_{CocompleteCat} (F C, D) \simeq hom_{Cat} (C, U D)

for every CCatC \in Cat, DCocompleteCatD \in CocompleteCat. And fiinally, it would also be saying that this equivalence is pseudonatural as a function of CC and DD.

If we have a pseudonatural equivalence of categories

hom CocompleteCat(FC,D)hom Cat(C,UD) hom_{CocompleteCat} (F C, D) \simeq hom_{Cat} (C, U D)

instead of a natural isomorphism of sets, then we say we have a ‘pseudoadjunction’ instead of an adjunction. A pseudoadjunction is the right generalization of adjunction when we go to 2-categories; if we were feeling in a modern mood we might just say ‘adjunction’ and expect people to know we meant ‘pseudo’.

Naively, it seems we do have such a pseudoadjunction, at least modulo size issues—which unfortunately is sort of like saying “modulo truth”! The problem is that if Cat is the 2-category of small categories then to define the free cocompletion functor

F:CatCocompleteCat F : Cat \to CocompleteCat

we need CocompleteCatCocompleteCat to be the 2-category of large categories. But if CocompleteCatCocompleteCat is the 2-category of large categories then to define

U:CocompleteCatCat U: CocompleteCat \to Cat

we need CatCat to be the 2-category of large categories! So, instead of an honest pseudoadjunction that bounces us back and forth between two 2-categories, the size keeps ratcheting up each time we make a round trip!

In particular, if we try to define a pseudomonad

UF:CatCat U F : Cat \to Cat

we’re stuck: the ‘CatCat’ at right contains larger categories than the one at left.

In their work on species, Fiore, Gambino, Hyland and Winskel had to confront this issue. In one draft of this paper they had a very artful and sophisticated device for dealing with this size problem. In the latest draft they seem to have sidestepped it entirely: you’ll see they discuss the ‘free symmetric monoidal category on a category’ pseudomonad, but never the ‘free cocomplete category on a category’ pseudomonad, even though they do use the C^\widehat{C} construction all over the place. Somehow they’ve managed to avoid the need to consider this construction as a pseudomonad!

In higher category theory

One can ask for the notion of free cocompletion in the wider context of higher category theory.

References

This reference might also give helpful clues:

A pedagogical explanation of the universal property of the Yoneda embedding is given starting on page 7. On page 8 there’s an explanation with lots of pictures how a presheaf is an “instruction for how to build a colimit”. Then on p. 9 the universal morphism that we are looking for here is identified as the one that “takes the instructions for building a colimit and actually builds it”.

(This text, by the way, contains various other gems. A pity that it is left unfinished.)

Revised on October 15, 2012 13:56:09 by Urs Schreiber (82.113.99.246)