Fully faithful adjoint criterion (source code)

= Fully faithful adjoint criterion

For $F\dashv G$, the right adjoint $G$ is <full and faithful functor>[full and faithful] exactly when the counit $FG\to1$ is an isomorphism. Dually, $F$ is full and faithful exactly when the unit $1\to GF$ is an isomorphism.