Suppose that the category $\mathbf C$ is cartesian closed: I must prove that, chosen three objects $x$, $y$, and $z$, the object $(x\times y)^z$ is isomorphic to $x^z\times y^z$. My idea was to define a morphism $(x\times y)^z\to x^z\times y^z$, one in the inverse direction, and prove that the composites are the identities. (Notation: given a product $a\times b$ I will call $\pi_a$ and $\pi_b$ the projections, and given $h:c\to a$, $k:c\to b$, the morphism $\langle h,k \rangle :c\to a\times b$ is the one defined using the universal property of products).
Now, for $f:(x\times y)^z\to x^z\times y^z$ one can choose $\langle (\pi_x)^z, (\pi_y)^z \rangle$; for the other direction things are more difficult, basically because it seems that I should at least have a map from $x$ to $y$, and using the adjunction (with the Hom-set definition) doesn't look helpful in this context. Actually, I prefer not to see the solution yet, but only to know if this direction can be the right one, and I just need to work with the adjunction and the properties of products (and the terminal object eventually), or if this approach is inconclusive. Thanks in advance
Best Answer
The easiest proof is by using that right adjoints preserve limits. The exponent functor $(-)^z$ is right adjoint to the product functor $(-) \times z$, that is: $(-) \times z \dashv (-)^z$. So this is just a direct application of that fact.
The proof of the above fact is constructive. So if you want an explicit proof you can just follow any (reasonable) proof, but just with the arbitrary adjunction and limit substituted by the exponential adjunction and product respectively. In fact, if you would follow the proof in the above link, then you get the proof you came up with in your comment.