Kerodon

Proof of Proposition 5.3.5.2. Assume first that the functors $\mathscr {F}_0, \mathscr {F}_1: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ are levelwise equivalent. Then there exists a functor $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ together with levelwise categorical equivalences $\mathscr {F}_0 \rightarrow \mathscr {F} \leftarrow \mathscr {F}_1$. Applying Corollary 5.3.3.20, we see that the induced maps $\operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \leftarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ are equivalences of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$.

We now prove the converse. Suppose that there exists a functor $T: \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ which is an equivalence of cocartesian fibrations over $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$. Let $\lambda _0: \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}_0) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_0}(\operatorname{\mathcal{C}})$ and $\lambda _{1}: \underset { \longrightarrow }{\mathrm{holim}}(\mathscr {F}_1) \rightarrow \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}})$ be the taut scaffolds of Construction 5.3.4.11. Then $T \circ \lambda _0$ is a scaffold of the cocartesian fibration $U_1$ (Remark 5.3.4.6). Applying Remark 5.3.4.10, we obtain levelwise categorical equivalences $\mathscr {F}_0 \rightarrow \operatorname{sTr}_{ \operatorname{N}_{\bullet }^{\mathscr {F}_1}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}} \leftarrow \mathscr {F}_1$. $\square$

Proof. Combine Theorem 5.3.5.7 with Proposition 5.3.4.8. $\square$

Proof. Using Proposition 4.1.3.2, we can choose a diagram of $\infty $-categories $\mathscr {F}': \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ and a levelwise categorical equivalence $\alpha : \mathscr {F} \rightarrow \mathscr {F}'$. We then have a commutative diagram of simplicial sets

where the horizontal maps are given by Construction 5.3.4.11 and the vertical maps are induced by the natural transformation $\alpha $. Since $\alpha $ is a levelwise categorical equivalence, Variant 5.3.2.19 and Corollary 5.3.3.20 guarantee that the vertical maps are categorical equivalences of simplicial sets. Consequently, to show that $\lambda _{t}$ is a categorical equivalence, it will suffice to show that $\lambda '_{t}$ is a categorical equivalence. This is a special case of Theorem 5.3.5.7, since $\lambda '_{t}$ is a scaffold of the cocartesian fibration $\operatorname{N}_{\bullet }^{\mathscr {F}'}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ (Proposition 5.3.4.17). $\square$

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

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

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

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$

Proof of Theorem 5.3.5.7. We first show that $(1)$ implies $(2)$. Assume that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is a cocartesian fibration of simplicial sets and let $\lambda : \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{\mathcal{E}}$ be a scaffold of $U$; we wish to show that $\lambda $ is a categorical equivalence of simplicial sets. By virtue of Corollary 4.5.7.3, it will suffice to show that for every $n$-simplex $\sigma : \Delta ^ n \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$, the induced map

is a categorical equivalence of simplicial sets. We may therefore assume without loss of generality that the category $\operatorname{\mathcal{C}}$ is a linearly ordered set of the form $[n] = \{ 0 < 1 < \cdots < n \} $ for some $n \geq 0$.

We proceed by induction on $n$. If $n = 0$, the result is clear. Let us therefore assume that $n > 0$. Let $S = \operatorname{N}_{\bullet }( \{ 1 < \cdots < n \} )$ be the $0$th face of the simplex $\Delta ^ n$ and set $\operatorname{\mathcal{E}}_{+} = S \times _{\Delta ^ n} \operatorname{\mathcal{E}}$. Let $\mathscr {F}_{+}$ denote the restriction of $\mathscr {F}$ to the subcategory $\{ 1 < \cdots < n \} \subset [n]$, so that our inductive hypothesis guarantees that $\lambda $ restricts to a categorical equivalence $\lambda _{+}: \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F}_{+}) \rightarrow \operatorname{\mathcal{E}}_{+}$. Note that Remark 5.3.2.12 supplies an isomorphism of simplicial sets

Let $V: \Delta ^{n} \rightarrow \Delta ^1$ be the morphism given on vertices by the formula $V(i) = \begin{cases} 0 & \textnormal{ if } i = 0 \\ 1 & \textnormal{ if } i > 0.\end{cases}$ Then $V$ is a cocartesian fibration of simplicial sets, and the edge $\operatorname{N}_{\bullet }( \{ 0 < 1 \} ) \subseteq \Delta ^ n$ is $V$-cocartesian. It follows that, for every vertex $x$ of the simplicial set $\mathscr {F}(0)$, the composite map

is a $(V \circ U)$-cocartesian edge of $\operatorname{\mathcal{E}}$. Applying Theorem 5.2.4.1 to the cocartesian fibration $V \circ U$, we deduce that the composition

is a categorical equivalence of simplicial sets. Consequently, to show that $\lambda $ is a categorical equivalence of simplicial sets, it will suffice to show that $\iota $ is inner anodyne. By construction, $\iota $ is a pushout of the inclusion map

By virtue of Lemma 1.5.7.5, it will suffice to show that the inclusion map $\Delta ^1 {\coprod }_{ \{ 1\} } S \hookrightarrow \Delta ^ n$ is inner anodyne. This is a special case of Example 4.3.6.5, since the inclusion $\{ 1\} \hookrightarrow S$ is left anodyne (Lemma 4.3.7.8).

We now show that $(2)$ implies $(1)$. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ be a functor of $\infty $-categories, and suppose that $\lambda : \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence of simplicial sets such that $U \circ \lambda $ is equal to the projection map $ \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$. We first claim that $U$ is an isofibration of $\infty $-categories. Since $\operatorname{\mathcal{E}}$ is an $\infty $-category, the morphism $U$ is an inner fibration (Proposition 4.1.1.10). It will therefore suffice to show that, for each object $\widetilde{C} \in \operatorname{\mathcal{E}}$ having image $C = U( \widetilde{C} ) \in \operatorname{\mathcal{C}}$ and every isomorphism $e: C \rightarrow D$ of $\operatorname{\mathcal{C}}$, there exists an isomorphism $\widetilde{e}: \widetilde{C} \rightarrow \widetilde{D}$ in $\operatorname{\mathcal{E}}$ satisfying $U( \widetilde{e} ) = e$. Since $\lambda $ is a categorical equivalence, we can choose a vertex $v$ of $ \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} )$ and an isomorphism $\widetilde{f}: \widetilde{C} \rightarrow \lambda (v)$ in $\operatorname{\mathcal{E}}$. Let us identify $v$ with a pair $(C',X)$, where $C'$ is an object of $\operatorname{\mathcal{C}}$ and $X$ is a vertex of the simplicial set $\mathscr {F}(C')$. Then $f = U( \widetilde{f} )$ is an isomorphism from $C$ to $C'$ in the category $\operatorname{\mathcal{C}}$. Replacing $v$ by the pair $(C, \mathscr {F}(f^{-1})(X) )$, we can reduce to the case where $C' = C$ and $f = \operatorname{id}_{C}$ so that $\widetilde{f}$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{E}}_{C}$. In this case, we can take $\widetilde{e}$ to be any composition of $\widetilde{f}$ with the morphism $\lambda (e, \operatorname{id}_ X ): \lambda (C, X) \rightarrow \lambda (D, \mathscr {F}(e)(X) )$ of $\operatorname{\mathcal{E}}$. This completes the proof that $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is an isofibration.

Using Corollary 5.3.4.18, we can choose a cocartesian fibration $U': \operatorname{\mathcal{E}}' \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}})$ and a scaffold $\lambda ': \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ) \rightarrow \operatorname{\mathcal{E}}'$. Then $U'$ is an isofibration, so composition with $\lambda $ induces a categorical equivalence $\operatorname{Fun}_{ / \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}) }( \operatorname{\mathcal{E}}, \operatorname{\mathcal{E}}' ) \rightarrow \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \underset { \longrightarrow }{\mathrm{holim}}( \mathscr {F} ), \operatorname{\mathcal{E}}' )$ (Corollary 4.5.2.34). It follows that there exists a functor $F: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$ satisfying $U' \circ F = U$ such that $F \circ \lambda $ is isomorphic to $\lambda '$ 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 '$ is a categorical equivalence of simplicial sets, the morphism $F \circ \lambda $ is also a categorical equivalence of simplicial sets (Corollary 4.5.3.9). Applying the two-out-of-three property (Remark 4.5.3.5), we deduce that $F$ is an equivalence of $\infty $-categories. It follows that $U$ is also a cocartesian fibration (Corollary 5.1.6.2) and that $\lambda $ is a scaffold of $U$ (Remark 5.3.4.6). $\square$

Proof. Using Corollary 5.3.2.23, we can identify $\theta $ with the functor

given by precomposition with the universal scaffold $\lambda _{u}$. The desired result now follows by combining Corollaries 5.3.5.8 and 4.5.2.34. $\square$

Proof. By virtue of Remark 5.3.4.10, we have a pullback diagram of $\infty $-categories

where the vertical maps are inclusions of replete full subcategories (and are therefore isofibrations; see Example 4.4.1.12). Since the bottom horizontal map is an equivalence of $\infty $-categories (Corollary 5.3.5.11), it follows that the upper horizontal map is also an equivalence of $\infty $-categories (Corollary 4.5.2.29). $\square$