Kerodon

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

Proposition 7.1.7.14. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibration of $\infty $-categories, let $C \in \operatorname{\mathcal{C}}$ be an object, and let $\overline{q}: K^{\triangleright } \rightarrow \operatorname{\mathcal{E}}_{C}$ be a diagram. Then $\overline{q}$ is a $U$-colimit diagram (in the sense of Definition 7.1.6.1) if and only if it is an edgewise $U$-colimit diagram (in the sense of Definition 7.1.7.9).

Proof. Set $q = \overline{q}_{K}$. By virtue of Proposition 7.1.6.19, $\overline{q}$ is a $U$-colimit diagram if and only if for every object $X \in \operatorname{\mathcal{E}}$, the diagram of Kan complexes

7.6
\begin{equation} \begin{gathered}\label{equation:relative-colimit-by-fiber-preliminary} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{E}}) }( \overline{q}, \underline{X}) \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{E}}) }( q, \underline{X}|_{K} ) \ar [d] \\ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}}) }( U \circ \overline{q}, U \circ \underline{X}) \ar [r] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( U \circ q, U \circ \underline{X}|_{K}) } \end{gathered} \end{equation}

is a homotopy pullback square, where $\underline{X} \in \operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{E}})$ denotes the constant diagram taking the value $X$. Since $U$ is an inner fibration, the vertical maps in (7.6) are Kan fibrations (Proposition 4.6.1.22 and Corollary 4.1.4.3). Using the criterion of Example 3.4.1.4, we see that (7.6) is a homotopy pullback square if and only if, for every vertex $u \in \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}}) }( U \circ \overline{q}, U \circ \underline{X})$, the induced map

\[ \xymatrix@R =50pt@C=50pt{ \{ u\} \times _{\operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{C}}) }( U \circ \overline{q}, U \circ \underline{X})} \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{E}}) }( \overline{q}, \underline{X}) \ar [d]^{\theta _ u} \\ \{ u|_{K} \} \times _{ \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( U \circ q, U \circ \underline{X}|_{K}) }\operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{E}}) }( q , \underline{X}|_{K}) } \]

is a homotopy equivalence of Kan complexes. Set $C' = U(X)$, so that $u$ can be identified with a morphism of simplicial sets $K^{\triangleleft } \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( C, C' )$ and the condition that $\theta _ u$ is a homotopy equivalence depends only on the homotopy class of $u$. Since the simplicial set $K^{\triangleright }$ is weakly contractible (Example 4.3.7.11), it suffices to check that $\theta _ u$ is a homotopy equivalence in the special case where $u$ is the constant morphism taking the value $e$, for some morphism $e: C \rightarrow C'$ in the $\infty $-category $\operatorname{\mathcal{C}}$. The desired result is now a reformulation of Remark 7.1.7.11. $\square$