3
$\begingroup$

How can I go about proving that $B^{A \times A'} \cong (B^A)^{A'}$ where $A$, $B$ and $A'$ are objects in a closed cartesian category.

The problem is, I can't even find a morphism from $B^{A \times A'}$ to $(B^A)^{A'}$.

I've found an arrow that goes the otherway around, it is: $curry(ev \circ(ev \times Id_A))$, where $curry(g)$ is a curried version of $g$ (I've seen it also denoted as $\hat{g}$) and $ev$ is an eval arrow.

Thanks.

Disclamer: This is a question from a textbook/tutorial "Basic Category Theory for Computer Scientists" by B. Pierce. I am working through that book on my own, so this question is not a part of my homework

$\endgroup$
6
$\begingroup$

The universal property of exponentiation says that to give a morphism $X\times Y \to Z$ is equivalent to giving a morphism $X \to Z^Y$. We just use this in reverse twice, first to give a morphism

$B^{A \times A'} \to (B^A)^{A'}$

is equivalent to giving a morphism

$B^{A \times A'} \times A' \to B^A$

(use $X = B^{A \times A'}$, $Y = A'$, and $Z = B^A$). But giving that morphism is equivalent to giving a morphism

$B^{A \times A'} \times A' \times A \to B$

and this final morphism can be given using an eval.

$\endgroup$
  • $\begingroup$ Thanks! When I wrote everything down in a diagram it all made sense, the arrow is $curry(curry(ev))$. However, I still have a minor question: how would I go about proving that the composition of those arrows is an identity arrow? Previously, I was able to present such proofs using commutative diagrams, but in this case I only have diagrams with $(B^A)^{A'} \times A \times A'$ and not $(B^A)^{A'}$ $\endgroup$ – Daniil Jan 29 '13 at 20:13
  • 2
    $\begingroup$ The universal property says that arrows $X \times Y \to Z$ are uniquely associated to arrows $X \to Z^Y$. The identity map $B^{A \times A'} \to B^{A \times A'}$ gets associated to the eval map $B^{A \times A'} \times A \times A' \to B$ so show that the composition $B^{A \times A'} \to (B^A)^{A'} \to B^{A \times A'}$ of your two arrows is also associated to this eval map. $\endgroup$ – Jim Jan 29 '13 at 20:59
5
$\begingroup$

This is going to add nothing to Jim's answer, but the adjoint-nonsense is much more evident:

$$ \begin{align} \hom(X,B^{A\times C}) & \cong \hom(X\times A\times C,B) \\ & \cong \hom(X\times A,B^C) \\ & \cong \hom(X,(B^C)^A) \end{align} $$ Now (with a smart application of Yoneda Lemma: see below Zhen Lin's comment) $B^{A\times C}\cong (B^C)^A$. []

Additional exercise: Notice that this is nothing more than the second of these properties. :)

$\endgroup$
  • 2
    $\begingroup$ $\textrm{Hom}(X, -)$ doesn't reflect isomorphisms in general, but the collection of all $\textrm{Hom}(X, -)$ jointly reflect isomorphisms. $\endgroup$ – Zhen Lin Jan 30 '13 at 9:36
  • $\begingroup$ Thanks for the correction! $\endgroup$ – Fosco Jan 30 '13 at 20:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.