Lemma 11.9.7.7 (029S)

Lemma 11.9.7.7. Let $n$ be a positive integer, let $U: \operatorname{\mathcal{E}}\rightarrow \Delta ^ n$ be a cocartesian fibration of $\infty $-categories, and let $\operatorname{\mathcal{E}}_0 \subseteq \operatorname{\mathcal{E}}$ be the fiber product $\operatorname{\partial \Delta }^{n} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$. Suppose we are given a diagram $\mathscr {F}_0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ and a morphism $G_0: \operatorname{\mathcal{E}}_0 \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}'$ which is an equivalence of cocartesian fibrations over $\operatorname{\partial \Delta }^ n$. Then there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ satisfying $\mathscr {F}_0 = \mathscr {F}|_{\operatorname{\partial \Delta }^ n}$ and an equivalence $G: \operatorname{\mathcal{E}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ of cocartesian fibrations over $\Delta ^ n$ satisfying $G_0 = G|_{\operatorname{\mathcal{E}}'}$.

Proof of Lemma 11.9.7.7. Let $\operatorname{\mathcal{C}}$ denote the fiber $\{ 0\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}$. By virtue of Corollary 11.9.6.7, there exists a categorical pushout diagram

11.18

\begin{equation} \begin{gathered}\label{equation:relative-universality-for-simplex} \xymatrix@R =50pt@C=50pt{ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\ar [r] \ar [d] & \Delta ^ n \times \operatorname{\mathcal{C}}\ar [d]^{H} \\ \operatorname{\mathcal{E}}_0 \ar [r] & \operatorname{\mathcal{E}}} \end{gathered} \end{equation}

where $H|_{ \{ 0\} \times \operatorname{\mathcal{C}}}$ is the identity functor from $\operatorname{\mathcal{C}}$ to itself and, for every object $C \in \operatorname{\mathcal{C}}$, the induced map $H|_{\Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \operatorname{\mathcal{E}}$ carries each edge of $\Delta ^ n$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$. Let $G'_{0}$ denote the composite map

\[ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\xrightarrow { H|_{ \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}} } \operatorname{\mathcal{E}}_0 \xrightarrow {G_0} \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0. \]

Applying Lemma 11.9.7.6, we conclude that $\mathscr {F}_0$ and $G'_0$ admit extensions

\[ \mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}\quad \quad G': \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F} \]

having the property that, for every object $C \in \operatorname{\mathcal{C}}$, the restriction $G'|_{ \Delta ^ n \times \{ C\} }: \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F}$ carries each edge of $\Delta ^ n$ to a $V$-cocartesian morphism of $\int _{\Delta ^ n} \mathscr {F}$, where $V: \int _{\Delta ^ n} \mathscr {F} \rightarrow \Delta ^ n$ is the projection map.

Since (11.18) is a categorical pushout square, the induced diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } & \operatorname{Fun}( \Delta ^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [l] \\ \operatorname{Fun}( \operatorname{\mathcal{E}}_0, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [u] & \operatorname{Fun}( \operatorname{\mathcal{E}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [u] \ar [l] } \]

is a homotopy pullback diagram of Kan complexes, in which the horizontal maps are Kan fibrations (Corollary 4.4.5.4). Applying Example 3.4.1.4, we deduce that the map of fibers

\[ \xymatrix@R =50pt@C=50pt{ \{ G_0\} \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}', \int _{\Delta ^ n} \mathscr {F} )^{\simeq }} \operatorname{Fun}( \operatorname{\mathcal{E}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } \ar [d] \\ \{ G'_0 \} \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } } \operatorname{Fun}( \Delta ^ n \times \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} )^{\simeq } } \]

is a homotopy equivalence of Kan complexes. We may therefore assume (after replacing $G'$ by an isomorphic functor if necessary) that $G'$ factors as a composition

\[ \Delta ^ n \times \operatorname{\mathcal{C}}\xrightarrow {H} \operatorname{\mathcal{E}}\xrightarrow {G} \int _{\Delta ^ n} \mathscr {F}, \]

where $G|_{\operatorname{\mathcal{E}}_0} = G_0$. We will complete the proof by showing that $G$ is an equivalence of cocartesian fibrations over $\Delta ^ n$. Note that, since $G_0$ is an equivalence of cocartesian fibrations over $\operatorname{\partial \Delta }^ n$, it follows that $G$ restricts to an equivalence of $\infty $-categories $\{ i\} \times _{\Delta ^ n} \operatorname{\mathcal{E}}\rightarrow \{ i\} \times _{\Delta ^ n} \int _{\Delta ^ n} \mathscr {F}$ for $0 \leq i \leq n$. By virtue of the criterion of Proposition 5.1.7.15, it will suffice to show that $G$ carries every $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$ to a $V$-cocartesian morphism of $\int _{\Delta ^ n} \mathscr {F}$. If $n > 1$, this is automatic (since $\operatorname{\mathcal{E}}_0$ contains the $1$-skeleton of $\operatorname{\mathcal{E}}$). In the case $n=1$, it follows from Remark 5.1.6.8. $\square$