Pointwise Kan extension formula

Remarks

The comma category $(K \downarrow b)$ is small because $\mathcal{A}$ is small and $\mathcal{B}$ is locally small, so the colimit exists. A morphism $g \colon b \to b'$ induces a functor $(K \downarrow b) \to (K \downarrow b')$ by composing with $g$, and hence a map between the colimits; this makes $b \mapsto (\mathrm{Lan}_K F)(b)$ a functor. The component $\eta_a$ is the colimit injection at the object $(a, \id_{K(a)})$. The universal property is checked by turning a natural transformation $F \Rightarrow G \circ K$ into a compatible family of cocones, one for each $b$.

Dually, suppose that $\mathcal{C}$ has all small limits. Then $(\mathrm{Ran}_K F)(b)$ is the limit of $F$ over the comma category $(b \downarrow K)$ of pairs $(a, f \colon b \to K(a))$. When $K$ is fully faithful, the unit $\eta \colon F \Rightarrow (\mathrm{Lan}_K F) \circ K$ is an isomorphism. The reason is that $(a, \id_{K(a)})$ is then a terminal object of $(K \downarrow K(a))$.

Example: view a group $G$ and a subgroup $H$ as one-object categories, and let $K$ be the inclusion. Let $F$ be a representation of $H$ on a vector space $V$ over a field $k$. Then the formula gives the induced representation $k[G] \otimes_{k[H]} V$ of $G$.

Going deeper

For a student

This is the standard way to show that Kan extensions exist, and it is the version used in most applications. Taking $\mathcal{B} = \mathbf{1}$ recovers the colimit of $F$. Taking $K$ to be the Yoneda embedding of $\mathcal{A}$ extends $F$ to a colimit-preserving functor on presheaves. This is the basis of the nerve and realization adjunctions. A Kan extension computed by this formula is called pointwise. In the language of coends the formula reads $(\mathrm{Lan}_K F)(b) = \int^{a} \mathcal{B}(K(a), b) \cdot F(a)$. Here $S \cdot c$ is the coproduct of copies of $c$ indexed by the set $S$.