Definition 1

Let G be a topological group and B a topological space. A (right) principal fibre space with base B and group G is a B-space $(E, p)$ endowed with a right operation of G on E (A, I, p. 50) having the following property:

(FP) For every point $b$ of B, there exists a neighbourhood U of $b$ and a

U-isomorphism $f: U\times G\rightarrow \overset{-1}{p}(U)$ such that for all $u\in U$

and $g,g'\in G$, one has $f(u, gg') =f(u, g)\cdot g'$.

Instead of saying that $(E, p)$ is a principal fibre space with base B and group G, one sometimes says that the quadruple $(E,G,B, p)$ is a principal fibration (cf. VAR, R, § 6), or, by abuse, that the mapping $p: E\rightarrow B$ is a principal fibration with base B and group G.

When no doubt is possible as to the base B, the group G and the operation of G on E, we shall simply say that $(E, p)$ is a principal fibre space.

Let G be a topological group. Let $(E, p)$ be a B-space endowed with a left operation of G. If, for the right operation of the group $G^{\circ}$ opposite to the given operation (A, I, p. 50), $(E, p)$ is a right principal fibre space with group $G^{\circ}$, one says that $(E, p)$ is a left principal fibre space with group G.

A principal fibre space is a locally trivial fibre space (I, p. 68, def. 1).

It follows from property (FP) that the group G acts continuously (TG, III, p. 9) and freely on E, and that the orbits of this operation are the fibres of the B-space $(E, p)$. The mapping $p': E/G\rightarrow B$ deduced from $p$ is continuous and bijective. Again from property (FP), the mapping $p$ is open (TG, I, p. 30, prop. 2 and p. 26, prop. 5); hence $p'$ is a homeomorphism (TG, I, p. 32, prop. 3).

Let $(E, p)$ and $(E', p')$ be principal fibre spaces with base B and group G. A mapping $f: E\rightarrow E'$ is said to be a morphism of principal fibre spaces (with base B and group G) if $f$ is a B-morphism and if one has $f(x\cdot g) =f(x)\cdot g$ for every $x\in E$ and every $g\in G$. Let $(E'', p'')$ be a principal fibre space with base B and group G. If $f: E\rightarrow E'$ and $g: E'\rightarrow E''$ are morphisms of principal fibre spaces, the mapping $g\circ f: E\rightarrow E''$ is a morphism of principal fibre spaces. In accordance with the general definitions (E, IV, p. 11), one may take as morphisms of the structure of principal fibre space with base B and group G those defined above. We denote by $\mathscr{C}_B^G(E; E')$ the set of morphisms of principal fibre spaces from $(E, p)$ into $(E', p')$.

A trivial principal fibre space with base B and group G is the B-space $(B\times G$, pr$_1)$ endowed with the law of right operation of G on $B\times G$ defined by $(b, g)\cdot h= (b, gh)$.

A principal fibre space $(E, p)$ with base B and group G is said to be trivializable if there exists an isomorphism of $(E, p)$ onto the trivial principal fibre space $(B\times G$, pr$_1)$; such an isomorphism is called a trivialization of the principal fibre space $(E, p)$. Property (FP) expresses that there exists an open covering $(U_i)_{i\in I}$ of B such that, for every $i\in I$, the $U_i$-space $(\overset{-1}{p}(U_i), p|U_i)$, endowed with the right operation of G deduced from that of G on E, is a trivializable principal fibre space.