Kerodon

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

Proposition 7.4.4.16. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a diagram having a limit $\varprojlim (\mathscr {F})$ and let $q: K \rightarrow \varprojlim ( \mathscr {F} )$ be a diagram. Assume that:

$(a)$

For each vertex $C \in \operatorname{\mathcal{C}}$, the diagram $q_{C}: K \rightarrow \varprojlim (\mathscr {F}) \rightarrow \mathscr {F}(C)$ admits a colimit in the $\infty $-category $\mathscr {F}(C)$.

$(b)$

For every edge $e: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the functor $\mathscr {F}(e): \mathscr {F}(C) \rightarrow \mathscr {F}(D)$ preserves the colimit of the diagram $q_{C}$.

Then the diagram $q$ admits a colimit in the $\infty $-category $\varprojlim (\mathscr {F})$. Moreover, a diagram $\overline{q}: K^{\triangleright } \rightarrow \varprojlim (\mathscr {F})$ extending $q$ is a colimit diagram if and only if it satisfies the following condition:

$(\ast )$

For every vertex $C \in \operatorname{\mathcal{C}}$, the composition $K^{\triangleright } \rightarrow \varprojlim (\mathscr {F}) \rightarrow \mathscr {F}(C)$ is a colimit diagram in the $\infty $-category $\mathscr {F}(C)$.

Proof. As in the proof of Proposition 7.4.4.15, we may assume that $\mathscr {F}$ is the covariant transport representation of a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, and that $\varprojlim (\mathscr {F})$ is the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ of cocartesian sections of $U$. Combining assumptions $(a)$ and $(b)$ with Corollary 7.1.10.3, we deduce that $q$ can be extended to a diagram $\overline{q}: K^{\triangleright } \rightarrow \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ satisfying condition $(\ast )$. Any such extension is automatically a colimit diagram (Proposition 7.4.4.15). Conversely, any colimit diagram $\overline{q}': K^{\triangleright } \rightarrow \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ extending $q$ is isomorphic to $\overline{q}$, and therefore also satisfies condition $(\ast )$. $\square$