# Kerodon

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

Corollary 4.2.3.20. Let $f: X \rightarrow S$ be a morphism of simplicial sets. The following conditions are equivalent:

$(1)$

The morphism $f$ is a covering map.

$(2)$

The morphism $f$ is a left covering map and a Kan fibration.

$(3)$

The morphism $f$ is a right covering map and a Kan fibration.

Proof. The implication $(1) \Rightarrow (2)$ follows from Remarks 4.2.3.10 and 3.1.4.3. We will prove that $(2) \Rightarrow (1)$ (the equivalence of $(1)$ and $(3)$ follows by a similar argument). Assume that $f$ is a left covering map and a Kan fibration; we wish to show that $f$ is a covering map. By virtue of Remark 3.1.4.3, it will suffice to show that the relative diagonal $\delta : X \rightarrow X \times _{S} X$ is a Kan fibration. Note that $\delta$ is a left fibration (Remark 4.2.3.11) and therefore a left covering map (Example 4.2.3.12). Let $D \subseteq X \times _{S} X$ denote the smallest summand which contains the image of $\delta$. We will complete the proof by showing that $\delta$ induces an isomorphism from $X$ to $D$ (see Corollary 3.1.4.14). By virtue of Proposition 4.2.3.19, it will suffice to show that the map $\delta : X \rightarrow D$ is bijective on vertices. Equivalently, we must show that if $(e,e'): (x,x') \rightarrow (y,y')$ is any edge of the simpicial $X \times _{S} X$, then $x=x'$ if and only if $y = y'$. If $x = x'$, then our assumption that $f$ is a covering map immediately guarantees that $e = e'$, so that $y = y'$. For the converse, suppose that $y = y'$, and set $s = f(x) = f(x')$. Invoking our assumption that $f$ is a Kan fibration, we conclude that there exists a $2$-simplex $\sigma : \Delta ^2 \rightarrow X$ whose boundary is indicated in the diagram

$\xymatrix { & x' \ar [dr]^{ e'} & \\ x \ar [ur]^{u} \ar [rr]^{e} & & y, }$

where $f(u) = \operatorname{id}_{s}$. Since $f$ is a left covering map, the fiber $X_{s} = \{ s\} \times _{S} X$ is discrete (Remark 4.2.3.17). It follows that $u$ is a degenerate $1$-simplex of $X$, so that $x = x'$ as desired. $\square$