Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 7.1.7.3. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $B$ be a simplicial set, and let $f: K \rightarrow \operatorname{Fun}(B,\operatorname{\mathcal{C}})$ be a diagram. Assume that, for every vertex $b \in B$, the composite diagram

\[ K \xrightarrow {f} \operatorname{Fun}(B,\operatorname{\mathcal{C}}) \xrightarrow { \operatorname{ev}_ b } \operatorname{\mathcal{C}} \]

admits a colimit in the $\infty $-category $\operatorname{\mathcal{C}}$. Then:

$(1)$

The diagram $f$ admits a colimit in $\operatorname{Fun}(B,\operatorname{\mathcal{C}})$.

$(2)$

Let $\overline{f}: K^{\triangleright } \rightarrow \operatorname{Fun}(B,\operatorname{\mathcal{C}})$ be an extension of $f$. Then $\overline{f}$ is a colimit diagram if and only if it is a levelwise colimit diagram.

Proof of Proposition 7.1.7.3. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $B$ be a simplicial set, and let $f: K \rightarrow \operatorname{Fun}(B,\operatorname{\mathcal{C}})$ be a diagram. Assume that, for every vertex $b \in B$, the composite diagram

\[ K \xrightarrow {f} \operatorname{Fun}(B,\operatorname{\mathcal{C}}) \xrightarrow { \operatorname{ev}_ b } \operatorname{\mathcal{C}} \]

admits a colimit in the $\infty $-category $\operatorname{\mathcal{C}}$. Applying Corollary 7.1.7.11, we see that $f$ can be extended to a levelwise colimit diagram $\overline{f}: K^{\triangleright } \rightarrow \operatorname{Fun}(B, \operatorname{\mathcal{C}})$. Applying Corollary 7.1.7.15, we see any such extension is a colimit diagram in $\operatorname{Fun}(B,\operatorname{\mathcal{C}})$. To complete the proof, it will suffice to show the converse: if $\overline{f}': K^{\triangleright } \rightarrow \operatorname{Fun}(B,\operatorname{\mathcal{C}})$ is any colimit diagram extending $f$ and $b \in B$ is a vertex, then $\operatorname{ev}_{b} \circ \overline{f}'$ is also a colimit diagram in $\operatorname{\mathcal{C}}$. In this case, the extension $\overline{f}'$ is isomorphic to $\overline{f}$ as an object of the $\infty $-category $\operatorname{Fun}(K^{\triangleright }, \operatorname{Fun}(B,\operatorname{\mathcal{C}}) )$. It follows that $\operatorname{ev}_{b} \circ \overline{f}'$ is isomorphic to $\operatorname{ev}_{b} \circ \overline{f}$ as an object of the $\infty $-category $\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}})$ and therefore a colimit diagram by virtue of Corollary 7.1.3.14. $\square$