Kerodon

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

Theorem 5.3.5.6. Let $\operatorname{\mathcal{C}}$ be a category. Then the weighted nerve functor $\mathscr {F} \mapsto \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}})$ induces a bijection

\[ \xymatrix@R =50pt@C=50pt{ \{ \textnormal{Diagrams $\operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$} \} / \textnormal{Levelwise Equivalence} \ar [d] \\ \{ \textnormal{Cocartesian Fibrations $\operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$} \} / \textnormal{Equivalence}. } \]

The inverse bijection carries (the equivalence class of) a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ to (the equivalence class of) the strict transport representation $\operatorname{sTr}_{ \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}}$.

Proof of Theorem 5.3.5.6. Let $\operatorname{\mathcal{C}}$ be a category. It follows from Proposition 5.3.5.2 that the construction $\mathscr {F} \mapsto \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}})$ determines an injective function

\[ \xymatrix@R =50pt@C=50pt{ \{ \textnormal{Diagrams $\operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$} \} / \textnormal{Levelwise Equivalence} \ar [d]^{\Phi } \\ \{ \textnormal{Cocartesian Fibrations $\operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$} \} / \textnormal{Equivalence}. } \]

Moreover, the construction $(U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) ) \mapsto \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ carries equivalences of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ to levelwise categorical equivalences, and therefore induces a function

\[ \xymatrix@R =50pt@C=50pt{ \{ \textnormal{Cocartesian Fibrations $\operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$} \} / \textnormal{Equivalence} \ar [d]^{\Psi } \\ \{ \textnormal{Diagrams $\operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$} \} / \textnormal{Levelwise Equivalence} } \]

in the opposite direction. We will show that $\Phi \circ \Psi $ is equal to the identity; it will then follow that $\Phi $ is a bijection and that $\Psi = \Phi ^{-1}$ is the inverse bijection.

Fix a cocartesian fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$, let $\mathscr {F} = \operatorname{sTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ denote its strict transport representation, and let $U': \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be the projection map. We wish to show that $U$ and $U'$ are equivalent as cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$. Let $\lambda _{u}: \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{\mathcal{E}}$ denote the universal scaffold (Construction 5.3.4.7) and let $\lambda _{t}: \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}})$ denote the taut scaffold (Construction 5.3.4.11). Then $\lambda _{t}$ is a categorical equivalence of simplicial sets (Corollary 5.3.5.9). Applying Corollary 4.5.2.34, we see that precomposition with $\lambda _{t}$ induces an equivalence of $\infty $-categories

\[ \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}), \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}), \operatorname{\mathcal{E}}). \]

In particular, there exists a morphism $T: \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$ such that $U \circ T = U'$ and $T \circ \lambda _{t}$ is isomorphic to $\lambda _{u}$ (as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}), \operatorname{\mathcal{E}})$). Since $\lambda _{u}$ is a categorical equivalence of simplicial sets (Corollary 5.3.5.8), it follows that $T \circ \lambda _{t}$ is also a categorical equivalence of simplicial sets (Corollary 4.5.3.9). Applying the two-out-of-three property, we see that $T$ is an equivalence of $\infty $-categories (Remark 4.5.3.5) and therefore an equivalence of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ (Proposition 5.1.7.5). $\square$