# Kerodon

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

Theorem 5.3.7.7. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty$-categories, let $\pi : \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}$ be given by projection onto the second factor, let $\delta : \operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$ be the diagonal map. For every cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}$, precomposition with $\delta$ induces a trivial Kan fibration of $\infty$-categories

$\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}}).$

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.8), 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 (Proposition 5.3.7.1). 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

$\delta ^{\ast }: \operatorname{\mathcal{M}}\rightarrow \operatorname{Res}_{ \operatorname{\mathcal{C}}/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}) = \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}$

which fits into a commutative diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{M}}\ar [rr]^{ \delta ^{\ast } } \ar [dr]_{T} & & \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}\ar [dl]^{U''} \\ & \operatorname{\mathcal{C}}& }$

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

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{M}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{D}}}, \operatorname{\mathcal{E}}) \simeq \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

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.6.14), 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

$\delta ^{\ast }_{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{M}}\simeq \operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{D}}}( \{ C\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}, \operatorname{\mathcal{E}}) \rightarrow \{ C\} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{E}}$

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.6.23). $\square$