If an adjunction $G$ preserves exponents, a particular morphism is iso.

Question

Let $F: \mathcal{C} \to \mathcal{D}$ and $G: \mathcal{D} \to \mathcal{C}$ be adjoint functors between cartesian closed categories. Suppose $G$ preserves exponentials. Prove that for all $X \in \mathcal{C}, Y \in \mathcal{D}$, the morphism

$(F\pi_X, \epsilon_Y \circ F\pi_{GY}): F(X \times GY) \to FX \times Y$

is an isomorphism.

As there is an isomorphism between $G(Y^{FX})$ and $(GY)^{GFX}$, there is a natural isomorphism between $\hom(-, G(Y^{FX}))$ and $\hom(-, (GY)^{GFX})$ by the Yoneda lemma. By definitions of the exponential object and adjunction, there are natural isomorphisms

$\hom(-, G(Y^{FX})) \cong \hom(F(-), Y^{FX}) \cong \hom(F(-) \times FX, Y)$ and

$\hom(-, (GY)^{GFX}) \cong \hom(- \times GFX, GY) \cong \hom F(- \times GFX), Y) $

for all $X, Y$. I hope we can massage this into a form where there is a natural isomorphism $F(- \times GY) \implies F(-) \times Y$. I can't manage to do this, but I think it is true because that is how we can prove the reverse implication. Even then, I don't see how we get that this is the desired isomorphism at $X$, since we are given no explicit isomorphism $G(Y^{FX}) \to (GY)^{GFX}$. Can we make this approach work or is there a better way?

Answer 1

You're actually very close to a solution : all you have to do is replace $F(X)$ by $Y$ and $Y$ by $Z$, i.e. start from the isomorphism $G(Z^Y)\simeq G(Z)^{G(Y)}$, and your reasoning will give you the isomorphism you want.

In fact, this reasoning is a specific instance of two properties of adjunctions :

1. the composition of two right adjoints is right adjoint to the (reversed) composition of their left adjoint;
2. any two adjoints to a functor, or more generally adjoints to isomorphic functors, are isomorphic.

Indeed, the property that $G$ preserve exponentials means that we have a natural isomorphism $G(Z^Y)\simeq G(Z)^{G(Y)}$, and this amounts to saying that $G\circ (\_)^{Y}\simeq (\_)^{G(Y)}\circ G$. Now the first property I mentioned above tells you that $G\circ (\_)^{Y}$ is right adjoint to $((\_)\times Y)\circ F$ and $(\_)^{G(Y)}\circ G$ is right adjoint to $F\circ ((\_)\times G(Y))$, and then the second property tells you that these left adjoints must also be isomorphic, i.e. $F(X)\times Y\simeq F(X\times G(Y))$.

Now as you said, this argument gives one isomorphism, but it is not clear why the isomorphism must be $(F(\pi_X),\epsilon_Y\circ F(\pi_{G(Y)})$. I guess you would get that if you assume that the isomorphism $G(Z^Y)\to G(Z)^{G(Y)}$ correspond under the product/exponential adjunction to the composite $G(Z^Y)\times G(Y)\to G(Z^{Y}\times Y)\to G(Z)$.