Kerodon

Proof of Theorem 5.3.7.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of $\infty $-categories, and let $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ be the diagonal embedding. Since $U$ is an isofibration (Proposition 5.1.4.9), the restriction map $\overline{\theta }: \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is also an isofibration (Corollary 4.5.5.16). Because $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$ is a replete full subcategory of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}})$, it follows that $\overline{\theta }$ restricts to an isofibration $\theta : \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$. To prove Theorem 5.3.7.7, we will show that $\theta $ is an equivalence of $\infty $-categories (it is then automatically a trivial Kan fibration of simplicial sets: see Proposition 4.5.5.20).

Note that the functor $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$ induces cocartesian fibrations $U': \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ and $U'': \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$. Let $\pi ': \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be given by projection onto the first factor, so that $\pi '$ is a cartesian fibration (Corollary 5.3.7.3). Let $\operatorname{\mathcal{M}}$ denote the cocartesian direct image $\operatorname{Res}^{\operatorname{CCart}}_{ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}/ \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}})$ and let $T: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{C}}$ be the projection map. Precomposition with the diagonal embedding $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ induces a restriction functor

which fits into a commutative diagram

It follows from Proposition 5.3.7.10 that $T$ is a cocartesian fibration and that $\delta ^{\ast }$ carries $T$-cocartesian morphisms of $\operatorname{\mathcal{M}}$ to $U''$-cocartesian morphisms of $\operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}$. Using Proposition 5.3.7.11, we can identify $\theta $ with the map

given by postcomposition with $\delta ^{\ast }$. Consequently, to show that $\theta $ is an equivalence of $\infty $-categories, it will suffice to show that $\delta ^{\ast }$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$. By virtue of Proposition 5.1.7.15), this can be checked fiberwise: that is, it suffices to show that for each object $C \in \operatorname{\mathcal{C}}$, the induced map of fibers

is an equivalence of $\infty $-categories. This is a special case of Corollary 5.3.1.22, since $\delta (C)$ is an initial object of the $\infty $-category $\{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ (Proposition 4.6.7.22). $\square$