Kerodon

Example 7.1.7.10. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of simplicial sets, let $C \in \operatorname{\mathcal{C}}$ be a vertex, and let $\overline{f}: K^{\triangleright } \rightarrow \operatorname{\mathcal{E}}_{C}$ be a morphism of simplicial sets. If $\overline{f}$ is an edgewise $U$-colimit diagram (in the sense of Definition 7.1.7.9), then it is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$. The converse holds if $U$ is a locally cartesian fibration. To see this, let $e: C \rightarrow C'$ be an edge of $\operatorname{\mathcal{C}}$ and let $\operatorname{\mathcal{E}}'$ denote the fiber product $\Delta ^1 \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. We wish to show that the inclusion map $\operatorname{\mathcal{E}}_{C} \simeq \{ 0\} \times _{\Delta ^1} \operatorname{\mathcal{E}}$ carries colimit diagrams in $\operatorname{\mathcal{E}}_{C}$ to colimit diagrams in $\operatorname{\mathcal{E}}'$. This is a special case of Variant 7.1.4.26, since $\operatorname{\mathcal{E}}_{C}$ is a coreflective subcategory of $\operatorname{\mathcal{E}}'$ (see Corollary 6.2.5.2).