Quirkiness with Kan Extensions

Quirkiness with Kan Extensions

Given two functors F :  C  \to D and K : C \to Dleft kan extension of F along K is a functor Lan_kF : D \to E along with a natural transformation \eta : F \to \text{Lan}_KF K universal in that for any pair (G:  D \to E, \gamma: F \to GK) there is a unique natural transformation \alpha : \text{Lan}_KF \to G such that  \gamma = \alpha_K \eta as in the diagram


Our counterexample is meant to define intuition about this commutativity “up to universal natural transformation.” A properly commutating diagram may not actually be the Kan extension.  In other words, if F factors through K by some H then (H,1_H) is not necessarily the same as (\text{Lan}_KF, \eta).

Spoiler Alert: This is exercise 1.1.3. in [1]. If you want to find out for yourself, stop reading.

Take 1 = C, E=Set and D arbitrary. Let d \in D be an arbitrary object and let d : 1 \to D denote the functor constant at d. We take F = \ast e.g. F is the functor constant at some singleton set \ast. Then, we can (by abuse of notation) write \ast : D \to Set again for the functor constant at \ast. Indeed we have \ast = \ast \circ d. But, \ast : D \to Set is not the (left) Kan extension of \ast along d.

Claim: (\text{Lan}_d\ast,\eta)=(\text{Hom}_D(d,-),1_D)

Why is this true?  Because elements x \in Fd are in bijection with natural transformations x : \ast \to F.d By Yoneda’s lemma, these elements are in natural bijection with natural transformations \text{Hom}_D(d,-) \to F. This is exactly the universal property of left Kan extensions.


[1] Riehl, E. Categorical Homotopy Theory. Cambridge University Press, 2014.


Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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