Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Consider the evident isomorphism between $(A^B)^C$ and $A^{B\times C}$. Awodey gives this to be given by $g=\lambda(\epsilon\circ (\epsilon\times 1)\circ \alpha_{(A^B)^C})$ and $g^{-1}=\lambda\lambda (\epsilon\circ \alpha^{-1}_{A^{B\times C}})$, where $\alpha_Z : (Z\times B) \times C \rightarrow Z\times (C\times B)$ is the evident isomorphism from commutativity and associativity.

However, I have been unable to verify that $g\circ g^{-1}=1$ or $g^{-1}\circ g=1$. I do not see any way to apply the equations of the exponential to either expression. How can I reduce these expressions to obtain the desired identity? Or does verifying the isomorphism require some other mechanism?

share|cite|improve this question
I do not think it is productive to try to write out this isomorphism using one-dimensional notation. There may be a better two-dimensional notation. – Qiaochu Yuan Dec 22 '12 at 8:25
I'm not sure I agree. Two-dimensional notion tends to sweep coherence isomorphisms such as this one under the rug. – Zhen Lin Dec 22 '12 at 9:14
@Zhen: then perhaps there is a three-dimensional notation which describes those coherence isomorphisms...? – Qiaochu Yuan Dec 22 '12 at 9:44
up vote 3 down vote accepted

Schematically, the isomorphism arises by applying the Yoneda lemma to the following chain of natural bijections: \begin{align} \textrm{Hom}(D, (A^B)^C) & \cong \textrm{Hom}(D \times C, A^B) \\ & \cong \textrm{Hom}((D \times C) \times B, A) \\ & \cong \textrm{Hom}(D \times (C \times B), A) \\ & \cong \textrm{Hom}(D \times (B \times C), A) \\ & \cong \textrm{Hom}(D, A^{B \times C}) \end{align} Substituting $D = (A^B)^C$ and $D = A^{B \times C}$ and chasing the bijections will give the required equations. If you are unfamiliar with this technique, here is one calculation. Let $D = A^{B \times C}$. The isomorphism $A^{B \times C} \to (A^B)^C$ is given by the formula $$c = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B})^B \circ \lambda_{D \times C, B})^C \circ \lambda_{D, C}$$ where $\epsilon_{B \times C, A} : A^{B \times C} \times (B \times C) \to A$ is evaluation, $\gamma_{C, B} : C \times B \to B \times C$ is the symmetry isomorphism, $\alpha_{D,C,B} : (D \times C) \times B \to D \times (C \times B)$ is the associativity isomorphism, and $\lambda_{D \times C, B} : D \times C \to ((D \times C) \times B)^B$ and $\lambda_{D, C} : D \to (D \times C)^C$ are the components of the units of the respective adjunctions. With similar notation, writing $E = (A^B)^C$, the isomorphism $(A^B)^C \to A^{B \times C}$ is: $$u = (\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}))^{B \times C} \circ \lambda_{E, B \times C}$$ Now, $\lambda_{D, C}$ is natural in $D$, so $$\lambda_{D, C} \circ u = (u \times \textrm{id}_C)^C \circ \lambda_{E, C}$$ and therefore $$c \circ u = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B})^B \circ \lambda_{D \times C, B} \circ (u \times \textrm{id}_C))^C \circ \lambda_{E, C}$$ and similarly, $\lambda_{D \times C, B}$ is natural in $D \times C$, so $$\lambda_{D \times C, B} \circ (u \times \textrm{id}_C) = ((u \times \textrm{id}_C) \times \textrm{id}_B)^B \circ \lambda_{E \times C, B}$$ hence: \begin{align} c \circ u & = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ \alpha_{D, C, B} \circ ((u \times \textrm{id}_C) \times \textrm{id}_B))^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B \times C, A} \circ (\textrm{id}_D \times \gamma_{C, B}) \circ (u \times \textrm{id}_{C \times B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) \circ (\textrm{id}_E \times \gamma_{C, B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \end{align} Now, $\epsilon_{B \times C, A}$ is natural in $A$, so expanding even more: \begin{align} \epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) & = \epsilon_{B \times C, A} \circ (((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}))^{B \times C} \circ \lambda_{E, B \times C}) \times \textrm{id}_{B \times C}) \\ & = \epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}) \circ \epsilon_{B \times C, E \times (B \times C)} \circ (\lambda_{E, B \times C} \times \textrm{id}_{B \times C}) \end{align} and fortunately for us, $\epsilon_{B \times C, E \times (B \times C)} \circ (\lambda_{E, B \times C} \times \textrm{id}_{B \times C}) = \textrm{id}_{E \times (B \times C)}$ by the triangle identity, so $$\epsilon_{B \times C, A} \circ (u \times \textrm{id}_{B \times C}) = \epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B})$$ and putting this back in yields: \begin{align} c \circ u & = ((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B) \circ \alpha^{-1}_{E,B,C} \circ (\textrm{id}_E \times \gamma^{-1}_{C, B}) \circ (\textrm{id}_E \times \gamma_{C, B}) \circ \alpha_{E, C, B})^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B, A} \circ (\epsilon_{C, A^B} \times \textrm{id}_B))^B \circ \lambda_{E \times C, B})^C \circ \lambda_{E, C} \\ & = ((\epsilon_{B, A})^B \circ \lambda_{A^B, B} \circ \epsilon_{C, A^B})^C \circ \lambda_{E, C} \\ & = (\epsilon_{C, A^B})^C \circ \lambda_{E, C} \\ & = \textrm{id}_E \end{align} by the triangle identities and the naturality of $\lambda_{E \times C, B}$ in $E \times C$.

Now aren't you glad equations aren't the only way of proving the isomorphism?

share|cite|improve this answer
I am aware that the Yoneda lemma provides a much easier proof. I am specifically trying to do this directly. – James Koppel Dec 22 '12 at 8:33
As I said, you can get the equations by chasing these bijections. This is a standard way of converting Yoneda-style proofs into direct proofs. – Zhen Lin Dec 22 '12 at 8:52

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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