Kerodon

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

Proposition 5.2.0.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left covering map of simplicial sets. Then there is a unique functor

\[ \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \operatorname{Set} \]

with the following properties:

  • For each vertex $C \in \operatorname{\mathcal{C}}$, we have $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C) = \operatorname{\mathcal{E}}_{C}$.

  • Let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$, and let $[f]$ denote the corresponding morphism in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$. Then $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( [f] )$ is the covariant transport function $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ of Construction 5.2.0.1.

Proof. By virtue of Example 5.2.0.2 (and the proof of Proposition 1.2.5.4), it will suffice to show that if $\sigma $ is a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ as indicated in the diagram

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

then the covariant transport function $h_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{E}$ is equal to the composition $g_{!} \circ f_{!}$. Fix a vertex $X \in \operatorname{\mathcal{E}}_{C}$. By construction, there is an edge $\widetilde{f}: X \rightarrow e_{!}(X)$ satisfying $U( \widetilde{e} ) = e$ and an edge $\widetilde{h}: X \rightarrow g_{!}(X)$ satisfying $U( \widetilde{h} ) = h$. Since $U$ is a left covering map, we can lift $\sigma $ (uniquely) to a $2$-simplex of $\operatorname{\mathcal{E}}$ with boundary indicated in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & f_{!}(X) \ar [dr]^{\widetilde{g}} & \\ X \ar [ur]^{\widetilde{f}} \ar [rr]^-{\widetilde{h}} & & h_{!}(X). } \]

The edge $\widetilde{g}$ then satisfies $U( \widetilde{g} ) = g$, and therefore witnesses the identity $g_{!}( f_{!}(X) ) = h_{!}(X)$. $\square$