Derive adjoint unit from counit

Question

As an exercise (2.4.12#5) in Pierce's Basic Category Theory for Computer Scientists, I'm trying to derive the unit natural transformation $\eta : I_{\textbf{C}} \xrightarrow{\cdot} G \circ F$ given the counit transformation $\epsilon : F \circ G \xrightarrow{\cdot} I_{\textbf{D}}$ and two adjoint functors $F : \textbf{C} \rightarrow \textbf{D} \dashv G : \textbf{D} \rightarrow \textbf{C}$

I figure I need something that takes $X \rightarrow G(F(X))$ for any X.

For any Y, if I provide an arrow $g : F(X) \rightarrow Y$, $\epsilon$ guarantees the existence of a unique arrow $g^* : X \rightarrow G(Y)$ satisfying $\epsilon_Y \circ F(g^*) = g$

So I consider $Y = F(X)$ and select the arrow $id_{F(X)}$, this guarantees a unique $id_{F(X)}^* : X \rightarrow G(F(X))$ such that $\epsilon_{F(X)} \circ F(id_{F(X)}^*) = id_{F(X)}$.

This $id_{F(X)}^*$ has the right type to be $\eta_X$, and intuitively $id_{F(X)}^*$ is a suspiciously good candidate. Unfortunately, I haven't had luck converting that intuition into a proof.

In order to show that $id_{F(X)}^*$ works as $\eta_X$ I need to show that for any $f : X \rightarrow G(Y)$ there's a unique $f^\# : F(X) \rightarrow Y$ satisfying $G(f^\#) \circ id_{F(X)}^* = f$.

This is where I'm stuck: I've gone down a number of paths here, and I always end up with deep functor stacks like $G(F(G(F(X))))$ that I have trouble reducing without loss of generality. I'm having trouble finding a way to generate an arrow $F(X) \rightarrow Y$ from an arrow $X \rightarrow G(Y)$ without invoking the $\eta$ transformation (which is what I'm trying to derive).

I'm sure I'm neglecting a crucial adjoint law that makes this easy. Can you point me in the right direction?

Answer 1

You were just there!

The mapping you need maps a morphisms $f:X\to GY$ to $$f^\# := \varepsilon_Y\circ Ff\,. $$ Show that this is inverse to $g\mapsto g^*$ and that these build a natural isomorphism $\hom(X,GY)\to\hom(FX,Y)$, so already create an adjunction. Show that its counit is indeed $\varepsilon$.

---

To prove the required property explicitly, it seems that you may work more:

• Prove that $\eta:=X\mapsto 1_{FX}^*$ is a natural transformation.

Then, by naturality, we have $\ G(f^\#)\circ\eta_X=G\varepsilon_Y\circ GFf\circ\eta_X= G\varepsilon_Y\circ \eta_{GY}\circ f$.

• Prove the familiar identity $G\varepsilon_Y\circ \eta_{GY} = 1_{GY}$.
• And still, uniqueness for that property would need a prove..