Lemma 8.6.2.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories and let $\overline{V}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}})/ \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ be the cartesian fibration of Lemma 8.6.2.6. Then:
- $(1)$
Let $\widetilde{e}: (C, f_ C) \rightarrow (D, f_{D} )$ be a $\overline{V}$-cartesian morphism of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}})/ \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$. If $(D,f_ D)$ belongs to the simplicial subset $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ of Construction 8.6.2.2, then $(C, f_ C)$ also belongs to $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$.
- $(2)$
The morphism $\overline{V}$ restricts to a cartesian fibration of $\infty $-categories
\[ V:\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}. \]
- $(3)$
A morphism in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is $V$-cartesian if and only if it is $\overline{V}$-cartesian when regarded as a morphism of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}})/ \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$.
Proof.
We will prove assertion $(1)$; assertions $(2)$ and $(3)$ then follow as formal consequences (see Proposition 5.1.4.17). Let us identify $\widetilde{e}$ with a pair $(e, f_{e} )$, where $e: C \rightarrow D$ is a morphism in the $\infty $-category $\operatorname{\mathcal{C}}^{\operatorname{op}}$ and $f_{e}: \Delta ^1 \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ is a functor. Let $u: \widetilde{C} \rightarrow \widetilde{C}'$ be a morphism in the fiber $\{ C \} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$; we wish to show that $f_{C}(u)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$. Since the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \Delta ^1$ is a cocartesian fibration, we can choose a diagram
\[ \xymatrix@R =50pt@C=50pt{ \widetilde{C} \ar [d]^{u} \ar [r] & \widetilde{D} \ar [d]^{v} \\ \widetilde{C}' \ar [r] & \widetilde{D}' } \]
in the $\infty $-category $\Delta ^1 \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$, where $v$ is a morphism of $\{ D \} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$ and the horizontal maps are $\pi $-cocartesian. Applying the functor $f_{e}$, we obtain a diagram
\[ \xymatrix@R =50pt@C=50pt{ f_{C}(\widetilde{C}) \ar [d]^{f_{C}(u)} \ar [r] & f_{D}(\widetilde{D}) \ar [d]^{f_{D}(v)} \\ f_{C}(\widetilde{C}') \ar [r] & f_{D}(\widetilde{D}' )} \]
in the $\infty $-category $\operatorname{\mathcal{E}}$, where the horizontal maps are isomorphisms (by virtue of our assumption that $\widetilde{e}$ is $\overline{V}$-cartesian; see Lemma 8.6.2.6). It will therefore suffice to show that $f_{D}(v)$ is $U$-cocartesian (Corollary 5.1.2.5), which follows from our assumption that $(D,f_{D})$ is an object of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$.
$\square$