Kerodon

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

Proposition 5.2.3.15. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories. Then:

  • The projection map $\pi : \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \Delta ^1$ is a cocartesian fibration of $\infty $-categories.

  • The map

    \[ \widetilde{F}: \Delta ^1 \times \operatorname{\mathcal{C}}\simeq ( \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}} \]

    witnesses the functor $F$ as given by covariant transport along the nondegenerate edge of $\Delta ^1$.

Proof of Proposition 5.2.3.15. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, so that the projection map $\pi : \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}\rightarrow \Delta ^{1}$ of Example 5.2.3.18 is a cocartesian fibration. Note that the morphism

\[ H: \Delta ^1 \times \operatorname{\mathcal{C}}\simeq \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}} \]

satisfies $H|_{ \{ 0\} \times \operatorname{\mathcal{C}}} = \operatorname{id}_{\operatorname{\mathcal{C}}}$ and $H|_{ \{ 1\} \times \operatorname{\mathcal{C}}} = F$. To complete the proof, it will suffice to show that for every object $C \in \operatorname{\mathcal{C}}$, the restriction $H|_{ \Delta ^1 \times \{ C\} }$ is a $\pi $-cocartesian morphism $e: X \rightarrow F(X)$ in the $\infty $-category $\operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}$. This follows from the criterion of Example 5.2.3.18, since $e$ corresponds to the identity morphism $\operatorname{id}_{ F(X) }: F(X) \rightarrow F(X)$ under the identification of Remark 5.2.3.14. $\square$