One-triangle adjunction idempotent (source code)

= One-triangle adjunction idempotent
{title2=$e=\varepsilon_FF\eta$}

Let $F:\mathcal C\to\mathcal D$, $G:\mathcal D\to\mathcal C$, $\eta:1\Rightarrow GF$ and $\varepsilon:FG\Rightarrow1$ be <natural transformations>. If $G\varepsilon\,\eta_G=1_G$, then $e=\varepsilon_FF\eta:F\Rightarrow F$ is an <idempotent morphism> in the <functor category>. Naturality implies $Ge\,\eta=\eta$ and $\varepsilon e_G=\varepsilon$; these absorption identities prove $e^2=e$. The omitted triangle measures exactly whether $e=1_F$.