Kerodon

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

Proposition 5.6.1.5. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left covering map of simplicial sets, let $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \operatorname{Set}$ be the covariant transport representation of Construction 5.6.1.2, and let us abuse notation by identifying $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a morphism of simplicial sets from $\operatorname{\mathcal{C}}$ to $\operatorname{N}_{\bullet }(\operatorname{Set})$. Then there is a canonical isomorphism $\operatorname{\mathcal{E}}\simeq \int _{\operatorname{\mathcal{C}}} \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$.

Proof. Every vertex $X \in \operatorname{\mathcal{E}}$ can be regarded as an element of the set $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}( U(X) )$, and the construction $(X \in \operatorname{\mathcal{E}}) \mapsto ( \operatorname{\mathcal{E}}_{U(X)}, X)$ determines a functor $\widetilde{\operatorname{Tr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{E}}} \rightarrow \operatorname{Set}_{\ast }$. Let us identify $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a morphism of simplicial sets from $\operatorname{\mathcal{C}}$ to $\operatorname{N}_{\bullet }(\operatorname{Set})$ and $\widetilde{\operatorname{Tr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ with a morphism of simplicial sets from $\operatorname{\mathcal{E}}$ to $\operatorname{N}_{\bullet }(\operatorname{Set}_{\ast } )$, so that we have a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [d]^{U} \ar [r]^-{ \widetilde{\operatorname{Tr}}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } & \operatorname{N}_{\bullet }( \operatorname{Set}_{\ast } ) \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{ \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} } & \operatorname{N}_{\bullet }( \operatorname{Set}) }$

which we can identify with a morphism $V: \operatorname{\mathcal{E}}\rightarrow \int _{\operatorname{\mathcal{C}}} \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ in the category $(\operatorname{Set_{\Delta }})_{/\operatorname{\mathcal{C}}}$. We will complete the proof by showing that $V$ is an isomorphism. Since $U$ and the projection map $\int _{\operatorname{\mathcal{C}}} \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}} \rightarrow \operatorname{\mathcal{C}}$ are both left covering maps (see Example 5.5.4.8), it follows that $V$ is a left covering map. By construction, $V$ is bijective at the level of vertices, and is therefore an isomorphism of simplicial sets (Proposition 4.2.3.19). $\square$