Proposition. Right adjoint fully faithful <=> counit is isomorphism [math-000Y]

Suppose $F \dashv G$ is an adjunction, and $G : B \to A$ is fully faithful, then counit $\varepsilon : FG \to 1_B$ is an isomorphism

Proof

Forward direction

To prove counit $\varepsilon_B : FG(B) \to B$ is an isomorphism, we need to find an inverse $\varepsilon^{-1}$ and show pre and post composition of them are identity. Let $\varepsilon^{-1} := G^{-1}\eta$, then we have two targets

1. $\varepsilon^{-1} \gg \varepsilon = id_X$

   Apply $G$ to get

   $$\boxed{G G^{-1} \eta = G \varepsilon^{-1}} \gg G \varepsilon = id_{G(X)}$$

   hence the target is $\eta \gg G \varepsilon = id_{G(X)}$, right triangle fills the target.

2. $\varepsilon \gg \varepsilon^{-1} = id_{FG(X)}$

   Use counit naturality on $\varepsilon^{-1}$ to get

   $$F \eta \gg \varepsilon_{FG(B)} = \varepsilon_B \gg \boxed{\varepsilon^{-1} = G^{-1}\eta}$$

   Therefore, we have target $F \eta \gg \varepsilon_{FG(B)} = id_{FG(X)}$, left triangle fills the target.

Backward direction

For $G$ is faithful, we want to know if $Gf = Gg$ then $f = g$. We first obtain two equations via naturality of counit:

Replace $Gf$ with $Gg$ then we have $\varepsilon_X \gg f = \varepsilon_X \gg g$, counit is an isomorphism and hence left-cancellable, $f = g$.

For $G$ is full, we want to show every $f$ there is a $a$ such that $G a = f$. Let $a = \varepsilon_X^{-1} \gg \varphi^{-1} f$ (where $\varphi$ is the hom-set equivalence of adjunction), this is same as asking

because isomorphism property, we have

now we use isomorphism to cancel right, so $G(\varepsilon_X^{-1}) = \eta_{GX}$.