# Kerodon

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

Proposition 7.4.8.2. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a 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.5. Then $(e_{!} \circ f): K^{\triangleright } \rightarrow \operatorname{\mathcal{C}}_{D'}$ is a colimit diagram in the $\infty$-category

Proof of Proposition 7.4.8.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.4.8.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.7.20). 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.7.12, this is equivalent to the assertion that for every object $C \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes

7.55
$$\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}$$

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.19). 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{C}}) }( f, \underline{C})} \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleright }, \operatorname{\mathcal{D}}) }( U \circ f, U \circ \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 that 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.2.1 to identify $\theta _{u}$ with 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.7.12). $\square$