Kerodon

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

Corollary 5.2.4.4. Let $U: \operatorname{\mathcal{M}}\rightarrow \Delta ^1$ be a cocartesian fibration of $\infty $-categories and let $F: \operatorname{\mathcal{M}}_0 \rightarrow \operatorname{\mathcal{M}}_1$ be a functor. The following conditions are equivalent:

$(1)$

The functor $F$ is given by covariant transport along the nondegenerate edge of $\Delta ^1$ (in the sense of Definition 5.2.2.4).

$(2)$

There exists a functor $R: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_{1}$ such that $R|_{ \operatorname{\mathcal{M}}_0} = F$, $R|_{ \operatorname{\mathcal{M}}_1} = \operatorname{id}$, and $R$ carries $U$-cocartesian morphisms of $\operatorname{\mathcal{M}}$ to isomorphisms in $\operatorname{\mathcal{M}}_1$.

Proof. Let $e$ denote the nondegenerate edge of $\Delta ^1$. By virtue of Proposition 5.2.2.8, we can choose a functor $F': \operatorname{\mathcal{M}}_{0} \rightarrow \operatorname{\mathcal{M}}_{1}$ and a natural transformation $H: \Delta ^1 \times \operatorname{\mathcal{M}}_0 \rightarrow \operatorname{\mathcal{M}}$ which exhibits $F'$ as given by covariant transport along $e$. Let $R: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_1$ be a functor satisfying condition $(2)$. Then the composition

\[ \Delta ^1 \times \operatorname{\mathcal{M}}_0 \xrightarrow {H} \operatorname{\mathcal{M}}\xrightarrow {R} \operatorname{\mathcal{M}}_1 \]

can be regarded as a natural transformation from $R \circ H|_{ \{ 0\} \times \operatorname{\mathcal{M}}_0} = F$ to $R \circ H|_{ \{ 1\} \times \operatorname{\mathcal{M}}_1} = F'$. By assumption, this natural transformation carries each object of $\operatorname{\mathcal{M}}_0$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}_1$, and is therefore an isomorphism of functors (Theorem 4.4.4.4). It follows that the functor $F$ is also given by covariant transport along $e$ (see Proposition 5.2.2.8). This proves the implication $(2) \Rightarrow (1)$.

Now suppose that condition $(1)$ is satisfied. Then we can assume that $F' = F$, so that we have a commutative diagram of simplicial sets

\[ \xymatrix { \operatorname{\mathcal{M}}_0 \ar [r]^{F} \ar [d] & \operatorname{\mathcal{M}}_1 \ar [d] \\ \operatorname{\mathcal{M}}_0 \coprod \operatorname{\mathcal{M}}_0 \ar [r]^-{\operatorname{id}\coprod F} \ar [d] & \operatorname{\mathcal{M}}_0 \coprod \operatorname{\mathcal{M}}_1 \ar [d] \\ \Delta ^1 \times \operatorname{\mathcal{M}}_0 \ar [r]^{H} & \operatorname{\mathcal{M}}. } \]

The upper half of the diagram is a pushout square in which the vertical maps are monomorphisms, and therefore a categorical pushout square (Example 4.5.4.12). Theorem 5.2.4.1 guarantees that the outer rectangle is a categorical pushout square, so the lower half of the diagram is also a categorical pushout square (Proposition 4.5.4.8). It follows that the diagram of $\infty $-categories

\[ \xymatrix { \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{M}}_1) \ar [r]^{\circ H} \ar [d] & \operatorname{Fun}( \Delta ^1 \times \operatorname{\mathcal{M}}_0, \operatorname{\mathcal{M}}_1 ) \ar [d] \\ \operatorname{Fun}( \operatorname{\mathcal{M}}_0 \coprod \operatorname{\mathcal{M}}_1, \operatorname{\mathcal{M}}_1 ) \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{M}}_0 \coprod \operatorname{\mathcal{M}}_0 , \operatorname{\mathcal{M}}_1) } \]

is a categorical pullback square (Proposition 4.5.4.4). Since the vertical maps are isofibrations (Corollary 4.4.5.3), Corollary 4.5.2.32 implies that composition with $H$ induces an equivalence of $\infty $-categories

\[ \{ (F, \operatorname{id}) \} \times _{ \operatorname{Fun}( \operatorname{\mathcal{M}}_0 \coprod \operatorname{\mathcal{M}}_1, \operatorname{\mathcal{M}}_1) } \operatorname{Fun}( \operatorname{\mathcal{M}}, \operatorname{\mathcal{M}}_1) \xrightarrow {\circ H} \operatorname{Hom}_{ \operatorname{Fun}( \operatorname{\mathcal{M}}_0, \operatorname{\mathcal{M}}_1) }( F, F ). \]

It follows that we can choose a functor $R: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_1$ such that $R|_{ \operatorname{\mathcal{M}}_0 } = F$, $R|_{ \operatorname{\mathcal{M}}_1} = \operatorname{id}$, and the composition $R \circ H$ is homotopic to the identity (when regarded as a morphism from $F$ to itself in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{M}}_0, \operatorname{\mathcal{M}}_1)$). To complete the proof, it will suffice to show that if $f: X \rightarrow Y$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{M}}$, then $U(f)$ is an isomorphism. We may assume without loss of generality that $X$ belongs to $\operatorname{\mathcal{M}}_0$ and $Y$ belongs to $\operatorname{\mathcal{M}}_1$ (otherwise, $f$ is already an isomorphism and there is nothing to prove). In this case, Remark 5.1.3.8 guarantees that $f$ is isomorphic (as an object of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{M}})$) to the edge $H|_{ \Delta ^1 \times \{ X\} }$. It will therefore suffice to show that $(R \circ H)|_{ \Delta ^1 \times \{ X\} }$ is an isomorphism in $\operatorname{\mathcal{M}}_1$, which is clear (since it is homotopic to the identity morphism from $F(X)$ to itself). $\square$