Auxiliary cocartesian operad

Proof. Step 1: We start with some auxiliary diagrams. Consider the following commutative diagram:

In particular, passing to restriction functors induces a commutative diagram as follows:

The functor \(m^*\) is an equivalence, since \(\Fin \) is the free \(\infty \)-category with finite coproducts. The functor \(i^*\) was shown to be an equivalence in Lemma 14.1.17. It follows by 2-out-of-3 that \({\iota '}^*\) is an equivalence as well. Since the inverses to \(m^*\) and \(i^*\) are given by left Kan extension along \(m\) and \(i\), the inverse to \({\iota '}^*\) is given by left Kan extension along \(\iota '\).

Step 2: We now prove the following auxiliary statement: for every object \(X = \{x_i\}_{i \in I}\) of \(\Fin (C)\), the relative slice category of \(\iota '\) over \(X\) embeds fully faithfully into the relative slice category of \(\iota \) over \(X\), and this inclusion admits a left adjoint. To see this, let us denote these two relative slice categories as follows: \[ P_X := \Span _{\ct ,\all }(\Fin (C))_{/X} \times _{\Span _{\ct ,\all }(\Fin (C))} (\Span (\Fin ) \times C); \] \[ Q_X := \Fin (C)_{/X} \times _{\Fin (C)} (\Fin \times C). \] The inclusions \(l\) and \(k\) induce a fully faithful inclusion \(Q_X \hookrightarrow P_X\). We claim that this inclusion admits a left adjoint \(P_X \to Q_X\). To this end, note that an object of \(P_X\) consists of a pair \((J,y)\) and a span \[ \{y\}_{j \in J} \xleftarrow {(f, (\id _{y}))} \{y\}_{k \in K} \xrightarrow {(g, (\phi _k\colon y \to x_i))} \{x_i\}_{i \in I} = X \] in \(\Fin (C)\), where the left-pointing map is \(q\)-cartesian. We will send this to the object of \(Q_X\) given by the morphism \[ \{y\}_{k \in K} \xrightarrow {(g, (\phi _k\colon y \to x_i))} \{x_i\}_{i \in I} = X. \] If we include this back into \(P_X\) by taking the left-pointing map to be the identity, the span \(J\xleftarrow {f}K\xrightarrow {=}K\) and the identity of \(y\) define a morphism from the original object to the resulting object. Let \(L\colon P_X\to Q_X\) denote the construction just described and let \(j\colon Q_X\hookrightarrow P_X\) denote the inclusion. Composition with this morphism induces natural equivalences \[ \Hom _{Q_X}(L(p),q) \simeq \Hom _{P_X}(p,j(q)). \] Indeed, a morphism on the right is uniquely determined by its map from the middle object of the left leg, because that leg is \(q\)-cartesian. Thus \(L\) is left adjoint to \(j\).

Step 3: We now return to the question of interest by showing that \(\iota ^*\) admits a left adjoint given by left Kan extension. Consider a functor \(F\colon \Span (\Fin ) \times C \to D\) which preserves finite coproducts in the first variable. We need to show that the left Kan extension \(\iota _! F\colon \Span _{\ct ,\all }(\Fin (C)) \to D\) exists and preserves finite coproducts. For the former, we may use the pointwise criterion for left Kan extensions and show that for each object \(\{x_i\}_{i \in I}\) of \(\Span _{\ct ,\all }(\Fin (C))\) the colimit \[ (\iota _!F)(\{x_i\}_{i \in I}) = \colim _{(J,y) \in P_X} F(J,y) \] exists in \(D\), where \(P_X\) denotes the relative slice category of \(\iota \) considered in Step 2. Since the inclusion \(Q_X \hookrightarrow P_X\) is a right adjoint, it is in particular final, hence the above colimit exists in \(D\) if and only if so does \(\colim _{(J,y) \in Q_X} F(J,y)\). But this is indeed the case, since \(Q_X\) is the relative slice category of \(\iota '\) and the pointwise left Kan extension of \(l^*F\colon \Fin \times C \to D\) along \(\iota '\) exists by Step 1.

We conclude that \(\iota _!F\) exists, and that the canonical map \(\iota '_!l^*F \to k^*\iota _!F\) is a natural isomorphism. It remains to show that \(\iota _!F\) preserves finite coproducts, but this can be checked after restricting along the inclusion \(k\colon \Fin (C) \hookrightarrow \Span _{\ct ,\all }(\Fin (C))\), and thus follows from the fact that \(\iota '_!l^*F\) preserves finite coproducts.

Step 4: Finally, we show that the resulting adjunction \[ \iota _! \colon \Fun ^{\amalg , -}(\Span (\Fin ) \times C, D) \rightleftarrows \Fun ^{\amalg }(\Span _{\ct ,\all }(\Fin (C)), D)\noloc \iota ^* \] is an adjoint equivalence. Since \(\Fin (C)\) is generated under coproducts by the image of \(\Fin \times C\), the functor \(\iota ^*\) is conservative, hence it suffices to show that for every \(F \in \Fun ^{\amalg ,-}(\Span (\Fin ) \times C, D)\) the unit \(F \to \iota ^*\iota _!F\) is an isomorphism. By essential surjectivity of \(l\), this in turn reduces to \(l^*F \iso l^*\iota ^*\iota _!F\). Under the isomorphisms \(l^*\iota ^*\iota _!F = {\iota '}^*k^*\iota _!F \simeq {\iota '}^*\iota '_!l^*F\), this corresponds to the unit of the adjunction \(\iota '_! \dashv {\iota '}^*\), hence is an isomorphism by Step 1. □