Reviewing Mac Lane: Kans and Ends II

The other topic I wanted to cover in this post is Kan extensions, another concept I’ve seen repeatedly yet not really understood. So there’s the Haskell-as-semi-formal-notation approach in Kmett’s posts (starting here) that give lots of examples, but for me to understand something I really need to see it in more traditional mathematical form. Going back to Mac Lane, we see that there are both left and right Kan extensions. We’ll start by describing the right kind.

A right Kan extension for a pair of functors K : M \to C and T: M \to A is a functor R : C \to A and a natural transformation \epsilon : R \circ K \to T such that \epsilon is a universal arrow to T in the appropriate functor category. What does this actually mean, though? Well, my guess is that this right Kan extension generalizes the concept of extending the map T: M \to A to a map R : C \to A. The interesting thing, to me, is that we’re not requiring that the composition of R \circ K is T just that there’s a consistent way to transform back to T. If we squint for a moment and consider sets as categories with only trivial arrows, then it seems like for an arbitrary T and any 1-1 function K then we’ll have a right Kan extension for it, which will be the function R that sends the image of K to the image of T and maps everything not in the image of K to a single point.

There’s also the left Kan extension, which is just the same as the right Kan extension but with the direction of \epsilon swapped and the universality swapped as well. If the right Kan extension generalizes extending a function to a larger domain through an embedding, then I would guess that the left Kan extension generalizes restriction through an onto function. In this case, the natural transformation \epsilon would be a “contraction” of sorts that takes the image of T and shrinks it to the image of the restriction.

So that’s neat, but what’s the point of Kan extensions in general? Well, I’d always heard the line from Mac Lane “all concepts are Kan extensions” but what exactly does that mean? In section 7 of “Categories…”, he gives a number of examples how other constructions can be described as Kan extensions. For example, a functor T : M \to A has a colimit exactly when there is a left Kan extension for T : M \to A and 1 : M \to 1, here we’re considering T as the T above and 1 as our K. Why does this exactly work? Well, if you consider that a left Kan extension for these functors means that we have a functor a : 1 \to A which just selects out the object a from A and a natural transformation \epsilon from T to the functor a \circ 1 : M \to A then we’ve just described the universal cone for T which is precisely how we defined the colimit. Similarly, right Kan extensions correspond to limits. We can also use Kan extensions to describe adjoints.

Of course, the problem I have in a sense is what else do you actually use Kan extensions for other than unifying other existing constructions? Now, generalizing is always nice but usually generalizations also expand what you can describe. Here I’m still at a loss for good examples.

I feel slightly guilty that the last two posts I don’t think will have much value for the reader, but they’re at least my attempt to review topics that didn’t sink in on first reading.

Next time I think we’ll finish the simplicial sets paper we’ve been going through and then move onto other things more directly about type theory.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s