9.3 Adjunctions

The definition of adjoint functors is straightforward; the main interesting aspect arises from proof-relevance.

Definition 9.3.1.

A functor $F:A\to B$ is a left adjoint if there exists

•

A functor $G:B\to A$ .
•

A natural transformation $\eta:1_{A}\to GF$ (the unit).
•

A natural transformation $\epsilon:FG\to 1_{B}$ (the counit).
•

$(\epsilon F)(F\eta)=1_{F}$ .
•

$(G\epsilon)(\eta G)=1_{G}$ .

The last two equations are called the triangle identities or zigzag identities. We leave it to the reader to define right adjoints analogously.

Lemma 9.3.2.

If $A$ is a category (but $B$ may be only a precategory), then the type “ $F$ is a left adjoint” is a mere proposition.

Proof.

Suppose we are given $(G,\eta,\epsilon)$ with the triangle identities and also $(G^{\prime},\eta^{\prime},\epsilon^{\prime})$ . Define $\gamma:G\to G^{\prime}$ to be $(G^{\prime}\epsilon)(\eta^{\prime}G)$ , and $\delta:G^{\prime}\to G$ to be $(G\epsilon^{\prime})(\eta G^{\prime})$ . Then

	$\displaystyle\delta\gamma$	$\displaystyle=(G\epsilon^{\prime})(\eta G^{\prime})(G^{\prime}\epsilon)(\eta^{% \prime}G)$
		$\displaystyle=(G\epsilon^{\prime})(GFG^{\prime}\epsilon)(\eta G^{\prime}FG)(% \eta^{\prime}G)$
		$\displaystyle=(G\epsilon)(G\epsilon^{\prime}FG)(GF\eta^{\prime}G)(\eta G)$
		$\displaystyle=(G\epsilon)(\eta G)$
		$\displaystyle=1_{G}$

using \autorefct:interchange and the triangle identities. Similarly, we show $\gamma\delta=1_{G^{\prime}}$ , so $\gamma$ is a natural isomorphism $G\cong G^{\prime}$ . By \autorefct:functor-cat, we have an identity $G=G^{\prime}$ .

Now we need to know that when $\eta$ and $\epsilon$ are transported along this identity, they become equal to $\eta^{\prime}$ and $\epsilon^{\prime}$ . By \autorefct:idtoiso-trans, this transport is given by composing with $\gamma$ or $\delta$ as appropriate. For $\eta$ , this yields

$(G^{\prime}\epsilon F)(\eta^{\prime}GF)\eta=(G^{\prime}\epsilon F)(G^{\prime}F% \eta)\eta^{\prime}=\eta^{\prime}$

using \autorefct:interchange and the triangle identity. The case of $\epsilon$ is similar. Finally, the triangle identities transport correctly automatically, since hom-sets are sets. ∎

In \autorefsec:yoneda we will give another proof of \autorefct:adjprop.

Title	9.3 Adjunctions
\metatable