Kerodon

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

Corollary 7.7.2.32. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category which admits pullbacks and let $F: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ be a morphism. Then $F$ is a descent diagram for $\operatorname{ev}_{1}: \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ if and only if the following condition is satisfied:

$(\ast )$

For every morphism $u: C' \rightarrow C$ of $\operatorname{\mathcal{C}}$ and every lift of $F$ to a diagram $\widetilde{F}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C\} $, the composite map

\[ K^{\triangleright } \xrightarrow { \widetilde{F} } \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C \} \xrightarrow {u^{\ast }} \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C'\} \]

is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C'\} $.

Proof. Assume first that $F$ is a descent diagram for $\operatorname{ev}_{1}$. Fix a morphism $u: C' \rightarrow C$ and a lift of $F$ to a diagram $\widetilde{F}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ C\} $, which we can identify with a natural transformation $\beta : F \rightarrow \underline{C}$. Then $u^{\ast } \circ \widetilde{F}$ can be identified with a diagram $F': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ equipped with a natural transformation $\beta ': F' \rightarrow \underline{C}'$. Using the description of $u^{\ast }$ given by Proposition 7.6.2.20, we see that there is a levelwise pullback diagram

\[ \xymatrix { F' \ar [r]^{ \beta ' } \ar [d]^{\gamma } & \underline{C}' \ar [d]^{ \underline{u} } \\ F \ar [r]^{\beta } & \underline{C} } \]

in the $\infty $-category $\operatorname{Fun}(K,\operatorname{\mathcal{C}})$. It follows from Remark 7.7.1.11 and Example 7.7.1.6 that the natural transformation $\gamma $ is cartesian, so that $F'$ is a weak colimit diagram (Corollary 7.7.2.31). Applying Remark 7.7.2.29, we conclude that $u^{\ast } \circ \widetilde{F}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C'\} $.

We now prove the converse. Assume that condition $(\ast )$ is satisfied; we wish to show that $F$ is a descent diagram for $\operatorname{ev}_{1}$. By virtue of Corollary 7.7.2.31, it will suffice to show that for every cartesian natural transformation $\gamma : F' \rightarrow F$, the morphism $F': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a weak colimit diagram. Let $u: C' \rightarrow C$ denote the morphism of $\operatorname{\mathcal{C}}$ obtained by evaluating $\gamma $ at the cone point of $K^{\triangleright }$, so that Variant 7.7.1.14 supplies a levelwise pullback square $\sigma :$

7.83
\begin{equation} \begin{gathered}\label{equation:universal-colimit-preserved-by-base-change} \xymatrix { F' \ar [r]^{ \beta ' } \ar [d] & \underline{C}' \ar [d]^{ \underline{u} } \\ F \ar [r]^{\beta } & \underline{C} } \end{gathered} \end{equation}

in the $\infty $-category $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})$. Let us identify the lower and upper halves of (7.83) with diagrams $\widetilde{F}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C\} $ and $\widetilde{F}': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C' \} $. Since $\sigma $ is a levelwise pullback square, we can identify $\widetilde{F}'$ with the composition $u^{\ast } \circ \widetilde{F}$ (Proposition 7.6.2.20). Invoking assumption $(\ast )$, we see that $\overline{F}'$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C' \} $: that is, $F'$ is a weak colimit diagram. $\square$