Construction of Kan Extensions
Here, we will introduce Kan extensions, and give an explicit construction thereof. The data we will work with consists of two small categories, and , along with an arbitrary category that has small colimits. We will fix a functor . Note first that we have a functor . This functor has a left adjoint, called the (left) Kan extension along , denoted . We will explicitly define and show that it has the desired property.
For that, we will need a few additional notations – for , let denote the comma category consisting of pairs and denote by the forgetful projection functor .
So, for a functor , define on objects as follows:
Theorem: This assignment rule on objects actually extends to a functor.
Proof: We need to give a a well-defined behavior on maps. For maps, take a map in . We need to assign a canonical map . Note that we have a limit cone that comes with a family of maps
for every . At the same time, we have a limit cone and family of maps
for every . But observe that, given an , we can produce . Then we can form the co-cone:
If this is an honest co-cone, then we are guaranteed a unique map , the desired value for . Let’s verify that the above is actually a co-cone. Take a map in , which is actually a map such that . Note that (similarly for ) and . So we just the following triangle to commute:
But notice that since , its also true that , thus is also permissible as a map in . Then applying the fact that (2) is a cone to this map produces exactly the commuting triangle (4). So, (3) really is a co-cone, which makes well-defined.
It’s fairly straightforward to see that is itself a functor . To see how it behaves on a map (natural transformation) , observe that for each , induces a natural transformation between diagrams . Such a natural transformation induces a map between the limits , so let have components .
Now, let’s show the functor is actually the left adjoint.
Theorem: is left-adjoint to .
Proof: We will show that is in natural bijection with . First, let’s define the bijection itself by defining two operations and that are mutually inverse.
Take a natural transformation . It comes with components . We wish to define with components . For each , consider . Also note that . Thus, since , we have a projection map . Then we can form . We let this be the map . To verify that it is natural, we need that this outer rectangle commutes for any .
The bottom square commutes since is natural. For the top square, notice that it can be split into two triangles by the map shown. The lower-left of these triangles is precisely an expression of the universal property of . For the upper right, note that is permissible as a map in . As such, the upper right triangle is simply an expression of the (co)cone condition with respect to this map.
Take a natural transformation , with components . We wish to define , with components . For some , we can form a co-cone with vertex as follows – for each :
let’s quickly verify that this is indeed a co-cone. Take a map in , which is really a map with . We need this outer pentagon to commute:
It does, because it can be split into a square and a triangle as shown. The left square is a naturality square of , while the right triangle is just applied to the commuting triangle , which satisfies. So finally, let be the guaranteed unique map resulting from this co-cone.
Let’s show that and are mutually inverse. Take . is the unique map induced by the following cone
Simply observe that the following diagram commutes:
The left triangle is again the universal property of . The right triangle is actually a naturality square of disguised as a triangle. So, since makes this diagram commute it must be the unique such map mentioned. So , and .
Consider . We have . is the unique map induced by the cone:
that is to say, the unique map making this commute:
for all . Then, in particular, for , the diagram becomes:
And since , we have , and finally .
The only thing left to show is that this bijection is natural! Fix a and let’s show naturality in . This amounts to showing that is naturally isomorphic to (here denotes the Yoneda embedding), i.e. that this commutes for any
(note the contravariance due to the Yoneda embedding). Evaluating at a single , we have:
Without further ado, we have:
Using the commuting square from the universal property of , we can rewrite , and we continue:
So and the diagram commutes.
Our final task is to show naturality in . Fix an . We must show is naturally isomorphic to , which is to say this commutes:
Evaluating at an , we have:
And we proceed: So and the diagram commutes.
So, is well-defined and left-adjoint to , making it the left Kan extension along .