Proposition 7

Let B be a topological space, let G be a topological group, let $(E, p)$ be a principal fibred space over B with group G and let F be a topological space in which the group G operates continuously on the left.

a) The topological space $E\times^GF$ endowed with the continuous mapping $p^F: E\times^GF\rightarrow B$ deduced from the mapping $p\circ$pr$_1: E\times F\rightarrow B$ by passing to the quotient is a locally trivial fibred space over B of fibre type F; it is trivializable if the fibred space over B E is trivializable.

b) Let $\pi : E\times F\rightarrow E\times^GF$ be the canonical surjection. The mapping $\mu: E\times F\rightarrow E\times_B(E\times^GF)$ which associates to $(x, f)$ the element $(x, \pi (x, f))$ is a homeomorphism whose inverse mapping is a trivialization of the locally trivial fibred space over E $(E\times_B(E\times^GF)$, pr$_1)$.

Suppose first that E is the trivial principal fibred space over B $B\times G$. By example 2, the space $E\times^GF$ is then identified with $B\times F$ and the mapping $p^F$ with the first projection pr$_1: B\times F\rightarrow B$, which proves that $(E\times^GF, p^F)$ is a trivializable fibred space over B in this case. In the general case, every point of B possesses a neighbourhood U such that the mapping $p_U:\overset{-1}{p}(U)\rightarrow U$ makes $\overset{-1}{p}(U)$ into a trivializable principal fibred space over U. From what precedes, $(\overset{-1}{p}(U)\times^GF\rightarrow U,(p_U)^F)$ is a trivializable fibred space over U. By the above lemma, applied to the case where $B'= U$ and $h: U\rightarrow B$ is the canonical injection, the same is

true of the fibred space over U ($(p^{-F1})(U),(p^F)_U$) deduced from $(E\times^GF, p^F)$ by restriction above U. This proves that $(E\times^GF, p^F)$ is a locally trivial fibred space over B and concludes the proof of assertion a).

The mapping $\theta : E\times G\rightarrow E\times_BE$ defined by $\theta (x, g) = (x, x\cdot g)$ is a homeomorphism (I, p. 94, prop. 3) compatible with the operations of G on $E\times G$ and on $E\times_BE$ given by $((x, g), g')\mapsto (x, gg')$ and $((x, y), g')\mapsto (x, yg')$ respectively. By passing to quotients, $\theta$ therefore induces a homeomorphism $\theta '$ of $(E\times G)\times^GF$ onto $(E\times_B$ $E)\times^GF$. The mapping $\mu$ is the composite of the homeomorphism $E\times F\rightarrow$ $(E\times G)\times^GF$ (example 2), of $\theta '$, and of the canonical homeomorphism $(E\times_BE)\times^GF\rightarrow E\times_B(E\times^GF)$ (I, p. 105, lemma), whence b).

Under the hypotheses of proposition 7, the locally trivial fibred B-space ($E\times^GF, p^F$) is called the locally trivial fibred space of fibre type F associated with the principal fibred space $(E, p)$. All the fibres of the B-space $E\times^GF$ are homeomorphic to the space F. In particular, if the space F is discrete, the mapping $p^F$ is a covering.