===== Counit-unit adjunction =====
==== Collection ====
| @#55CCEE: context     | @#55CCEE: $F$ in ${\bf D}\longrightarrow{\bf C}$ |
| @#55CCEE: context     | @#55CCEE: $G$ in ${\bf C}\longrightarrow{\bf D}$ |
| @#FFBB00: definiendum | @#FFBB00: $\langle\varepsilon,\eta\rangle$ in $F\dashv G$ |
| @#AAFFAA: inclusion   | @#AAFFAA: $\varepsilon, \eta$ ... my nice nats $\left(F,G\right)$ |
| @#FFFDDD: for all     | @#FFFDDD: $X\in{\bf C}, Y\in{\bf D}$ |
| @#55EE55: postulate   | @#55EE55: $\varepsilon_{FY}\circ F(\eta_Y)=1_{FY}$  |
| @#55EE55: postulate   | @#55EE55: $G(\varepsilon_X)\circ \eta_{GX}=1_{GX}$  |

-----
=== Elaboration ===
The pair $\langle\varepsilon,\eta\rangle$ being [[my nice nats|nice nats]] for $F$ and $G$ means

$\varepsilon:FG\xrightarrow{\bullet}1_{\bf C}$

$\eta:1_{\bf D}\xrightarrow{\bullet}GF$

=== Idea ===
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.

== Inducing hom-set adjunctions ==
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.

== As universals ==

For another perspective relating to universal morphisms, see [[On universal morphisms]] (31.10.2014).

== To monads ==

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]].

=== Theorems ===
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.

=== Terminology/Notation ===
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.

=== Examples ===
>[[http://math.stackexchange.com/questions/927832/adjoint-functors-for-the-power-set-monad|power set/list monad]], also list-monad <=> set to free monoid

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Adjunction_%28category_theory%29|Adjoint functors (category theory)]]

-----
=== Context ===
[[Functor]]
=== Subset of ===
[[My nice nats]]
=== Related ===
[[My equivalence of categories]]