"Nice proof" that the unit of the left Kan extension of $F$ is an isomorphism, if $F$ is fully faithful

Let $F: \mathbf C \to \mathbf D, G: \mathbf C \to \mathbf E$ be functors. Assume that $\mathbf C$ is small, $\mathbf D$ is locally small and $\mathbf E$ is cocomplete. Then, I can compute the left Kan extension $\mathrm{Lan}_F(G)$ as a coend: \begin{equation} \mathrm{Lan}_F(G) = \int^c \mathbf D(F(c),-)\cdot G(c). \end{equation} Now, assume that $F$ is fully faithful. Then, if I consider $\mathrm{Lan}_F(G) \circ F$, I can compute: \begin{equation} \mathrm{Lan}_F(G) \circ F = \int^c \mathbf D(F(c),F(-)) \cdot G(c) \cong \int^c \mathbf C(c,-) \cdot G(c) \cong G, \end{equation} where the last isomorphism comes frome the co-Yoneda lemma. Now, what I want to show is not only that $\mathrm{Lan}_F(G) \circ F \cong G$, but that the unit of the Kan extension \begin{equation} \eta_G \colon G \to \mathrm{Lan}_F(G) \circ F \end{equation} is an isomorphism. I think that the above chain of isomorphisms actually gives the unit $\eta_G$ (MacLane in X.4.2 gives an explicit formula for that). Is there a "nice" proof of this? Or, a nice direct proof that $\eta$ is an isomorphism? I'm thinking of something which avoids trivial but tedious computations. This is the advantage of using end and coends, after all.

Solution 1:

There is a useful trick for dealing with this. The following appears as Lemma 1.3 in [Johnstone and Moerdijk, Local maps of toposes].

Proposition. Given an adjunction $$L \dashv R : \mathcal{D} \to \mathcal{C}$$ if $\mathrm{id}_{\mathcal{C}} \cong R L$ (as functors) then the unit $\eta : \mathrm{id}_{\mathcal{C}} \Rightarrow R L$ is (also) a natural isomorphism.

Proof. Let $\mu = R \epsilon L$, where $\epsilon : L R \Rightarrow \mathrm{id}_{\mathcal{D}}$ is the counit. Then (by the triangle identities), we have a monad. We can transport this structure along any natural isomorphism $\theta : \mathrm{id}_{\mathcal{D}} \Rightarrow R L$, so that e.g. $$\begin{array}{rcl} \mathrm{id}_{\mathcal{C}} & \overset{\theta}{\to} & \mathrm{id}_{\mathcal{C}} \\ {\scriptstyle \eta} \downarrow & & \downarrow {\scriptstyle \eta'} \\ \mathrm{id}_{\mathcal{C}} & \underset{\theta}{\to} & R L \end{array}$$ commutes. But (using naturality) any comonad structure $(\eta', \mu')$ on $\mathrm{id}_{\mathcal{C}}$ must consist of natural isomorphisms, so we deduce that the original $\eta$ and $\mu$ are also natural isomorphisms.　◼

Solution 2:

Another proof of the proposition in Zhen Lin's answer is to note that for any functors $F,G$ we have $1\cong GF$ implies $F$ is fully faithful, and if $F\dashv G$ then the unit is an isomorphism by mez's comment. (In fact full faithfulness of $F$ is equivalent to isomorphy of the unit.)