Kerodon

Proof. Combine Theorem 7.7.2.8 with Remark 7.7.2.11. $\square$

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

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$

Proof. The first assertion follows from the observation that the forgetful functor $U: \operatorname{\mathcal{C}}_{/C} \rightarrow \operatorname{\mathcal{C}}$ is conservative and creates colimits (Proposition 7.1.4.20). To prove the converse, it will suffice to show that the functor $U$ preserves $K$-indexed colimits. If $\operatorname{\mathcal{C}}$ admits $K$-indexed colimits, this follows from Corollary 7.1.4.21. If $\operatorname{\mathcal{C}}$ admits finite products, then the functor $U$ has a right adjoint (given on objects by the construction $X \mapsto X \times C$; see Proposition 7.6.1.14) and therefore preserves $K$-indexed colits by virtue of Corollary 7.1.4.22. $\square$

Proof. The implication $(2) \Rightarrow (1) \Rightarrow (3)$ are immediate from the definitions. To prove the reverse implications, we note that if $\widetilde{F}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{/C}$ is a lift of $F$, then $\widetilde{F}$ is a weak colimit diagram in $\operatorname{\mathcal{C}}_{/C}$ if and only if $F$ is a weak colimit diagram in $\operatorname{\mathcal{C}}$. It will therefore suffice to show that this condition is satisfied if and only if $\widetilde{F}$ is a colimit diagram in $\operatorname{\mathcal{C}}_{/C}$. This follows from Proposition 7.7.2.26, since the $\infty $-category $\operatorname{\mathcal{C}}_{/C}$ admits finite products (Corollary 7.6.2.17). $\square$

Proof. Let $C \in \operatorname{\mathcal{C}}$ be the value of the diagram $F$ at the cone point of $K^{\triangleright }$, and let $\underline{C}: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ denote the constant diagram taking the value $C$. By virtue of Variant 7.7.1.14, a natural transformation $\gamma : G \rightarrow F$ is cartesian if and only if there exists a morphism $u: D \rightarrow C$ of $\operatorname{\mathcal{C}}$ and a pullback diagram

We may therefore assume without loss of generality that $F = \underline{C}$ is a constant diagram, and consider only constant natural transformations $\underline{u}: \underline{D} \rightarrow \underline{C}$ in the formulation of condition $(\ast )$.

Let $\widetilde{\operatorname{\mathcal{C}}}$ denote the oriented fiber product $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ C\} $. Then the pair $(F', \beta )$ can then be identified with a diagram $\widetilde{F}': K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$. $\beta $ then determines a lift of $F'$ to a diagram $\widetilde{F}: K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$. Let us abuse notation by writing $\underline{D}$ for the constant diagram $K^{\triangleright } \rightarrow \operatorname{\mathcal{D}}$ taking the value $D$ (regarded as an obejct of $\operatorname{\mathcal{D}}$ via the morphism $u$). Recall that Corollary 4.6.4.18 supplies an equivalence of the slice $\infty $-category $\operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})_{ / G }$ with the oriented fiber product

and $\operatorname{Fun}( K, \operatorname{\mathcal{C}})_{ / G|_{K} }$ by $\operatorname{Fun}(K, \operatorname{\mathcal{D}})$. We can therefore reformulate condition $(\ast )$ as follows:

$(\ast ')$

For every object $D \in \operatorname{\mathcal{D}}$, the restriction map

\[ \operatorname{Hom}_{ \operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}}) }( \widetilde{F}', \underline{D} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(K, \operatorname{\mathcal{D}})}( \widetilde{F}|_{K}, \underline{D}|_{K} ) \]

is a homotopy equivalence.

Using Corollary 7.1.6.14, we see that condition $(\ast ')$ is satisfied if and only if $\widetilde{F}'$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{D}}$. By virtue of Corollary 7.7.2.28 (and Remark 7.7.2.29), this is equivalent to the condition that $F$ is a weak colimit diagram. $\square$

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

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$

Proof of Theorem 7.7.2.8. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category which admits pullbacks and let $F: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ be a universal colimit diagram. Then, for every cartesian natural transformation $\beta : F' \rightarrow F$, the morphism $F': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a colimit diagram, and therefore a weak colimit diagram (Proposition 7.7.2.26). Applying Corollary 7.7.2.31, we deduce that $F$ is a descent diagram for the evaluation functor $\operatorname{ev}_{1}: \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$. The converse holds whenever every weak colimit diagram $F': K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ is a colimit diagram. By virtue of Proposition 7.7.2.26, this condition is satisfied if $\operatorname{\mathcal{C}}$ admits $K$-indexed colimits or finite products (which follows from the existence of a final object of $\operatorname{\mathcal{C}}$, since $\operatorname{\mathcal{C}}$ admits pullbacks: see Corollary 7.6.2.30). $\square$

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

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 :$

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$

Proof. Combine Corollary 7.7.2.33 with Proposition 7.7.2.26 and Theorem 7.7.2.8. $\square$