Unit and Counit of an Adjunction

definition theorem proof example

Given an Adjunction $L⊣R$ with hom-set isomorphism ${\varphi }_{x,y}:\mathcal{D}(Lx,y)\cong \mathcal{C}(x,Ry)$:

• setting $y:=Lx$ and applying $\varphi$ to ${\mathrm{id}}_{Lx}$ (the Yoneda trick) gives the unit ${\eta }_x:x\to R(Lx)$, a Natural Transformation $\eta :\mathrm{Id}\Rightarrow R\circ L$;
• setting $x:=Ry$ and applying ${\varphi }^{-1}$ to ${\mathrm{id}}_{Ry}$ gives the counit ${\epsilon }_y:L(Ry)\to y$, a natural transformation $\epsilon :L\circ R\Rightarrow \mathrm{Id}$.

They satisfy the triangle identities (zig-zag identities), using horizontal composition/whiskering:

$$(\epsilon \circ L)\cdot (L\circ \eta )={\mathrm{id}}_L,(R\circ \epsilon )\cdot (\eta \circ R)={\mathrm{id}}_R,$$

i.e. $L\stackrel{L\eta }{\to }LRL\stackrel{\epsilon L}{\to }L$ and $R\stackrel{\eta R}{\to }RLR\stackrel{R\epsilon }{\to }R$ are identities. Conversely, natural transformations $\eta ,\epsilon$ satisfying the triangle identities determine the adjunction: $f:x\to Ry$ has mate ${\epsilon }_y\circ Lf$, and $g:Lx\to y$ has mate $Rg\circ {\eta }_x$ (DaoFP Exercise 10.5.2). ”$\eta$ can be used to insert $RL$ anywhere an identity would work; $\epsilon$ to eliminate $LR$.”

Sources: DaoFP §10.5 (“Unit and Counit of an Adjunction”, “Triangle identities”, “The unit and counit of the currying adjunction”), Exercises 10.5.1–10.5.4; 7 Sketches Proposition 1.107 (preorder version: $p\le g(f(p))$ and $f(g(q))\le q$), Exercise 1.119; Kittenlab Lecture 7 (${\eta }_X:X\to UFX$, $x\mapsto [x]$).

Examples

adjunction	unit	counit
$(+)⊣\Delta$	the pair of injections $⟨\mathsf{Left},\mathsf{Right}⟩:(a,b)\to \Delta (a+b)$	$[\mathrm{id},\mathrm{id}]:x+x\to x$ (DaoFP Exercise 10.5.1)
$\Delta ⊣(\times )$	$⟨\mathrm{id},\mathrm{id}⟩:x\to x\times x$	the pair of projections $⟨\mathsf{fst},\mathsf{snd}⟩$
$(-\times a)⊣(-{)}^a$	$\eta :e\to (e\times a{)}^a$, unit = curry id (the curried pair constructor)	$\epsilon :b^a\times a\to b$, counit = uncurry id — function application
free $⊣$ forgetful monoid	$x\mapsto [x]$, singleton list	$\mathrm{fold}$: evaluate a list of monoid elements (DaoFP Exercise 10.9.1)
Galois Connection $f⊣g$	$p\le g(f(p))$	$f(g(q))\le q$
$\mathrm{Colim}⊣\Delta ⊣\mathrm{Lim}$	the colimit cocone / the map into the limit of a constant diagram	the universal cocone map / the limit cone

In string diagrams (DaoFP §15.1) the unit is a cup and the counit a cap, and the triangle identities say a zig-zag string straightens out. The unit and counit are the universal arrows of the adjunction (DaoFP §10.6). The composite $RL$ with $\eta$ and $R\epsilon L$ is a Monad; $LR$ with $\epsilon$ and $L\eta R$ a Comonad. In a preorder, $g\circ f$ is a Closure Operator.

LeanHaskell

#check CategoryTheory.Adjunction.unit          -- 𝟭 C ⟶ F ⋙ G
#check CategoryTheory.Adjunction.counit        -- G ⋙ F ⟶ 𝟭 D
#check CategoryTheory.Adjunction.left_triangle_components
#check CategoryTheory.Adjunction.right_triangle_components
#check CategoryTheory.Adjunction.mkOfUnitCounit

-- DaoFP §10.5: unit and counit of currying
unit :: e -> (a -> (e, a))
unit = curry id
 
counit :: (a -> b, a) -> b
counit = uncurry id          -- function application
 
-- triangle identity tests (DaoFP Exercise 10.5.3/10.5.4)
-- triangle (L (2, 'a')) == L (2, 'a');   let R f = triangle' (R (+1)) in f 3 == 4