Associated coverings of a G-principal cover

Question

I'm reading through Tammo Tom Dieck's algebraic topology textbook, and at the end of 3.1 he defines the associated coverings of a right G-principal cover $p \colon E \to B$ ($G-$principal meaning that $p(xg) = p(x)$, the action of $G$ on $E$ is properly discontinuous, and the induced action on each fiber is transitive).

For any set $F$ with a left $G$-action, the associated cover with respect to $p$ is defined as the map $p_F \colon E \times_G F \to B$ sending $(x, f)$ to $p(x)$, where $E \times_G F = E \times F$ quotiented by the relation $(x, f) \sim (xg^{-1}, gf)$ for $x \in E, f \in F, g \in G$. $p_F$ has typical fiber $F$.

I would like to see a proof that $p_F$ is a covering space, and if possible an explanation for why $E \times_G F$ is used instead of $E \times G$. I recall that if $p$ is $G$-principal then the associated orbit space is homeomorphic to $B$, so intuitively it seems like we are trying to identify the sheets of a given open set $U$ in some way, so that a trivialization $\varphi \colon p^{-1}(U) \to U \times J$ is analogous to a trivialization $\psi \colon p_F^{-1}(U) \to U \times F$ i.e it is defined so that $F$ is the typical fiber of $p_F$. However I don't understand the details here, or how $E \times_G F$ relates to the orbit space of $E$ under $G$.

Edit: I should also mention that I saw earlier in the book that $G$-maps between spaces $F_1$ and $F_2$ give rises to maps $E \times_G F_1 \to E \times_G F_2$ which is necessary for this associated cover construction to give rise to a functor from G-SET to COV$_B$, but again I'm pretty hazy on the details and whether or not this wouldn't work with $E \times F_1 \to E \times F_2$.

Answer 1

For any point $b_0\in B$, let $U$ be an open set evenly covered by $p$, let $\tilde{U}$ be a sheet over $U$. We can assume that $\tilde{U}$ satisfies that for any $g\in G$, $\tilde{U}g\cap \tilde{U}=\emptyset$, or we can replace $\tilde{U}$ by a smaller open subset. Then $\tilde{U}g$ are all the sheets over $U$.

For every $b\in U$, let $e_b\in \tilde{U}$ such that $p(e_b)=b$. We define a map $\phi:p_F^{-1}(U)=p^{-1}(U)\times F/\sim \to U\times F:[(e_b,f)]\to (b,f)$, where $[\cdot]$ denotes the equivalence class under $\sim$.

First we should show this is well-defined. Since $G$ is transitive on every fibre of $p$, every equivalence class in $p^{-1}(U)\times F/\sim$ can be represented by some $(e_b,f)$. If $[(e_b,f)]=[(e_{b'},f')]$, we must have $e_b=e_{b'}$; thus $f=f'$, since $G$ is free. The bijection of $\phi$ and the commutativity of $\pi_U\circ \phi=p_F$ are easy to verify.

$p^{-1}(U)\times F\to p^{-1}(U)\times F/\sim$ is still a quotient map, since $E\times F\to E\times_G F$ is open (See Munkres Theorem 22.1(2)). Consider $p^{-1}(U)\times F\to p^{-1}(U)\times F/\sim\to U\times F$; for a fixed $f$ and a sheet $\tilde{U}g$, $(e_bg,f)\mapsto (b,g^{-1}f)$ under the map. Thus $\phi$ is continuous. Since both $E\times F\to B$ and $E\times F\to E\times_G F$ are open and the latter is surjective, $\phi$ is open. Hence $\phi$ is a homeomorphism.

Answer 2

Suppose that $\mathcal F$ is the typical fibre of $p$. $G$ is a free (and transitive) action on $\mathcal F$ as it's properly discontinuous (and transitive)

First we show the typical fibre of $p_F$ is $F$. It's immediate that the typical fibre is given by $\frac{\mathcal F\times F}{\sim}$ immediately showing discreteness. Next, notice that $\left\{\left(\mathfrak f,f\right)|f\in F\right\}$ are the representatives of $\frac{\mathcal F\times F}{\sim}$ for some arbitrary $\mathfrak f$ as supose $\mathfrak f'=\mathfrak fg$, then $\left(\mathfrak f',f\right)=\left(\mathfrak f,gf\right)$ and $\left(\mathfrak f,f\right)=\left(\mathfrak f,f'\right)$ implies that either $\mathfrak f$ has a nontrivial stabalizer or $f=f'$, hence we need to assume the action is free on $\mathcal F$.

Next we show that this is indeed a covering. Suppose $U$ has a trivialization, i.e. $p^{-1}(U)\cong U\times\mathcal F$. Then $\frac{p^{-1}(U)\times F}{\sim}\cong\frac{U\times\mathcal F\times F}{\sim}\cong U\times F$. Hence $p_F$ is a covering with typical fibre $F$.

We can set $F=G$ but then you no longer that the functor from $G$-Set to COV${}_B$