Kerodon

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

Corollary 7.7.2.19. Let $K$ be a simplicial set and let $\operatorname{\mathcal{C}}$ be an $\infty $-category which admits pullbacks and $K$-indexed colimits. Then a morphism $F: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a strongly universal colimit diagram if and only if it satisfies the following condition:

$(\ast )$

A natural transformation $\gamma : G \rightarrow F$ in $\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}})$ is cartesian if and only if the restriction $\gamma |_{K}: G|_{K} \rightarrow F|_{K}$ is cartesian and $G$ is a colimit diagram.

Proof. Assume first that $F$ is a strongly universal colimit diagram. Then $F$ is a universal colimit diagram (Remark 7.7.2.14). Consequently, if we are given cartesian natural transformation $\gamma : G \rightarrow F$, then $G: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a colimit diagram. Conversely, suppose we are given a natural transformation $\gamma : G \rightarrow F$ where $G$ is a colimit diagram and $\gamma |_{K}$ is cartesian. Our assumption that $F$ is a strongly universal colimit diagram guarantees that we can lift $\gamma |_{K}$ to a cartesian natural transformation $\gamma ': G' \rightarrow F$. Since $F$ is a universal colimit diagram, $G'$ is a colimit diagram. It follows that the identity transformation $\operatorname{id}: G|_{K} \rightarrow G|_{K}$ admits an essentially unique lift to a natural transformation $G' \rightarrow G$. Our assumption that $G$ is a colimit diagram guarantees that this natural transformation is an isomorphism (Proposition 7.1.3.13). We may therefore assume without loss of generality that $G' = G$. In this case, to show that $\gamma $ is cartesian, it will suffice to show that it is homotopic to the $\gamma '$. By construction $\gamma $ and $\gamma '$ have the same image under the restriction map

\[ \rho : \operatorname{Hom}_{ \operatorname{Fun}(K^{\triangleright },\operatorname{\mathcal{C}})}( G, F ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( G|_{K}, F|_{K} ). \]

The desired result now follows from the observation that $\rho $ is a homotopy equivalence (since $G$ is a colimit diagram; see Proposition 7.1.7.4).

We now prove the converse. Assume that condition $(\ast )$ is satisfied; we wish to show that the restriction functor $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})_{ /F}^{\operatorname{Cart}} \rightarrow \operatorname{Fun}( K, \operatorname{\mathcal{C}})_{ /F|_{K}}^{\operatorname{Cart}}$ is an equivalence of $\infty $-categories. It follows from Theorem 7.7.2.8 that the functor $\theta $ is fully faithful. Consequently, to show that it is an equivalence of $\infty $-categories, it will suffice to show that it is surjective on objects (Theorem 4.6.2.21). Fix a diagram $G_0: K \rightarrow \operatorname{\mathcal{C}}$ and a cartesian natural transformation $\gamma _0: G_0 \rightarrow F|_{K}$. Our assumption that $\operatorname{\mathcal{C}}$ admits $K$-indexed colimits guarantees that we can extend $G_0$ to a colimit diagram $G: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. As above, the restriction map $\rho $ is a homotopy equivalence, hence a trivial Kan fibration; we can therefore extend $\gamma _0$ to a natural transformation $\gamma : G \rightarrow F$. Condition $(\ast )$ then guarantees that $\gamma $ is cartesian, so that the pair $(G,\gamma )$ is a lift of $(G_0, \gamma _0)$ to the $\infty $-category $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})_{ /F}^{\operatorname{Cart}}$. $\square$