| context | $F$ in ${\bf D}\longrightarrow{\bf C}$ |
| context | $G$ in ${\bf C}\longrightarrow{\bf D}$ |
| definiendum | $\langle\varepsilon,\eta\rangle$ in $F\dashv G$ |
| inclusion | $\varepsilon, \eta$ … my nice nats $\left(F,G\right)$ |
| for all | $X\in{\bf C}, Y\in{\bf D}$ |
| postulate | $\varepsilon_{FY}\circ F(\eta_Y)=1_{FY}$ |
| postulate | $G(\varepsilon_X)\circ \eta_{GX}=1_{GX}$ |
The pair $\langle\varepsilon,\eta\rangle$ being nice nats for $F$ and $G$ means
$\varepsilon:FG\xrightarrow{\bullet}1_{\bf C}$
$\eta:1_{\bf D}\xrightarrow{\bullet}GF$
Counit-unit adjunctions should be contrasted with my equivalence of categories, which is another special case of nice nats. In the case of equivalences, $\langle\varepsilon,\eta\rangle$ are isomorphisms
$\alpha$ in $FG\cong 1_{\bf C}$
$\beta$ in $1_{\bf D}\cong GF$
In the case of equivalence, we can go from a category ${\bf D}$ along $F$ (to the image of ${\bf D}$ in ${\bf C}$, call that “image 1”) and then back along $G$ (the image of “image 1” in ${\bf D}$, call it “image 2”) and find the same (${\bf D}$ and “image 2” are actually isomorphic). This possibility for invertibility means nothing was lost when passing from ${\bf D}$ to “image 1”.
In the case of an adjunction, not both nats are invertible. However, we need not go two times along a functor to invert! We already know about an left-invertibility relation of $\eta$ (either in the form $F(\eta_Y)$ or $\eta_{GX}$) once we go to the first image.
$\varepsilon_{FY}\circ F(\eta_Y)=1_{FY}$
$G(\varepsilon_X)\circ \eta_{GX}=1_{GX}$
There is also the combined case where you have an equivalence where the natural transformations are related in the sense of above - this is called an adjoint equivalence.
Say you're given an arrow $f$ from or to the images of one of the functors (in either ${\mathrm{Hom}}(FX,Y)$ or ${\mathrm{Hom}}(X,GY)$). We can now pre- or post-compose with arrows formed from $\eta$ and $\epsilon$, use the functors on arrows and thus algebraically find an image of $f$ in the other category.
Of course, each identity morphisms $1_{FX}:{\mathrm{Hom}}(FX,FX)$ in ${\bf C}$ corresponds to a component $\eta_X:{\mathrm{Hom}}(X,GFX)$ of $\eta:1_{\bf D}\xrightarrow{\bullet}GF$. And the claim here is that not only
$1_{FX}\leftrightarrow \eta_X$
or even
${\mathrm{Hom}}(FX,FX)\cong{\mathrm{Hom}}(X,GFX)$,
but in fact
| ${\mathrm{Hom}}(FX,Y)\cong{\mathrm{Hom}}(X,GY)$ |
|---|
It's not that hard do the construction in both directions, after you've written down the types of $\eta,\epsilon, F, G$ before you.
For another perspective relating to universal morphisms, see On universal morphisms (31.10.2014).
Having an adjoint functor pair really means you also got a nice pair of natural transofmrations (for which functors are only a conditions). Given any functor $G$ (w.l.o.g, say you're in ${\bf D}$ and the functor out of it is $G$), then if there is an $F$ so that $F\dashv G$, you got yourself a monad.
It's important to note that as soon as (the fmap of one of) the adjoint functors are full and faithful, the adjunction provides and equivalence of categories.
To remember the symbol of the counit and unit, maybe it helps to point out that $\varepsilon$ kinda looks like a $c$ and $\eta$ kinda looks like a turned around $u$.
The arrow $\eta:1_{\bf D}\xrightarrow{\bullet}GF$ called the “unit” (or “return”, in the programming world). Here a mnemonic I cam up with:
tfw oneitis returns, becomes your GF and wants the D
The functor $F$ in $F\dashv G$ is the left adjoint. Analogously, $G$ is the right adjoint functor.
power set/list monad, also list-monad ⇔ set to free monoid
Wikipedia: Adjoint functors (category theory)