Covering spaces are stable under restriction, finite products, and pullback

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

For a covering $p:E\to B$ and a continuous map $f:X\to B$, define $f^{\ast }E:=\{(x,e)\in X\times E:f(x)=p(e)\}$ with the subspace topology, and let $f^{\ast }p:f^{\ast }E\to X$ be $(x,e)\mapsto x$ (def-product-topology, def-subspace-topology-top). This is the pullback covering space; its covering property is proved in prop-covering-spaces-are-stable-under-restriction-finite-products-and-pullback. (The pullback of a covering space along a continuous map).

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).

The product set. Let $I$ be a set and let $X_i$ be a set for each $i\in I$. The product is ${\prod }_{i\in I}{X}_i:=\{x:x\text{ is a function with domain }I\text{ and }x(i)\in X_i\text{ for every }i\in I\},$ and we write $x_i:=x(i)$, the $i$-th coordinate of $x$. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For $j\in I$ the $j$-th projection is ${\pi }_j:{\prod }_{i\in I}{X}_i\to X_j,{\pi }_j(x):=x_j\mathrm{.}$. The product topology ${\mathcal{T}}^{\mathrm{\Pi }}$ on ${\prod }_i{X}_i$ is the initial topology of the projections: the topology generated by the subbasis $\{{\pi }_i^{-1}[U]:i\in I,U\in {\mathcal{T}}_i\}$. Finite intersections of subbasic sets form a basis for it, and they are exactly the boxes ${\prod }_{i\in I}{U}_i$ with every $U_i$ open in $X_i$ and $U_i=X_i$ for all but finitely many $i$. (The product set ${\prod }_{i\in I}{X}_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space) and let $S\subseteq X$. The subspace topology (also relative topology) on $S$ is ${\mathcal{T}}_S:=\{U\cap S:U\in \mathcal{T}\},$ the family of traces on $S$ of the open sets of $X$. The pair $(S,{\mathcal{T}}_S)$ is a subspace of $X$. A subset of $S$ that lies in ${\mathcal{T}}_S$ is said to be open in $S$, and relatively open where the ambient space needs emphasis. (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).