# Kerodon

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

Lemma 8.8.1.3. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a diagram and let $X$ be a simplicial set. Then the comparison map

$\theta : \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} )$

of Construction 8.8.1.2 is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$.

Proof. Let $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \operatorname{\mathcal{C}}$ and $V: \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} ) \rightarrow \operatorname{\mathcal{C}}$ be the projection maps. By virtue of Proposition 5.1.6.14, it will suffice to prove the following:

$(1)$

For every vertex $C \in \operatorname{\mathcal{C}}$, the map of fibers

$\theta _{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X} \rightarrow \{ C\} \times _{ \operatorname{Fun}(X, \operatorname{\mathcal{C}}) } \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}} \mathscr {F} )$

is an equivalence of $\infty$-categories.

$(2)$

The morphism $\theta$ carries carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $V$-cocartesian edges of $\operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(X,\operatorname{\mathcal{C}})} \operatorname{Fun}(X, \int _{\operatorname{\mathcal{C}}}( \mathscr {F} ))$.

We first prove $(2)$. By virtue of Remark 5.1.1.11 and Theorem 5.2.1.1, it will suffice to show that for each vertex $x \in X$, the evaluation map $\mathscr {F}^{X} \rightarrow \mathscr {F}^{\{ x\} } \simeq \mathscr {F}$ carries $U$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}^{X}$ to $U'$-cocartesian edges of $\int _{\operatorname{\mathcal{C}}} \mathscr {F}$, where $U': \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ is the projection map. This follows immediately from Remark 8.8.1.1.

To prove $(1)$, we can assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^{0}$ is a $0$-simplex, in which case the diagram $\mathscr {F}: \Delta ^{0} \rightarrow \operatorname{\mathcal{QC}}$ correponds to an $\infty$-category $\operatorname{\mathcal{E}}$ and $\theta$ corresponds to a functor of $\infty$-categories from $\int _{\Delta ^{0}} \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ to $\operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}})$. Let $\theta _{\operatorname{\mathcal{E}}}: \operatorname{\mathcal{E}}\rightarrow \int _{\Delta ^{0}} \operatorname{\mathcal{E}}$ and $\rho _{ \operatorname{Fun}(X,\operatorname{\mathcal{E}})}: \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \rightarrow \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}})$ be the comparison maps described in Example 5.5.4.16. Unwinding the definitions, we see that the composition

$\operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow {\rho _{\operatorname{Fun}(X,\operatorname{\mathcal{E}})}} \int _{ \Delta ^{0} } \operatorname{Fun}(X, \operatorname{\mathcal{E}}) \xrightarrow { \theta } \operatorname{Fun}(X, \int _{\Delta ^{0}} \operatorname{\mathcal{E}})$

coincides with the map given by postcomposition with $\rho _{\operatorname{\mathcal{E}}}$. It follows from Example 5.5.4.16 that $\rho _{\operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ and $\theta \circ \rho _{ \operatorname{Fun}(X, \operatorname{\mathcal{E}})}$ are equivalences of $\infty$-categories, so that $\theta$ is also an equivalence of $\infty$-categories (Remark 4.5.1.18). $\square$