Faithful left adjoint criterion
= Faithful left adjoint criterion
For $F\dashv G$, the left adjoint $F$ is <faithful functor>[faithful] exactly when every unit component $\eta_A:A\to GFA$ is a <monomorphism>. Under the adjunction, equality after $\eta_A$ corresponds precisely to equality after applying $F$.