For a nonempty path-connected locally path-connected semilocally simply connected space, the path-class projection is a covering map

Given: The objects, hypotheses, and choice principles stated above.

Fix a path-connected space $X$ and $x_0\in X$. Let $\tilde{X}$ be the set of endpoint-fixed homotopy classes $[\alpha ]$ of paths beginning at $x_0$, and put $p([\alpha ])=\alpha (1)$. If $U$ is an open path-connected neighbourhood of $\alpha (1)$ on which the inclusion-induced fundamental-group map is trivial, define $B([\alpha ],U)$ to consist of the classes $[\alpha \ast \gamma ]$ with $\gamma$ a path in $U$ beginning at $\alpha (1)$. These sets are the proposed basic neighbourhoods for the path-class model (def-homotopy-relative-and-path-homotopy, def-semilocally-simply-connected-space, def-path-connected). (The based path-class model and basic sets for a universal cover).

A covering map is a continuous surjection $p:E\to B$ such that every $b\in B$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets $V_j$, called sheets, and each restriction $p{\mathrm{\mid }}_{V_j}:V_j\to U$ is a homeomorphism (def-continuous-map-top, def-homeomorphism-and-open-maps, def-disjoint-union-topology). Such a $U$ is evenly covered, and $p^{-1}(b)$ is the fibre over $b$. A covering is trivial when it is isomorphic over $B$ to a product projection $B\times F\to B$ with $F$ discrete. (Covering maps, evenly covered neighbourhoods, fibres, sheets, and trivial coverings).

A space $X$ is semilocally simply connected at $x\in X$ when there is a neighbourhood $U$ of $x$ and a basepoint-preserving inclusion $(U,x)\hookrightarrow (X,x)$ whose induced map on fundamental groups is trivial (def-neighbourhood-top, def-induced-homomorphism-on-fundamental-groups, def-based-loops-and-fundamental-group). It is semilocally simply connected when this holds at every point. The neighbourhood need not itself be simply connected. (Semilocally simply connected spaces with explicit basepoint convention).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space) and let $x\in X$. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. $X$ is locally connected at $x$ when for every open $U$ with $x\in U$ there is an open connected $V$ with $x\in V\subseteq U$, and locally connected when this holds at every point; $X$ is locally path-connected at $x$ when for every open $U$ with $x\in U$ there is an open path-connected $V$ with $x\in V\subseteq U$, and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).