Kerodon

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

Proposition 7.3.9.2. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a locally cocartesian fibration of $\infty $-categories, let $D \in \operatorname{\mathcal{D}}$ be an object, and let $f: K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D} = \{ D\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}$ be a diagram. Then $f$ is a $U$-colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}$ if and only if it satisfies the following condition:

$(\ast )$

Let $e: D \rightarrow D'$ be a morphism in the $\infty $-category $\operatorname{\mathcal{D}}$ and let $e_{!}: \operatorname{\mathcal{C}}_{D} \rightarrow \operatorname{\mathcal{C}}_{D'}$ be the covariant transport functor of Notation 5.2.2.9. Then $(e_{!} \circ f): K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D'}$ is a colimit diagram in the $\infty $-category

Proof of Proposition 7.3.9.2. For every morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$, we can choose a natural transformation $\alpha : f \rightarrow e_{!} \circ f$ carrying each vertex of $K^{\triangleright }$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{C}}$. It follows from Proposition 7.3.9.1 that if $f$ is a $U$-colimit diagram, then $e_{!} \circ f$ is also a $U$-colimit diagram, and therefore a colimit diagram in the $\infty $-category $\operatorname{\mathcal{C}}_{D'}$ (Corollary 7.1.6.22). This proves the necessity of condition $(\ast )$. For the converse, suppose that $f$ satisfies condition $(\ast )$; we wish to show that $f$ is a $U$-colimit diagram. By virtue of Proposition 7.1.6.12, this is equivalent to the assertion that for every object $C \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes

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

is a homotopy pullback square, where $\underline{C} \in \operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}})$ is the constant diagram taking the value $C$. Since $U$ is an inner fibration, the vertical maps in this diagram are Kan fibrations (Proposition 4.6.1.21 and Corollary 4.1.4.3). Using the criterion of Example 3.4.1.4, it will suffice to show that for every vertex $u \in \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}}) }( U \circ f, U \circ \underline{C} )$, the induced map

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

is a homotopy equivalence of Kan complexes. Set $D' = U(C)$, so that $u$ can be identified with a morphism of simplicial sets $K^{\triangleright } \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, D' )$, 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), we may assume without loss of generality that $u: K^{\triangleright } \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{D}}}( D, D' )$ is the constant map taking the value $e$, for some morphism $e: D \rightarrow D'$ in $\operatorname{\mathcal{D}}$. In this case, we can use Proposition 5.1.3.11 to replace $\theta _{u}$ by the restriction map

\[ \operatorname{Hom}_{ \operatorname{Fun}( K^{\triangleright }, \operatorname{\mathcal{C}}_{D'})}( e_{!} \circ f, \underline{D} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( K, \operatorname{\mathcal{C}}_{D'})}( e_{!} \circ f|_{K}, \underline{D}|_{K} ), \]

which is a homotopy equivalence by virtue of assumption $(\ast )$ (see Proposition 7.1.6.12). $\square$