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\mathrm{:}A\mathrm{\to }B$ is a left adjointif there exists

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

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

• A natural transformation $ϵ:FG\to 1_B$ (the counit).

• $(ϵF)(F\eta )=1_F$.

• $(Gϵ)(\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 ,ϵ)$ with the triangle identities and also $(G^{\prime },{\eta }^{\prime },{ϵ}^{\prime })$.Define $\gamma :G\to G^{\prime }$ to be $(G^{\prime }ϵ)({\eta }^{\prime }G)$, and $\delta :G^{\prime }\to G$ to be $(G{ϵ}^{\prime })(\eta G^{\prime })$.Then

$\delta \gamma$$=(G{ϵ}^{\prime })(\eta G^{\prime })(G^{\prime }ϵ)({\eta }^{\prime }G)$

$=(G{ϵ}^{\prime })(GF{G}^{\prime }ϵ)(\eta G^{\prime }FG)({\eta }^{\prime }G)$

$=(Gϵ)(G{ϵ}^{\prime }FG)(GF{\eta }^{\prime }G)(\eta G)$

$=(Gϵ)(\eta G)$

$=1_G$

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

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

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

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

In sec:yoneda we will give another proof of ct:adjprop.