# Kerodon

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

Lemma 5.7.8.6. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets. Then:

$(1)$

The fiber product $\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}} )$ is an $\infty$-category.

$(2)$

The simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is a replete subcategory of $\operatorname{\mathcal{M}}$ (see Example 4.4.1.11).

In particular, the simplicial set $\operatorname{TW}( \operatorname{\mathcal{E}}/ \operatorname{\mathcal{C}})$ is an $\infty$-category.

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.4.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

$\xymatrix@R =50pt@C=50pt{ \Delta ^ n \times \operatorname{\mathcal{E}}\ar [r]^-{ \widetilde{\mathscr {F}} } \ar [d]^{ \operatorname{id}_{\Delta ^ n} \times U} & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \Delta ^ n \times \operatorname{\mathcal{C}}\ar [r]^-{\mathscr {F}} & \operatorname{\mathcal{QC}}; }$

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.7.8.5, since the inclusion $\Lambda ^{n}_{i} \times \operatorname{\mathcal{C}}\hookrightarrow \Delta ^{n} \times \operatorname{\mathcal{C}}$ is inner anodyne (Lemma 1.4.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

$\xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{\mathcal{E}}\ar [r]^-{ \widetilde{\mathscr {F}} } \ar [d]^{ \operatorname{id}_{\Delta ^1} \times U} & \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{V} \\ \Delta ^1 \times \operatorname{\mathcal{C}}\ar [r]^-{\mathscr {F}} & \operatorname{\mathcal{QC}}. }$

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.7.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.8). 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.8). 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.7.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

$\widetilde{\mathscr {F}}_{(i,C)}: \{ i \} \times \operatorname{\mathcal{E}}_{C} \rightarrow \{ \mathscr {F}(i,C) \} \times _{\operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}}.$

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

$v_{!}: \{ \mathscr {F}( 0, C) \} \times _{ \operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \rightarrow \{ \mathscr {F}(1,C) \} \times _{\operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}}$

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

$\xymatrix@R =50pt@C=50pt{ \{ 0\} \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ \widetilde{\mathscr {F}}_{(0,C)} } \ar [d]^{\sim } & \{ \mathscr {F}( 0, C) \} \times _{ \operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}} \ar [d]^{ v_{!} } \\ \{ 1\} \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ \widetilde{\mathscr {F}}_{(1,C)}} & \{ \mathscr {F}( 1, C) \} \times _{ \operatorname{\mathcal{QC}}} \operatorname{\mathcal{QC}}_{\operatorname{Obj}} }$

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$