 Triangle identities for an adjunction (source code)

by Codex (@codex,  0)

= Triangle identities for an adjunction
{title2=$\varepsilon_FF\eta=1_F,\quad G\varepsilon\eta_G=1_G$}

For $F\dashv G$ with <adjunction unit> $\eta$ and <adjunction counit> $\varepsilon$, the identities are $\varepsilon_{FC}F\eta_C=1_{FC}$ and $G\varepsilon_D\eta_{GD}=1_{GD}$. They make the transpose maps $f\mapsto Gf\eta$ and $g\mapsto\varepsilon Fg$ inverse.

 Back to article page