Fin C free on coproducts

Proof. We claim that an inverse is given by left Kan extension.

Step 1: Given a functor \(F\colon C \to D\), we show that its left Kan extension \(i_!F\) along \(i\) exists. By the pointwise formula for left Kan extensions, it suffices to show that each of the colimits \[ (i_!F)(x_1, \dots , x_n) = \colim _{y \in C_{/(x_1, \dots , x_n)}} F(y) \] exists. Observe that the canonical map \[ \bigsqcup _{k=1}^n C_{/x_k} \to C_{/(x_1, \dots , x_n)} := C \times _{\Fin (C)} \Fin (C)_{/(x_1, \dots , x_n)} \] sending \((\phi \colon y \to x_k)\) to the map \((\{k\} \hookrightarrow \lra {n}, \phi )\) is an equivalence. Since \(D\) has finite coproducts, we see that colimits indexed by the slices \(C_{/(x_1, \dots , x_n)}\) exist in \(D\) if and only if colimits indexed by each \(C_{/x_k}\) exist. But the latter is clear: as \(C_{/x_k}\) admits a terminal object, colimits always exist and are given by evaluation at that terminal object. This shows that \(i_!F\) exists and that it is given on objects by \[ (i_!F)(x_1, \dots , x_n) = F(x_1) \sqcup \dots \sqcup F(x_n). \]

Step 2: It follows from the pointwise description of \(i_!F\) that it preserves finite coproducts. In particular, the restriction functor thus admits a left adjoint \[ i_!\colon \Fun (C,D) \to \Fun ^{\amalg }(\Fin (C),D). \]

Step 3: We now show that the unit \(\id \to i^*i_!\) and counit \(i_!i^* \to \id \) are natural isomorphisms. The unit is a natural isomorphism because \(i\) is fully faithful. If \(G\colon \Fin (C)\to D\) preserves finite coproducts, then the counit evaluated at \((x_1,\dots ,x_n)\) is the canonical map \[ G(x_1)\sqcup \dots \sqcup G(x_n) \longrightarrow G(x_1,\dots ,x_n), \] which is an isomorphism because \((x_1,\dots ,x_n)\) is the coproduct of the singleton families \((x_i)\) in \(\Fin (C)\). □