Kerodon

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

Proposition 5.5.2.3. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a locally cartesian fibration of simplicial sets and let $e: X \rightarrow Y$ be an edge of $\operatorname{\mathcal{D}}$. Then there exists a functor $G: \operatorname{\mathcal{C}}_{Y} \rightarrow \operatorname{\mathcal{C}}_{X}$ which is given by contravariant transport along $e$. Moreover, an arbitrary functor $G': \operatorname{\mathcal{C}}_{Y} \rightarrow \operatorname{\mathcal{C}}_{X}$ is given by contravariant transport along $e$ if and only if it is isomorphic to $G$ (as an object of the $\infty $-category of functors $\operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}}_{X} )$).

Proof. Replacing $q$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{C}}\rightarrow \Delta ^1$, we can reduce to the case where $\operatorname{\mathcal{D}}= \Delta ^1$ and $e$ is the unique nondegenerate edge of $\operatorname{\mathcal{D}}$. In this case, the simplicial set $\operatorname{\mathcal{C}}$ is an $\infty $-category and $q$ is a cartesian fibration. Let $\operatorname{\mathcal{C}}' \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$ denote the full subcategory spanned by those edges $e'$ of $\operatorname{\mathcal{C}}$ which are $q$-cartesian and satisfy $q(e') = e$. It follows from Proposition 5.5.1.4 that evaluation at the vertex $1 \in \Delta ^1$ induces a trivial Kan fibration of simplicial sets $u: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}_{Y}$. In particular, $u$ admits a section, which we can identify with a map of simplicial sets $h: \Delta ^1 \times \operatorname{\mathcal{C}}_{Y} \rightarrow \operatorname{\mathcal{C}}$. Setting $G = h|_{ \{ 0\} \times \operatorname{\mathcal{C}}_{Y} }$, we conclude that $h$ exhibits the functor $G$ as given by contravariant transport along $e$.

Let us regard $h$ as a morphism from $G$ to $\operatorname{id}_{\operatorname{\mathcal{C}}_{Y}}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}})$. Let $q': \operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}_ Y, \Delta ^1 )$ be the functor given by composition with $q$, so that $h$ is $q'$-cartesian (Theorem 5.5.1.1). Let $G': \operatorname{\mathcal{C}}_ Y \rightarrow \operatorname{\mathcal{C}}_{X}$ be any functor. There exists an isomorphism $u: G' \rightarrow G$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}}_{X} )$, then any choice of composition $h \circ u$ is a $q'$-cartesian morphism from $G'$ to $\operatorname{id}_{\operatorname{\mathcal{C}}_ Y}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}})$ (Corollary 5.4.2.5), which can therefore be identified with a morphism of simplicial sets $\Delta ^1 \times \operatorname{\mathcal{C}}_{Y} \rightarrow \operatorname{\mathcal{C}}$ which exhibits $G'$ as given by contravariant transport along $e$. Conversely, if $h': \Delta ^1 \times \operatorname{\mathcal{C}}_{Y} \rightarrow \operatorname{\mathcal{C}}$ exhibits $G'$ as given by contravaraint transport along $e$, then $h'$ can be regarded as a $q'$-cartesian morphism from $G'$ to $\operatorname{id}_{\operatorname{\mathcal{C}}_{Y}}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}_{Y}, \operatorname{\mathcal{C}})$ (Theorem 5.5.1.1), so that $G'$ is isomorphic to $G$ by virtue of Remark 5.4.3.9. $\square$