**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 .