Lagmental Vicfred

Unit and Counit Encode the Triangle Identities by Vicfred

An adjunction can be recovered from its unit and counit once two triangular composites are identities. The example is deliberately concrete; it is a test of the statement, not a substitute for it.

Start locally

Category theory records objects through their morphisms. A functor \(F:\mathcal C\to\mathcal D\) preserves identities and composition, while a natural transformation \(\eta:F\Rightarrow G\) compares functors uniformly.

$$ \eta:1_{\mathcal C}\Rightarrow GF,\qquad\varepsilon:FG\Rightarrow1_{\mathcal D} $$

The typography mirrors the proof: first declare \(\mathsf D\), then state \(\mathsf C\). The symbol \(\Longrightarrow\) below is a logical dependency, not extra mathematical structure.

$$ \varepsilon_{FX}\circ F(\eta_X)=1_{FX},\qquad G(\varepsilon_Y)\circ\eta_{GY}=1_{GY} $$

Compute before generalising

The following line is the smallest calculation that still exercises the mechanism. It keeps nested delimiters and the order of operations explicit.

$$ \begin{gathered}FX\xrightarrow{F\eta_X}FGFX\xrightarrow{\varepsilon_{FX}}FX,\\GY\xrightarrow{\eta_{GY}}GFGY\xrightarrow{G\varepsilon_Y}GY.\end{gathered} $$

The global view

What survives the example is not its particular numbers but the relation encoded by the two rows below. That relation is the part worth transporting to a new setting.

$$ \begin{aligned} \mathsf{D}\;&:\quad \eta:1_{\mathcal C}\Rightarrow GF,\qquad\varepsilon:FG\Rightarrow1_{\mathcal D},\\[5pt] \mathsf{C}\;&:\quad \varepsilon_{FX}\circ F(\eta_X)=1_{FX},\qquad G(\varepsilon_Y)\circ\eta_{GY}=1_{GY}. \end{aligned} $$

Edge conditions

An isomorphism of objects is stronger than a natural bijection of underlying sets unless that bijection respects all morphisms in the relevant category.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] \varepsilon_{FX}\circ F(\eta_X)=1_{FX},\qquad G(\varepsilon_Y)\circ\eta_{GY}=1_{GY} \end{gathered}} $$

The final box is a summary, not a new assumption; the proof still lives in the definitions and the intervening calculation. The source keeps each scope delimiter visible for later inspection.

This article was posted on Sun 30 August 2015. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.