Splitting a one-triangle adjunction idempotent (source code)

= Splitting a one-triangle adjunction idempotent

The <one-triangle adjunction idempotent> splits if and only if $G$ has a <left adjoint>. From a splitting $F\xrightarrow rH\xrightarrow sF$, define the new unit $Gr\,\eta$ and counit $\varepsilon s_G$; the absorption identities imply both <triangle identities for an adjunction>. Conversely, for $H\dashv G$ with unit $\psi:1\Rightarrow GH$ and counit $\varphi:HG\Rightarrow1$, the splitting maps are $r=\varepsilon_HF\psi$ and $s=\varphi_FH\eta$. Their composites are $rs=1_H$ and $sr=e$.