Kerodon

Proof. Let $S$ denote the collection of all morphisms of simplicial sets $i: A \rightarrow B$ with the following property: for every morphism of simplicial sets $B \rightarrow \operatorname{\mathcal{C}}$, if the restriction $\widetilde{\mathscr {F}}|_{ A \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}}$ witnesses $\mathscr {F}|_{ A }$ as a covariant transport representation for the projection map $A \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow A$, then $\widetilde{\mathscr {F}}|_{ B \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}}$ witnesses $\mathscr {F}|_{ B }$ as a covariant transport representation for the projection map $B \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow B$. To prove Lemma 5.6.8.5, it will suffice to show that every inner anodyne morphism of simplicial sets belongs to $S$. It is not difficult to see that the collection of morphisms $S$ is weakly saturated, in the sense of Definition 1.5.4.12. It will therefore suffice to show that, for every pair of integers $0 < i < n$, the inner horn inclusion $\Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ belongs to $S$. We may therefore assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ and $\operatorname{\mathcal{C}}_0 = \Lambda ^{n}_{i}$ is an inner horn.

Since every vertex of $\Delta ^ n$ is contained in $\Lambda ^{n}_{i}$, it follows immediately that the pair $(\mathscr {F}, \widetilde{\mathscr {F}})$ satisfies condition $(a)$ of Remark 5.6.5.3. To verify $(b)$, let $e: X \rightarrow Z$ be an $U$-cocartesian edge of $\operatorname{\mathcal{E}}$ having image $\overline{e} = U(e)$ in $\Delta ^ n$; we wish to show that $\widetilde{\mathscr {F}}(e)$ is a $V$-cocartesian edge of $\operatorname{\mathcal{E}}'$. If $\overline{e}$ belongs to the horn $\Lambda ^ n_{i}$, then this follows from our assumption on $\widetilde{F}|_{ \operatorname{\mathcal{E}}_0 }$. We may therefore assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^{2}$ and that $\overline{e}: 0 \rightarrow 2$ is the “long” edge of the simplex $\Delta ^{2}$. Since $U$ is a cocartesian fibration, there exists a $U$-cocartesian edge $e': X \rightarrow Y$ of $\operatorname{\mathcal{E}}$, where $U(Y) = 1$. Our assumption that $e'$ is $U$-cocartesian guarantees the existence of a $2$-simplex

of $\operatorname{\mathcal{E}}$, and Proposition 5.1.4.13 implies that $e''$ is also $U$-cocartesian. Since $\widetilde{\mathscr {F}}|_{ \operatorname{\mathcal{C}}_0}$ carries $U_0$-cocartesian morphisms of $\operatorname{\mathcal{E}}_0$ to $V$-cocartesian morphisms of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$, it follows that $\widetilde{\mathscr {F}}(e')$ and $\widetilde{\mathscr {F}}(e'')$ are $V$-cocartesian edges of $\operatorname{\mathcal{E}}'$. Applying Proposition 5.1.4.13 again, we deduce that $\widetilde{\mathscr {F}}(e)$ is also $V$-cocartesian. $\square$

Proof. Since $V$ is an inner fibration, the induced map $V': \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} ) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}})$ is also an inner fibration (Corollary 4.1.4.3). The projection map $\operatorname{\mathcal{M}}\rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$ is a pullback of $V'$, and is therefore also an inner fibration. Since $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$ is an $\infty $-category (Theorem 1.5.3.7), assertion $(1)$ follows from Remark 4.1.1.9.

We now prove $(2)$. We first show that $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is a subcategory of $\operatorname{\mathcal{M}}$: that is, that the inclusion map $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}) \hookrightarrow \operatorname{\mathcal{M}}$ is an inner fibration. Fix integers $0 < i < n$ and let $\sigma $ be an $n$-simplex of $\operatorname{\mathcal{M}}$ for which the restriction $\sigma |_{ \Lambda ^{n}_{i} }$ belongs to $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$; we wish to show that $\sigma $ is an $n$-simplex of $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$. Unwinding the definitions, we can identify $\sigma $ with a commutative diagram

we wish to show that $\widetilde{\mathscr {F}}$ witnesses $\mathscr {F}$ as a covariant transport representation for the cocartesian fibration $\operatorname{id}_{\Delta ^{n}} \times U$. This follows from Lemma 5.6.8.5, since the inclusion $\Lambda ^{n}_{i} \times \operatorname{\mathcal{C}}\hookrightarrow \Delta ^{n} \times \operatorname{\mathcal{C}}$ is inner anodyne (Lemma 1.5.7.5).

We now complete the proof by showing that the subcategory $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}) \subseteq \operatorname{\mathcal{M}}$ is replete. Let $u$ be an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}$, which we identify with a commutative diagram

Set $\mathscr {F}_0 = \mathscr {F}|_{ \{ 0\} \times \operatorname{\mathcal{C}}}$ and $\widetilde{\mathscr {F}}_{0} = \widetilde{\mathscr {F}}|_{ \{ 0\} \times \operatorname{\mathcal{E}}}$, and suppose that the pair $(\mathscr {F}_0, \widetilde{\mathscr {F}}_0)$ is an object of the $\infty $-category $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ (that is, $\widetilde{\mathscr {F}}_0$ witnesses $\mathscr {F}_0$ as a covariant transport representation for $U$. We wish to show that $\widetilde{\mathscr {F}}$ witnesses $\mathscr {F}$ as a covariant transport representation for $( \operatorname{id}_{\Delta ^1} \times U): \Delta ^1 \times \operatorname{\mathcal{E}}\rightarrow \Delta ^1 \times \operatorname{\mathcal{C}}$.

We first verify condition $(b)$ of Remark 5.6.5.3. Let $e$ be an $(\operatorname{id}_{\Delta ^1} \times U)$-cocartesian edge of the simplicial set $\Delta ^1 \times \operatorname{\mathcal{E}}$; we wish to show that $\widetilde{\mathscr {F}}( e )$ is a $V$-cocartesian morphism of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$. Write $e = ( \varphi _{ij}, \overline{e})$, where $\varphi _{ij}: i \rightarrow j$ is an edge of $\Delta ^1$ and $\overline{e}: X \rightarrow Y$ is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$. We consider three cases:

$(1)$

Suppose that $i=j=0$. Then $\widetilde{\mathscr {F}}(e) = \widetilde{\mathscr {F}}_0( \overline{e} )$ is $V$-cocartesian by virtue of our assumption that $\widetilde{\mathscr {F}}_{0}$ witnesses $\mathscr {F}_0$ as a covariant transport representation for $U$.

$(2)$

Suppose that $i=0$ and $j=1$. In this case, there exists a $2$-simplex of $\Delta ^1 \times \operatorname{\mathcal{E}}$ whose boundary is indicated in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & (0,Y) \ar [dr]^{ ( \varphi _{01}, \operatorname{id}_ Y) } & \\ (0,X) \ar [ur]^{ (\varphi _{00}, \overline{e} )} \ar [rr]^-{ ( \varphi _{01}, \overline{e} ) } & & (1,Y). } \]

Our assumption that $u$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}$ guarantees that $\widetilde{\mathscr {F}}( \varphi _{01}, \operatorname{id}_ Y)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$, and is therefore $V$-cocartesian (Proposition 5.1.1.9). It follows from case $(1)$ that $\widetilde{\mathscr {F}}( \varphi _{00}, \overline{e} )$ is also a $V$-cocartesian morphism of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$. Since the collection of $V$-cocartesian morphisms of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ is closed under composition (Corollary 5.1.2.4), we conclude that $\widetilde{\mathscr {F}}( \varphi _{01}, \overline{e})$ is also $V$-cocartesian.

$(3)$

Suppose that $i=j=1$. In this case, there exists a $2$-simplex of $\Delta ^1 \times \operatorname{\mathcal{E}}$ whose boundary is indicated in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & (1,X) \ar [dr]^{ ( \varphi _{11}, \overline{e}) } & \\ (0,X) \ar [ur]^{ (\varphi _{01}, \operatorname{id}_{X} )} \ar [rr]^-{ ( \varphi _{01}, \overline{e} ) } & & (1,Y). } \]

Our assumption that $u$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}$ guarantees that $\widetilde{\mathscr {F}}( \varphi _{01}, \operatorname{id}_ X)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$, and is therefore $V$-cocartesian (Proposition 5.1.1.9). It follows from case $(2)$ that $\widetilde{\mathscr {F}}( \varphi _{01}, \overline{e} )$ is also a $V$-cocartesian morphism of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$, so that $\widetilde{\mathscr {F}}( \varphi _{11}, \overline{e} )$ is $V$-cocartesian by virtue of Corollary 5.1.2.4.

We now complete the proof by showing that the pair $( \widetilde{\mathscr {F}}, \mathscr {F})$ satisfies condition $(a)$ of Remark 5.6.5.3. Let $(i,C)$ be a vertex of the product $\Delta ^1 \times \operatorname{\mathcal{C}}$, so that $\widetilde{\mathscr {F}}$ restricts to a functor of $\infty $-categories

We wish to show that the functor $\widetilde{\mathscr {F}}_{(i,C)}$ is an equivalence of $\infty $-categories. If $i=0$, this follows from our assumption that $\widetilde{\mathscr {F}}_{0}$ witnesses $\mathscr {F}_0$ as a covariant transport representation for $U$. We may therefore assume without loss of generality that $i=1$. Set $v = \mathscr {F}( \varphi _{01}, \operatorname{id}_{C})$ and let

be the functor given by covariant transport along $v$. Since $u$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{M}}$, $v$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{QC}}$ so that $v_{!}$ is an equivalence of $\infty $-categories (Remark 5.2.5.5). Combining the first part of the proof with Remark 5.2.8.5, we deduce that the diagram of $\infty $-categories

commutes up to isomorphism (that is, it determines a commutative diagram in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$). Since $v_{!}$ and $\widetilde{\mathscr {F}}_{(0,C)}$ are equivalences of $\infty $-categories, it follows that $\widetilde{\mathscr {F}}_{(1,C)}$ is also an equivalence of $\infty $-categories. $\square$

Proof. Since $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is an $\infty $-category (Lemma 5.6.8.6), it will suffice to show that every morphism $u$ of $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is an isomorphism (Proposition 4.4.2.1). Let us identify $u$ with a commutative diagram of simplicial sets

satisfying conditions $(a)$ and $(b)$ of Remark 5.6.5.3.

Passing to homotopy categories, we see that $\mathscr {F}$ induces a functor $\mathrm{h} \mathit{\mathscr {F}}: [1] \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{\mathcal{QC}}} \simeq \mathrm{h} \mathit{\operatorname{QCat}}$. Applying Remark 5.6.5.10, we see that $\mathrm{h} \mathit{\mathscr {F}}$ is isomorphic to the composite functor $[1] \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \twoheadrightarrow \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \xrightarrow { \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } \mathrm{h} \mathit{\operatorname{QCat}}$, where $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ denotes the homotopy transport representation of Construction 5.2.5.2. It follows that, for every vertex $C \in \operatorname{\mathcal{C}}$, the morphism $\mathscr {F}$ carries the edge $\Delta ^1 \times \{ C\} $ to an isomorphism $\overline{e}$ in $\operatorname{\mathcal{QC}}$. If $X$ is an object of $\operatorname{\mathcal{E}}$ satisfying $U(X) = C$, then $\widetilde{\mathscr {F}}$ carries $\Delta ^1 \times \{ X\} $ to a $V$-cocartesian morphism $e$ of $\operatorname{\mathcal{QC}}_{\operatorname{Obj}}$ satisfying $V(e) = \overline{e}$, which is then also an isomorphism by virtue of Corollary 5.1.1.11. Allowing $C$ and $X$ to vary and applying Theorem 4.4.4.4, we deduce that $\mathscr {F}$ and $\widetilde{\mathscr {F}}$ are isomorphisms when regarded as morphisms in the $\infty $-categories $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}})$ and $\operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}} )$, respectively.

Set $\operatorname{\mathcal{M}}= \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}) } \operatorname{Fun}( \operatorname{\mathcal{E}}, \operatorname{\mathcal{QC}}_{\operatorname{Obj}})$. Applying Corollary 4.4.3.19 to the pullback diagram

we deduce that $u$ is an isomorphism when regarded as a morphism of the $\infty $-category $\operatorname{\mathcal{M}}$. Since $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ is replete subcategory of $\operatorname{\mathcal{M}}$ (Lemma 5.6.8.6), it follows that $u$ is also an isomorphism when regarded as a morphism of $\operatorname{TW}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}})$ (Example 4.4.2.9). $\square$

Proof. We first prove $(1)$. Since the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ is a Kan complex (Lemma 5.6.8.7), it will suffice to show that $\theta $ is an isofibration. Define fiber products

so that we have a commutative diagram

It follows from Lemma 5.6.8.6 that $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is a replete subcategory of $\operatorname{\mathcal{M}}$, and therefore also a replete subcategory of the fiber product $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 ) \times _{ \operatorname{\mathcal{M}}_0 } \operatorname{\mathcal{M}}$. It will therefore suffice to show that the projection map $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 ) \times _{ \operatorname{\mathcal{M}}_0 } \operatorname{\mathcal{M}}\rightarrow \operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ is an isofibration of $\infty $-categories. Since the collection of isofibrations is stable under pullback, we are reduced to showing that the map $\overline{\theta }: \operatorname{\mathcal{M}}\rightarrow \operatorname{\mathcal{M}}_0$ is an isofibration. We now observe that $\overline{\theta }$ factors as a composition

where $\overline{\theta }''$ is a pullback of the restriction map

Since the forgetful functor $V: \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \rightarrow \operatorname{\mathcal{QC}}$ is an isofibration, $\psi ''$ is also an isofibration (Propositions 4.4.5.1). Similarly, $\overline{\theta }'$ is a pullback of the restriction map $\psi ': \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{QC}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{C}}_0, \operatorname{\mathcal{QC}})$, which is an isofibration by virtue of Corollary 4.4.5.3. It follows that $\overline{\theta } = \overline{\theta }'' \circ \overline{\theta }'$ is also an isofibration. This completes the proof of $(1)$.

We now prove $(2)$. Suppose that the inclusion map $\operatorname{\mathcal{C}}_0 \hookrightarrow \operatorname{\mathcal{C}}$ is inner anodyne; we wish to show that $\theta $ is a trivial Kan fibration. Applying Proposition 1.5.7.6, we deduce that $\psi '$ is a trivial Kan fibration of simplicial sets. Since $U$ is a cocartesian fibration, the inclusion map $\operatorname{\mathcal{E}}_0 \hookrightarrow \operatorname{\mathcal{E}}$ is a categorical equivalence (Lemma 5.3.6.5). Applying Proposition 4.5.5.18, we deduce that $\psi ''$ is a trivial Kan fibration. It follows that the morphisms $\overline{\theta }'$ and $\overline{\theta }''$ are also trivial Kan fibrations, so that $\overline{\theta } = \overline{\theta }'' \circ \overline{\theta }'$ is a trivial Kan fibration. Applying Lemma 5.6.8.5, we see that the diagram (5.62) is a pullback square, so that $\theta $ is also a trivial Kan fibration. $\square$

Proof of Theorem 5.6.5.12 from Theorem 5.6.8.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small cocartesian fibration of simplicial. Let $\operatorname{\mathcal{C}}_0 \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset and set $\operatorname{\mathcal{E}}_0 = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$. Applying Theorem 5.6.8.3, we see that the simplicial sets $\operatorname{TW}(\operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ and $\operatorname{TW}( \operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ are contractible Kan complexes. It follows that the restriction map $\theta : \operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}}) \rightarrow \operatorname{TW}(\operatorname{\mathcal{E}}_0 / \operatorname{\mathcal{C}}_0 )$ is a homotopy equivalence. Since $\theta $ is also Kan fibration (Lemma 5.6.8.10), it is a trivial Kan fibration (Proposition 3.2.7.2). In particular, $\theta $ is surjective on vertices, which is a restatement of Theorem 5.6.5.12. $\square$