Kerodon

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

Lemma 11.9.7.6. Let $n$ be a positive integer, let $\mathscr {F}_0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{QC}}$ be a diagram, let $V_0: \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \rightarrow \operatorname{\partial \Delta }^ n$ denote the projection map, let $\operatorname{\mathcal{C}}$ be an $\infty $-category, and let $G_0: \operatorname{\partial \Delta }^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0$ be a morphism in $(\operatorname{Set_{\Delta }})_{/\operatorname{\partial \Delta }^ n}$ with the following properties:

$(1)$

The morphism

\[ G_0|_{ \{ 0\} \times \operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \{ 0\} \times _{ \operatorname{\partial \Delta }^ n} \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \]

is a categorical equivalence of simplicial sets.

$(2')$

For each object $C \in \operatorname{\mathcal{C}}$, the restriction

\[ G_0|_{ \operatorname{\partial \Delta }^ n \times \{ C\} }: \operatorname{\partial \Delta }^ n \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 \]

carries each edge of $\operatorname{\partial \Delta }^ n$ to a $V_0$-cocartesian edge of $\int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0$.

Then there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ extending $\mathscr {F}_0$ and a functor $G: \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ which extends $G_0$ and satisfies the following stronger version of $(2')$:

$(2)$

For each 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 edge of $\int _{\Delta ^ n} \mathscr {F}$, where $V: \int _{\Delta ^ n} \mathscr {F} \rightarrow \Delta ^ n$ is the projection map.

Proof. Let us identify $G_0$ with a morphism of simplicial sets

\[ \tau _0: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\partial \Delta }^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) } \operatorname{Fun}( X, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 ), \]

and let $\theta _0: \int _{ \operatorname{\partial \Delta }^{n} } \mathscr {F}_0^{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\partial \Delta }^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0 )$ be the comparison map of Construction 11.9.7.2. It follows from Lemma 11.9.7.3 that there exists a morphism $\sigma _0: \operatorname{\partial \Delta }^ n \rightarrow \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}_0^{\operatorname{\mathcal{C}}}$ such that $\tau _0$ is isomorphic to $\theta _0 \circ \sigma _0$ as an object of the $\infty $-category

\[ \operatorname{Fun}_{ / \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) }( \operatorname{\partial \Delta }^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}') ). \]

It follows from assumptions $(1)$ and $(2')$ that the morphism $\sigma _0$ satisfies the hypotheses of Lemma 11.9.7.4. Consequently, there exists a functor $\mathscr {F}: \Delta ^ n \rightarrow \operatorname{\mathcal{QC}}$ extending $\mathscr {F}_0$ and a functor $\sigma : \Delta ^ n \rightarrow \int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}}$ extending $\sigma _0$ which carries each edge of $\Delta ^ n$ to a $V$-cocartesian edge of $\int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}}$, where $V: \int _{\Delta ^ n} \mathscr {F}^{\operatorname{\mathcal{C}}} \rightarrow \Delta ^ n$ is the projection map. Construction 11.9.7.2 then supplies a comparison map

\[ \theta : \int _{ \Delta ^{n} } \mathscr {F}^{\operatorname{\mathcal{C}}} \rightarrow \Delta ^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) \]

extending $\theta _0$. By construction, $(\theta \circ \sigma )|_{\operatorname{\partial \Delta }^ n}$ is isomorphic to $\tau _0$ as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\partial \Delta }^ n) }( \operatorname{\partial \Delta }^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\operatorname{\partial \Delta }^ n} \mathscr {F}') )$. Applying Proposition 4.4.5.8 (and Proposition 4.4.4.9), we deduce that $\tau _0$ can be extended to a map

\[ \tau : \Delta ^ n \rightarrow \Delta ^ n \times _{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n) } \operatorname{Fun}( \operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) \]

which is isomorphic to $\theta \circ \sigma $ as an object of the $\infty $-category $\operatorname{Fun}_{/\operatorname{Fun}(\operatorname{\mathcal{C}}, \Delta ^ n)}( \Delta ^ n, \operatorname{Fun}(\operatorname{\mathcal{C}}, \int _{\Delta ^ n} \mathscr {F} ) )$. Unwinding the definitions, we see can identify $\tau $ with a functor $G: \Delta ^ n \times \operatorname{\mathcal{C}}\rightarrow \int _{\Delta ^ n} \mathscr {F}$ which extends $G_0$ and satisfies $(2')$. $\square$