CatDat

Implication Details

Claim: If a functor is fully faithful and is a right adjoint, then it is left-invertible and is monadic.

Proof: A direct proof of monadicity is possible and straight forward. Alternatively, one can use Beck's monadicity theorem, since a fully faithful functor $U$ is conservative and creates coequalizers of $U$-split pairs. For the left adjoint $L$ the counit $L \circ U \to \id$ is an isomorphism (since $U$ is fully faithful, see Prop. 3.4 at the nLab), which shows that $U$ is left-invertible.