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

Suppose F⊣GF \dashv G is an adjunction, and G:B→AG : B \to A is fully faithful, then counit ε:FG→1B\varepsilon : FG \to 1_B is an isomorphism

Proof [local-2]

Forward direction [local-0]

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

  1. ε−1≫ε=idX\varepsilon^{-1} \gg \varepsilon = id_X

    Apply GG to get

    GG−1η=Gε−1≫Gε=idG(X)\boxed{G G^{-1} \eta = G \varepsilon^{-1}} \gg G \varepsilon = id_{G(X)}

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

  2. ε≫ε−1=idFG(X)\varepsilon \gg \varepsilon^{-1} = id_{FG(X)}

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

    Fη≫εFG(B)=εB≫ε−1=G−1ηF \eta \gg \varepsilon_{FG(B)} = \varepsilon_B \gg \boxed{\varepsilon^{-1} = G^{-1}\eta}

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

Backward direction [local-1]

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

FGf≫εY=εX≫fFGg≫εY=εX≫g\begin{align*}FGf \gg \varepsilon_Y = \varepsilon_X \gg f \\ FGg \gg \varepsilon_Y = \varepsilon_X \gg g\end{align*}

Replace GfGf with GgGg then we have εX≫f=εX≫g\varepsilon_X \gg f = \varepsilon_X \gg g, counit is an isomorphism and hence left-cancellable, f=gf = g.

For GG is full, we want to show every ff there is a aa such that Ga=fG a = f. Let a=εX−1≫φ−1fa = \varepsilon_X^{-1} \gg \varphi^{-1} f (where φ\varphi is the hom-set equivalence of adjunction), this is same as asking

G(εX−1)=ηGXG(\varepsilon_X^{-1}) = \eta_{GX}

because isomorphism property, we have

G(εX−1)= G(εX−1≫εX)= G(εX−1)≫G(εX)= ηGX≫G(εX)\begin{align*}&G(\varepsilon_X^{-1}) \\ =\ &G(\varepsilon_X^{-1} \gg \varepsilon_X) \\ =\ &G(\varepsilon_X^{-1}) \gg G(\varepsilon_X) \\ =\ &\eta_{GX} \gg G(\varepsilon_X)\end{align*}

now we use isomorphism to cancel right, so G(εX−1)=ηGXG(\varepsilon_X^{-1}) = \eta_{GX}.