Corollary

Let G be a topological group, $(E, p)$ and $(E', p')$ principal fibre spaces of group G and with bases B and $B'$ respectively. Let $f: B'\rightarrow$ B and $f': E'\rightarrow$ E be continuous mappings such that $p\circ f'=f\circ p'$ and such that, for every $x'\in E'$ and every $g\in G$, $f'(x'\cdot g) =f'(x')\cdot g$. Then the square

${E'}^{f'}$ E

$p'p$

${B'}^f$ B

is a cartesian square.

In fact, the mapping $h: E'\rightarrow B'\times_BE$ defined by $h(x') =$ $(p'(x'), f'(x'))$ for $x'\in E'$, is a $B'$-morphism of principal coverings, hence an isomorphism; moreover pr$_2\circ h=f'$, whence the result (I, p. 8, Prop. 2).

Under the hypotheses of the preceding corollary, one sometimes says that $f'$ is an $f$-morphism of principal fibre spaces.