Describing the universal property of the evaluation map

417 Views Asked by At

Emily Riehl's "Category Theory in Context", ${\rm Exercise}~2.3.{\rm iii}.$

The set $B^A$ of functions from a set $A$ to a set $B$ represents the contravariant functor ${\rm Set}(-\times A,B):{\rm Set}^{\rm op}\to{\rm Set}$. The universal element for this representation is a function $${\rm ev}:B^A\times A\to B$$ called the evaluation map. Define the evaluation map and descripe its universal property, in analogy with the universal bilinear map $\otimes$ of Example $2.3.7$ (the tensor product).

I will start by descrping the universal property. For a representable functor, a universal element $x\in Fc$ defines a natural isomorphism $\mathcal C(-,c)\cong F$ (in the contravariant case, as given). Given ${\rm ev}\in{\rm Set}(B^A\times A,B)$ is a universal element, the induced natural isomorphism arises as $${\rm Set}(X,B^A)\cong{\rm Set}(X\times A,B)$$ In particular, for every map $\bar f:B^A\to X$ there bijectively corresponds a map $f:X\times A\to B$ identified with each other via the natural isomorphism. Consider the following commutative square induced by $\bar f:B^A\to X$ $$\tag D\require{AMScd}\begin{CD} {\rm Set}(B^A,B^A) @>{\cong}>>{\rm Set}(B^A\times A,B)\\ @V{\bar f^*}VV @VV{\bar f^*\times{\rm id}_A}V\\ {\rm Set}(X,B^A) @>{\cong}>>{\rm Set}(X\times A,B) \end{CD}$$ Tracing $1_{B^A}$ around reveals $f={\rm ev}\circ(\bar f\times{\rm id}_A)$ which is in fact the universal property of the evaluation map. The map itself can be defined as $${\rm ev}:B^A\times A\to B,~(g,a)\mapsto g(a)$$

Is this account sufficient or have I left out something crucial? Following up, is the diagram $($D$)$ correct as it stands, i.e. are all arrows pointing in the correct direction (which boils down to: are $f$ and $\bar f$ correctly defined)?

Thanks in advance!


Remark: the notation $f^*$ refers to pre-composition with $f$.