I am doing an exercise in MacLane, in which three equivalent conditions for left-adjoint-left-inverses are to be proved. I have done the cycle of implications except for one point.
Let $G:A\rightarrow X$ be a functor and suppose there is a full, reflective subcategory $Y$ of $X$ and an iso $H:A\cong Y$ s.t. $G=KH$ where $K$ is the insertion. $G$ obviously has a left adjoint, and the counit is invertible, but I want to prove, in fact, that $\varepsilon $ is actually the identity.
Final edit: I have to prove that, under the given conditions, there exists a left adjoint $F$ to $G$ s.t the counit is the identity. Since $H$ is an isomorphism, it will suffice to show that $K$ has a left adjoint $L:X\rightarrow Y$ s.t. the counit is the identity. By hypothesis, $K$ has a left adjoint $F':X\rightarrow Y$ and the counit $\epsilon':F'K\rightarrow 1_{Y} $ of $F'\dashv K$ is an isomorphism, since $K$ is fully faithful.
Define $Lx$ = \begin{cases} x & x\in Y\ & \\ F'x & x\notin Y \end{cases}
I then define $\psi :F'\rightarrow L$ by $\psi_{x}$ = \begin{cases} \epsilon'_{x} & x\in Y\ & \\ id _{F'x} & x\notin Y \end{cases}
I will show that $L\dashv K$ and that the counit of this adjunction is the identity.
$L$ is a functor: Suppose $f:x\rightarrow x'$. There are four cases:
I. Both $x$ and $x'$ are in $Y$. In this case, we just take $Lf =f$
II. Neither $x$ nor $x'$ is in $Y$, in which case we take $Lf=F'f$
III. $x'$ is in $Y$ but $x$ is not. Then $f:x\rightarrow Kx'$ and so we may take $Lf:F'x\rightarrow x'$ to be the unique arrow given by the adjunction, which is $\epsilon'_{x'}\cdot F'f$
IV. $x$ is in $Y$ but $x'$ is not. In this case $f$ is an arrow: $x\rightarrow x'$ and $Lf$ is an arrow :$x\rightarrow F'x'$, which may be written $x\rightarrow KF'x'$, so we may define $Lf=F'f\cdot \eta' _{x}$
A tedious consideration of six cases shows that $L$ is a functor. Similarly, checking the various cases, using naturality of $\epsilon' $ and the fact that since $K$ is full, $K\epsilon' $ is invertible with inverse $\eta' _{K}$, we find that $\psi $ is a natural isomorphism.
The rest is easy: If $f:x\rightarrow Ky$, then the map that sends $f$ to $\epsilon '_{y}\cdot F'f\cdot \psi_{x} ^{-1}:Lx\rightarrow y$ is a natural bijection, and so establishes that $L\dashv K$. Using naturality of $\psi $, we write the bijection in terms of $L$ as $\epsilon '_{y}\cdot \psi _{ky}^{-1}\cdot Lf$, from which it is immediate that the counit $\epsilon :LK\rightarrow 1_{Y}$ is $\epsilon '_{y}\cdot \psi _{ky}^{-1}$. Now, $Ky=y\in Y$, so $\psi _{ky}^{-1} = \psi _{y}^{-1}=\epsilon '^{-1}_{y}$, by definintion of $\psi $ and so the counit $\epsilon $ is the identity.
Choose a left adjoint $L : \mathcal{X} \to \mathcal{A}$ for $G : \mathcal{A} \to \mathcal{X}$ and counit $\epsilon : L G \Rightarrow \mathrm{id}_{\mathcal{A}}$. Since $G : \mathcal{A} \to \mathcal{X}$ is fully faithful, $\epsilon$ is a natural isomorphism. Let $F : \mathcal{X} \to \mathcal{A}$ be defined on objects as follows: $$F x = \begin{cases} a & \text{if } x = G a \text{ for some } a \text{ in } A \\ L x & \text{otherwise} \end{cases}$$ This makes sense because $G : \mathcal{A} \to \mathcal{X}$ is injective on objects. Let $\phi_x : L x \to F x$ be $\epsilon_a : L G a \to a$ for $x = G a$ and $\mathrm{id}_x : L x \to L x$ otherwise. Then there is a unique way of making $F$ into a functor so that $\phi : L \Rightarrow F$ becomes a natural isomorphism. Moreover, $F : \mathcal{X} \to \mathcal{A}$ becomes a left adjoint for $G : \mathcal{A} \to \mathcal{X}$ with counit $\epsilon \bullet \phi^{-1} G : F G \Rightarrow \mathrm{id}$; but by construction, $\epsilon \bullet \phi^{-1} G = \mathrm{id}$, as required.