Kerodon

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

5.2.3 Transitivity of Covariant Transport

We now study the behavior of the transport functors of §5.2.2 with respect to composition.

Proposition 5.2.3.1 (Transitivity). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $\sigma$ be a $2$-simplex of $\operatorname{\mathcal{C}}$, which we display as a diagram

$\xymatrix@R =50pt@C=50pt{ & D \ar [dr]^{g} & \\ C \ar [ur]^{f} \ar [rr]^{h} & & E. }$

Let $f_!: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ and $g_!: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{E}$ be functors which are given by covariant transport along $f$ and $g$, respectively. Then the composite functor $(g_{!} \circ f_{!}): \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{E}$ is given by covariant transport along $w$.

Proof. Without loss of generality, we may replace $U$ by the projection map $\Delta ^{2} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^2$, and thereby reduce to the case where $\operatorname{\mathcal{C}}= \Delta ^2$ and $\sigma$ is the unique nondegenerate $2$-simplex of $\operatorname{\mathcal{C}}$. In this case, $\operatorname{\mathcal{E}}$ is an $\infty$-category. Let $u: \operatorname{id}_{ \operatorname{\mathcal{E}}_{C} } \rightarrow f_{!}$ be a morphism in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ which witnesses $f_{!}$ as given by covariant transport along $f$, and let $v: \operatorname{id}_{ \operatorname{\mathcal{E}}_{D} } \rightarrow g_{!}$ be a morphism in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}})$ which witnesses $g_{!}$ as given by covariant transport along $g$. Let $v': f_{!} \rightarrow g_{!} \circ f_{!}$ denote the image of $v$ under the functor $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$ given by precomposition with $f_!$. Let $w: \operatorname{id}_{\operatorname{\mathcal{E}}_{C}} \rightarrow g_{!} \circ f_{!}$ be a composition of $u$ with $v'$ in the $\infty$-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}})$. We will complete the proof by showing that $w$ witnesses $g_{!} \circ f_{!}$ as given by covariant transport along $h$. To prove this, we must show that for every object $X \in \operatorname{\mathcal{E}}_{C}$, the the image $w_{X}: X \rightarrow ( g_{!} \circ f_{!})(X)$ is $U$-cocartesian. This follows from Corollary 5.1.2.4, since $w_{X}$ is a composition of the $U$-cocartesian morphisms $u_{X}: X \rightarrow f_{!}(X)$ and $v_{ f_{!}(X)}: f_{!}(X) \rightarrow (g_{!} \circ f_{!})(X)$. $\square$

Construction 5.2.3.2 (The Homotopy Transport Representation: Covariant Case). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets and let $\mathrm{h} \mathit{\operatorname{QCat}}$ denote the homotopy category of $\infty$-categories. It follows from Proposition 5.2.3.1 and Example 5.2.2.2 that there is a unique functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ with the following properties:

• For each vertex $C$ of the simplicial set $\operatorname{\mathcal{C}}$, $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is the $\infty$-category $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ (regarded as an object of $\mathrm{h} \mathit{\operatorname{QCat}}$).

• For each edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$ representing a morphism $[f] \in \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(C,D)$, we have $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( [f] ) = [ f_{!} ]$. Here $[f_{!}]$ denotes the isomorphism class of the covariant transport functor of Notation 5.2.2.5, which we regarded as an element of the set

$\operatorname{Hom}_{ \mathrm{h} \mathit{\operatorname{QCat}} }( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} ) = \pi _0( \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D})^{\simeq } ).$

We will refer to $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ as the homotopy transport representation of the cocartesian fibration $U$.

Remark 5.2.3.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, and let $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ be the homotopy transport representation of Construction 5.2.3.2. It follows from Proposition 5.1.4.14 that $U$ is a left fibration if and only if the functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ factors through the full subcategory $\mathrm{h} \mathit{\operatorname{Kan}} \subseteq \mathrm{h} \mathit{\operatorname{QCat}}$. In particular, if $U$ is a left fibration, then Construction 5.2.3.2 determines a functor $\mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ which we will also refer to as the homotopy transport representation of the left fibration $U$.

Remark 5.2.3.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty$-categories, let $f: C \rightarrow D$ be a morphism of $\operatorname{\mathcal{C}}$, and let $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ be given by covariant transport along $f$. If $f$ is an isomorphism in the $\infty$-category $\operatorname{\mathcal{C}}$, then $f_{!}$ is an equivalence of $\infty$-categories. This follows from the observation that the homotopy transport functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ carries isomorphisms to isomorphisms.

Construction 5.2.3.2 has an analogue for cartesian fibrations:

Construction 5.2.3.5 (The Homotopy Transport Representation: Contravariant Case). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets and let $\mathrm{h} \mathit{\operatorname{QCat}}$ denote the homotopy category of $\infty$-categories (Construction 4.5.1.1). It follows from Proposition 5.2.3.1 and Example 5.2.2.2 that there is a unique functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ satisfying the following conditions:

• For each vertex $C$ of the simplicial set $\operatorname{\mathcal{C}}$, $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is the $\infty$-category $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ (regarded as an object of $\mathrm{h} \mathit{\operatorname{QCat}}$).

• For each edge $f: C \rightarrow D$ of the simplicial set $\operatorname{\mathcal{C}}$ representing a morphism $[f] \in \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(C,D)$, we have $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( [f] ) = [ f^{\ast } ]$, where $[f^{\ast }]$ denotes the isomorphism class of the contravariant transport functor of Notation 5.2.2.13.

We will refer to $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ as the homotopy transport representation of the cartesian fibration $U$.

Warning 5.2.3.6. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets which is both a cartesian fibration and a cocartesian fibration. Then Constructions 5.2.3.2 and 5.2.3.5 supply functors $\mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ and $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ respectively, which are both referred to as the homotopy transport representation of $U$ and both denoted by $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$. We will see later that these two functors are interchangeable data: either can be recovered from the other (see Proposition 6.2.3.5).

Example 5.2.3.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a morphism of simplicial sets. Combining Remark 5.2.3.3 with Theorem 5.2.2.15, we deduce that the following conditions are equivalent:

• The morphism $U$ is a Kan fibration.

• The morphism $U$ is a cocartesian fibration and the homotopy transport representation $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ of Construction 5.2.3.2 factors through the subcategory $\mathrm{h} \mathit{\operatorname{Kan}}^{\simeq } \subseteq \mathrm{h} \mathit{\operatorname{QCat}}$.

• The morphism $U$ is a cartesian fibration and the homotopy transport representation $\operatorname{hTr}'_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ of Construction 5.2.3.5 factors through the subcategory $\mathrm{h} \mathit{\operatorname{Kan}}^{\simeq } \subseteq \mathrm{h} \mathit{\operatorname{QCat}}$.

If these conditions are satisfied, then $\operatorname{hTr}'_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ is given by the composition

$\mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \xrightarrow { \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}^{\operatorname{op}} } ( \mathrm{h} \mathit{\operatorname{Kan}}^{\simeq } )^{\operatorname{op}} \xrightarrow {\iota } \mathrm{h} \mathit{\operatorname{Kan}}^{\simeq },$

where $\iota$ is the isomorphism which carries each morphism in $\mathrm{h} \mathit{\operatorname{Kan}}^{\simeq }$ to its inverse.