Kerodon

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

Corollary 7.7.2.31. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category which admits pullbacks, and let $\operatorname{ev}_{1}: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the cartesian fibration given by evaluation at $1 \in \Delta ^1$. Then a morphism $F: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ satisfies descent for $\operatorname{ev}_{1}$ if and only if, for every cartesian natural transformation $\beta : F' \rightarrow F$, the morphism $F': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a weak colimit diagram.

Proof. By virtue of Remark 7.7.2.11, $F$ is a descent diagram for $\operatorname{ev}_{1}$ if and only if, for every pair of cartesian transformations $\beta : F' \rightarrow F$ and $\gamma : G \rightarrow F$, the restriction map

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

is a homotopy equivalence. If we regard $\beta $ as fixed and allow $\gamma $ to vary, this is equivalent to the requirement that $F'$ is a weak colimit diagram. Corollary 7.7.2.31 now follows by allowing $\beta $ to vary. $\square$