Kerodon

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

Lemma 8.6.2.6. Let $\lambda = (\lambda _{-}, \lambda _{+} ): \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \times \operatorname{\mathcal{D}}_{+}$ be a coupling of $\infty $-categories and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{D}}_{+}$ be an isofibration. Then:

$(1)$

The projection map $\overline{V}: \operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$ is a cartesian fibration of $\infty $-categories.

$(2)$

Let $\widetilde{e}$ be a morphism in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$, corresponding to a morphism $e$ of $\operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$ and a functor $f_{e}: \Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$. Then $\widetilde{e}$ is $\overline{V}$-cartesian if and only if, for every morphism $u$ of $\Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}$ whose image in $\operatorname{\mathcal{D}}_{+}$ is an isomorphism, the image $f_{e}(u)$ is an isomorphism in $\operatorname{\mathcal{E}}$.

Proof. Unwinding the definitions, we have a pullback diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{ /\operatorname{\mathcal{D}}_{+}}( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \ar [r] \ar [d]^{\overline{V}} & \operatorname{Fun}( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \ar [d]^{\overline{V}'} \\ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} \ar [r] & \operatorname{Fun}( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{D}}_{+} ), } \]

where the lower horizontal map classifies the morphism $\lambda _{+}: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{+}$ and $\overline{V}'$ is given by composition with $U$. The functor $\lambda _{-}: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$ is a cocartesian fibration (Proposition 8.2.1.7) and therefore exponentiable (Proposition 5.3.6.1). It follows from Proposition 4.5.9.18 guarantees that $\overline{V}'$ is an isofibration, so that $\overline{V}$ is also an isofibration.

Let us say that a morphism $\widetilde{e}$ in the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is special if it satisfies the condition described in $(2)$. Let us identify $\widetilde{e}$ with a pair $(e, f_{e} )$, where $e: D' \rightarrow D$ is a morphism in the $\infty $-category $\operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$ and $f_{e}: \Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ is a functor of $\infty $-categories. Let $\pi : \Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}} \operatorname{\mathcal{D}}\rightarrow \Delta ^1$ be given by the projection map onto the first factor. Then $\pi $ is a cocartesian fibration, and a morphism $u$ of $\Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}} \operatorname{\mathcal{D}}$ is $\pi $-cocartesian if and only if its image in $\operatorname{\mathcal{D}}_{+}$ is an isomorphism (see Proposition 8.2.1.7). If this condition is satisfied, the assumption that $\widetilde{e}$ is special guarantees that $f_{e}( u )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}$, and is therefore $U$-cartesian (Proposition 5.1.1.9). Applying Lemma 5.3.6.11, we deduce that $\widetilde{e}$ is $\overline{V}'$-cartesian when regarded as a morphism of $\operatorname{Fun}( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$, and therefore also $\overline{V}$-cartesian when regarded as a morphism of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}_{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$.

To show that $\overline{V}$ is a cartesian fibration, it will suffice to show that if $(D, f_{D} )$ is an object of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$, then every morphism $e: C \rightarrow D$ in the $\infty $-category $\operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$ can be lifted to a special morphism $\widetilde{e}: (C, f_{C}) \rightarrow (D, f_{D} )$ in $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$. We first claim that the lifting problem

\[ \xymatrix@R =50pt@C=50pt{ \{ D\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}\ar [r]^-{ f_{D} } \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}\ar@ {-->}[ur]^{f_{e}} \ar [r] & \operatorname{\mathcal{D}}_{+} } \]

admits a solution $f_{e}$ which is $U$-right Kan extended from $\{ D\} \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}$. Using the criterion of Corollary 7.3.5.9, we are reduced to showing that if $u: X' \rightarrow X$ is a $\pi $-cocartesian morphism of $\Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}$ lying over the nondegenerate edge of $\Delta ^1$, then its image in $\operatorname{\mathcal{D}}_{+}$ can be lifted to a $U$-cartesian morphism $E \rightarrow f_{D}(X)$ in $\operatorname{\mathcal{E}}$. Since the image of $u$ in $\operatorname{\mathcal{D}}_{+}$ is an isomorphism (Proposition 8.2.1.7), this follows from our assumption that $U$ is an isofibration. Note that the functor $f_{e}$ carries every $\pi $-cocartesian morphism $u$ of $\Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}$ to an isomorphism in $\operatorname{\mathcal{D}}$ (if the image of $u$ in $\Delta ^1$ is degenerate, then $u$ is an isomorphism and this condition is automatically satisfied), so that $\widetilde{e} = (e, f_{e} )$ is a special morphism of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ having target $(D, f_ D)$. This completes the proof of $(1)$.

To complete the proof of $(2)$, it will suffice to show that every $\overline{V}$-cartesian morphism $\widetilde{e} = (C, f_{C}) \rightarrow (D, f_{D})$ of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is special. Let $e: C \rightarrow D$ denote the image of $\widetilde{e}$ in the $\infty $-category $\operatorname{\mathcal{D}}_{-}^{\operatorname{op}}$. Using the preceding argument, we can lift $e$ to a special morphism $\widetilde{e}': (C, f'_{C}) \rightarrow (D, f_{D} )$ of $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}^{+} }( \operatorname{\mathcal{D}}/ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ Write $\widetilde{e} = (e, f_ e )$ and $\widetilde{e}' = (e, f'_{e} )$. Since $\widetilde{e}'$ is also $\overline{V}$-cartesian, Remark 5.1.3.8 guarantees that the functors $f_{e}$ and $f'_{e}$ are isomorphic. In particular, if $u$ is a morphism of $\Delta ^1 \times _{ \operatorname{\mathcal{D}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}$ such that $f'_{e}(u)$ is an isomorphism in $\operatorname{\mathcal{E}}$, then $f_{e}(u)$ is also an isomorphism in $\operatorname{\mathcal{E}}$. It follows that the morphism $\widetilde{e}$ is also special, as desired. $\square$