Kerodon

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

Corollary 5.3.1.8. Let $\operatorname{\mathcal{C}}$ be a category and let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a cocartesian fibration of $\infty $-categories. Then the diagram of functors

\[ \xymatrix@C =50pt@R=50pt{ & \operatorname{QCat}\ar [dr] & \\ \operatorname{\mathcal{C}}\ar [ur]^-{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } \ar [rr]_-{ \operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) } } & & \mathrm{h} \mathit{\operatorname{QCat}} } \]

commutes up to natural isomorphism, given by the construction

\[ (C \in \operatorname{\mathcal{C}}) \mapsto (\operatorname{ev}_{C}: \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) \rightarrow \operatorname{hTr}_{\operatorname{\mathcal{E}}/ \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( C) = \operatorname{\mathcal{E}}_{C} ). \]

Proof. It follows from Proposition 5.3.1.7 that for each object $C \in \operatorname{\mathcal{C}}$, the evaluation functor $\operatorname{ev}_{C}$ is a trivial Kan fibration, and therefore an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$. To complete the proof, it will suffice to show that the construction $C \mapsto \operatorname{ev}_{C}$ is a natural transformation: that is, for every morphism $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, the diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \ar [r]^{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } \ar [d]^{\operatorname{ev}_{C}} & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D) \ar [d]^{ \operatorname{ev}_{D} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{ f_{!} } & \operatorname{\mathcal{E}}_{D} } \]

commutes up to natural isomorphism. Let $s: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ be a section of the trivial Kan fibration $\operatorname{ev}_{C}$. Then the homotopy class $[s]$ is an inverse of $[ \operatorname{ev}_{C} ]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$. It will therefore suffice to show that the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \ar [r]^{ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } & \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(D) \ar [d]^{ \operatorname{ev}_{D} } \\ \operatorname{\mathcal{E}}_{C} \ar [r]^{ f_{!} } \ar [u]_{ s } & \operatorname{\mathcal{E}}_{D} } \]

commutes up to isomorphism: that is, that the composite functor

\[ \operatorname{\mathcal{E}}_{C} \xrightarrow {s} \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \xrightarrow { \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) } \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( D) \xrightarrow { \operatorname{ev}_{D} } \operatorname{\mathcal{E}}_{D} \]

is given by covariant transport along $f$.

Unwinding the definitions, we can identify the composition

\[ \operatorname{\mathcal{E}}_{C} \xrightarrow {s} \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( C ) \subseteq \operatorname{wTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ), \operatorname{\mathcal{E}}) \]

with a functor $H: \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$. Let us regard $\operatorname{id}_{C}$ and $f$ as objects of the category $\operatorname{\mathcal{C}}_{C/}$, so that $f$ lifts to a morphism $\widetilde{f}: \operatorname{id}_{C} \rightarrow f$ corresponding to an edge $e: \Delta ^1 \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} )$. Let $H_{e}$ denote the composition

\[ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \xrightarrow {e \times \operatorname{id}} \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}_{C/} ) \times \operatorname{\mathcal{E}}_{C} \xrightarrow {H} \operatorname{\mathcal{E}}. \]

Unwinding the definitions, we see that the commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{H_{e}} \ar [d] & \operatorname{\mathcal{E}}\ar [d]^{U} \\ \Delta ^1 \ar [r]^{f} & \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) } \]

witnesses the composite functor $\operatorname{ev}_{D} \circ \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(f) \circ s$ as given by covariant transport along $f$, in the sense of Definition 5.2.2.4. $\square$