Let $f: B\times G\rightarrow B\times G$ be a morphism of the trivial principal fibre space $(B\times G$, pr$_1)$ into itself and let $\varphi : B\times G\rightarrow G$ be the continuous mapping pr$_2\circ f$, so that $f(b, g) = (b, \varphi (b, g))$. For every $b\in B$ and all $g,h\in G$, one has $\varphi (b, gh) =\varphi (b, g)\cdot h$, whence $\varphi (b, g) =\varphi (b, e)\cdot g$, where $e$ denotes the identity element of G. The morphism $f$ is therefore an isomorphism whose inverse morphism $f^{-1}$ is defined by $f^{-1}(b, g) =$ $(b, \varphi (b, e)^{-1}g)$ for $(b, g)\in B\times G$.

Now let E and $E'$ be principal fibre spaces and let $f: E\rightarrow E'$ be a morphism of principal fibre spaces. In view of property (FP), for every point $b\in B$, there exists an open neighbourhood U of $b$ such that the principal fibre spaces $E_U$ and $E'_U$ are trivializable. By passing to subspaces, $f$ induces a morphism $f_U: E_U\rightarrow E'_U$ of principal fibre spaces; by what precedes, this morphism $f_U$ is an isomorphism. In particular, $f_b: E_b\rightarrow E'_b$ is a bijection. There then exists a unique mapping $g: E'\rightarrow E$ which induces the bijection $f_b^{-1}$ by passing to subspaces. By Proposition 4 of I, p. 19, the mapping $g$ is continuous, hence $f$ is an isomorphism of principal fibre spaces.

${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.

(i) Endowed with the mapping $p$, E is a principal fibre space with base B and group G;

(ii) For every $x\in E$ and every $g\in G$, one has $p(x\cdot g) =p(x)$, the mapping $\theta : (x, g)\mapsto (x, x\cdot g)$ is a homeomorphism of $E\times G$ onto $E\times_BE$ and every point of B possesses a neighbourhood over which there exists a continuous section of the mapping $p$.

(i)$\Rightarrow$(ii) : Suppose that $(E, p)$ is a principal fibre space. The group G operates continuously and freely in E, with the fibres of $p$ as orbits. Hence the mapping $\theta$ is bijective and continuous. More precisely, if $E\times_BE$ is endowed with the operation of G defined by $(x, y)\cdot g= (x, y\cdot g)$, the mapping $\theta$ is an E-morphism of the trivial principal fibre space $E\times G$ into the principal fibre space $(E\times_BE\rightarrow E$, pr$_1)$ (example 5), hence an isomorphism (prop. 1). The other assertions of (ii) result immediately from the definition.

(ii)$\Rightarrow$(i) : Put $\varphi =$ pr$_2\circ \theta^{-1}$, so that, for every $(x, y)\in$ $E\times_BE$, one has

The mapping $\varphi : E\times_BE\rightarrow G$ is continuous and, for $(x, y)\in E\times_BE$, the element $\varphi (x, y)$ is the unique element $g$ of G such that $y=x\cdot g$. Let $b$ be a point of B; let U be a neighbourhood of $b$ and let $s$ be a continuous section of $p$ over U. For $(u, g)\in U\times G$, put $f(u, g) =s(u)\cdot$ $g$; the mapping $f$ is a U-morphism of $U\times G$ into $\overset{-1}{p}(U)$. For $y\in \overset{-1}{p}(U)$, put $f'(y) = (p(y), \varphi (s(p(y)), y))$. The mapping $f'$ is a U-morphism of $\overset{-1}{p}(U)$ into $U\times G$. One has

On the other hand, for $(u, g)\in U\times G$, one has

Hence $f$ is a U-isomorphism. It follows that $(E, p)$ is a principal fibre space with base B and group G.

(i) The orbit space $E/G$ is Hausdorff and the space E, endowed with the canonical mapping $p: E\rightarrow E/G$, is a principal fibre space with group G;

(ii) The group G operates properly (TG, III, p. 27) and freely in E, and every point of $E/G$ possesses a neighbourhood over which there exists a continuous section of the mapping $p$.

Put $B = E/G$. Under each of the hypotheses (i) and (ii), the group G operates continuously and freely in E, so that the mapping $\theta : (x, g)\mapsto (x, x\cdot g)$ is a continuous bijection of $E\times G$ onto $E\times_BE$. Let us place ourselves under this hypothesis and denote by $\varphi : E\times_BE\rightarrow G$ the mapping pr$_2\circ \theta^{-1}$. Having regard to formula (1), in order that $\theta$ be a homeomorphism, it is necessary and sufficient that the mapping $\varphi$ be continuous. On the other hand, since the equivalence relation defined by G is open (TG, III, p. 10, lemma 2), in order that the space $E/G$ be Hausdorff, it is necessary and sufficient that the graph $E\times_BE$ of this equivalence relation be closed in $E\times E$ (TG, I, p. 55, prop. 8). Finally (TG, III, p. 31, prop. 6), in order that G operate properly in E, it is necessary and sufficient that $E\times_BE$ be closed in $E\times E$ and that the mapping $\varphi$ be continuous. The equivalence of conditions (i) and (ii) then follows from prop. 3.

By left translations, every point of $G/H$ possesses a neighbourhood over which the mapping $p$ possesses a continuous section. On the other hand, for $(g, g')$ belonging to $G\times G$, put $\varphi (g, g') =$ $g^{-1}g'$. If $p(g) =p(g'),\varphi (g, g')$ belongs to H. The mapping $(g, g')\mapsto$ $(g, \varphi (g, g'))$ of $G\times_{G/H}G$ into $G\times H$ is continuous and is the inverse of the continuous mapping $\theta : G\times H\rightarrow G\times_{G/H}G$ defined by $\theta (g, h) = (g, gh)$, whence the corollary.

(i) The B-space E is a principal covering with group G;

(ii) For every $g\in G$ and every $x\in E$, one has $p(x\cdot g) =p(x)$, the mapping $p$ induces a homeomorphism of $E/G$ onto B, and the mapping $\theta : (x, g)\mapsto (x, x\cdot g)$ is a homeomorphism of $E\times G$ onto $E\times_BE$;

(iii) The group G operates continuously and freely in E, the mapping $p$ is etale, and its fibres are the orbits of G.

(i)$\Rightarrow$(ii) : This follows from I, p. 91 and from proposition 3 of I, p. 94.

(ii)$\Rightarrow$(iii): Under assumption (ii), the action law of G is continuous, and the mapping $p$ is surjective and open (TG, III, p. 10, lemma 2). Let $x\in E$; the mapping $\theta$ induces a bijection of $\{x\} \times G$ onto $\{x\} \times$ $\overset{-1}{p}(p(x))$, hence the group G operates freely and its orbits are the fibres of $p$. If $e$ denotes the identity element of G, the diagonal of $E\times_BE$ is the image of $E\times \{e\}$ under the homeomorphism $\theta$. Since the group G is discrete, the set $\{e\}$ is open in G, therefore the diagonal $\Delta_E$ is open in $E\times_BE$. By proposition 7 of I, p. 31, the mapping $p$ is étale.

(iii)$\Rightarrow$(i): Every fibre of $p$ being an orbit of the operation of G in E, the mapping $p$ is surjective. Since the mapping $p$ is étale, for every point $b$ of B, there exists an open neighbourhood U of $b$ and a continuous section $s$ of $p$ over U. The set $s(U)$ is open in E and $s$ induces a homeomorphism of U onto $s(U)$ (I, p. 30, cor. 3). For every $g\in G$, the set $s(U)\cdot g$ is open in E and the union of the sets $s(U)\cdot g$, for all $g\in G$, is equal to $\overset{-1}{p}(U)$. If $g$ and $g'$ are two distinct elements of G, the sets $s(U)\cdot g$ and $s(U)\cdot g'$ are disjoint, since G operates freely in E. The mapping $f: U\times G\rightarrow$ $\overset{-1}{p}(U)$ defined by $f(u, g) =s(u)\cdot g$ for $(u, g)\in U\times G$ is therefore a homeomorphism of $U\times G$ onto $\overset{-1}{p}(U)$, compatible with the right operations of G. By definition, E is therefore a principal covering of B with group G.

The operation of G in E is free by assumption, so it is enough to prove that the mapping $p$ is étale (I, p. 98, example 1). Let $x$ be a point of E and let U be an open neighbourhood of $x$ such that $U\cap U\cdot g=\emptyset$ for every element $g$ of G distinct from the identity element. The mapping $p$ is open (TG, III, p. 10, lemma 2) and induces an injective, continuous and open mapping of U onto $p(U)$, hence a homeomorphism, which proves that the mapping $p$ is étale.

(i) The group G operates properly and freely in E;

(ii) The space $E/G$ is separated and the space E is a principal covering with base $E/G$ and group G.

Moreover, under these conditions, the space E is separated.

Suppose condition (i) satisfied. Then the spaces E and $E/G$ are separated (TG, III, p. 29, prop. 3) and for every $x\in E$ there exists an open neighbourhood U of $x$ in E such that $U\cap (U\cdot g) =\emptyset$ for every element $g$ of G other than the identity element (TG, III, p. 32, prop. 8). By Theorem 1, condition (ii) is then satisfied.

The implication (ii)$\Rightarrow$(i) follows from corollary 1 of I, p. 96.

Let V be a neighbourhood of the identity element $e$ of G such that $H\cap V =\{e\}$. There exists an open neighbourhood U of $e$ in G such that $U^{-1}\cdot U\subset V$ (TG, III, p. 3) and consequently $U\cap U\cdot h=\emptyset$ for every $h\in H,h=\not e$. Corollary 2 of I, p. 100 therefore follows from theorem 1.

If moreover the group G is connected, H is contained in the center of G.

The homomorphism $\varphi$ induces a topological group isomorphism of $G/H$ onto $G'$ (TG, III, p. 16, prop. 24), whence the first assertion by Corollary 2. Suppose the group G connected. For every $h\in H$, the continuous mapping of G into H defined by $g\mapsto ghg^{-1}$ is constant, with value $h$. The group H is therefore contained in the center of G.

Let us endow the group Aut$_B(E)^{\circ}$ with the discrete topology; the operation law $(h, x)\mapsto h(x)$ is then continuous. This operation is free (I, p. 34, Corollary 2 of Proposition 11). Since E is a Galois covering of B, its fibres are the orbits of this operation. By Proposition 4 of I, p. 97, E is a principal covering with group Aut$_B(E)^{\circ}$.

(i) The covering E is Galois;

(ii) There exists a discrete topological group G and a continuous right operation of G on E making E into a principal covering with group G;

(iii) The covering $E\times_BE$ of E defined by the projection pr$_1$ is trivializable.

When these conditions are satisfied, the canonical mapping $G\rightarrow$ Aut$_B(E)^{\circ}$ defined by the operation of G is a group isomorphism.

If, moreover, the space B is locally connected, the preceding properties are equivalent to the following property:

(i$'$) There exists a point $b$ of B such that the operation of the group Aut$_B(E)$ on the fibre $E_b$ is transitive.

The implication (i)$\Rightarrow$(ii) results from proposition 5 and the implication (ii)$\Rightarrow$(iii) from remark 1 of I, p. 95. Let us prove (iii)$\Rightarrow$(i). Let us denote by $p: E\rightarrow B$ the projection of the covering E. Since B is connected, this covering has a degree, and this degree is not zero since E is not empty. Let $b$ be a point of B. Let us prove that the operation of Aut$_B(E)$ on the fibre $E_b$ is transitive. From the above, this fibre is not empty. Let $x$ and $x'$ be points of $E_b$. The B-morphisms $h: E\rightarrow E$ such that $h(x) =x'$ correspond bijectively to the continuous sections $s$ of the mapping pr$_1: E\times_BE\rightarrow E$ such that $s(x) = (x, x')$ (I, p. 9, prop. 3). Under assumption (iii), such a section exists (I, p. 70, cor. 2) and is unique (I, p. 34, cor. 1 of prop. 11) since the space E is connected. Thus, for every pair $(x, x')\in E\times_BE$, there exists a unique B-morphism $h: E\rightarrow E$ such that $h(x) =x'$. If $h': E\rightarrow E$ is the unique B-morphism such that $h'(x') =x$, one has $h'(h(x)) =x$ and $h(h'(x')) =x'$, whence $h'\circ h=$ Id$_E$ and $h\circ h'=$ Id$_{E'}$. This proves that $h$ is a B-automorphism of E. Hence the covering E is galoisian.

We have proved that conditions (i), (ii), (iii) are equivalent. Suppose them satisfied. Let $\delta : G\rightarrow$ Aut$_B(E)$ be the mapping which to $g\in G$ associates the B-automorphism $x\mapsto x\cdot g$ of E. The mapping $\delta$ is a group homomorphism of G into Aut$_B(E)^{\circ}$. Since G operates freely in E, the mapping $\delta$ is injective. Let $h\in$ Aut$_B(E)$, let $x\in$ E and let $g$ be the unique element of G such that $x\cdot g=h(x)$. The B-morphisms $h$ and $\delta (g)$ coincide at $x$, hence everywhere, since the space E is connected (I, p. 34, cor. 1 of prop. 11), which proves that $\delta$ is an isomorphism.

Now suppose the space B locally connected and let us prove, under assumption (i$'$), that the covering E is galoisian. Let $E'$ be the quotient space of E by the right operation of Aut$_B(E)^{\circ}$ and let us denote by $q: E\rightarrow E'$ the canonical mapping. It makes E into a surjective covering of $E'($I, p. 98, example 2); the mapping $p: E\rightarrow B$ defines by passing to the quotient a continuous mapping $p': E'\rightarrow B$ such that $p'\circ q=p$. Since the space B is locally connected, the B-space $(E', p')$ is a covering (I, p. 81, prop. 7). Under assumption (i$'$), there exists a point $b$ of B such that the fibre $E'_b$ has exactly one element; since the space B is connected, the same is then true for every point $b$ of B (I, p. 74, prop. 4), which proves that E is a galoisian covering of B.

Since the space B is locally connected, the same is true of E, so that $E_0$ is an open subspace of E (TG, I, p. 85, prop. 11). Since it is also closed (TG, I, p. 83), the space $E_0$ is therefore a covering of B (I, p. 80, cor. 1). Since B is connected, this covering has a degree; since $E_0$ is not empty, all the fibres of $p|E_0$ are therefore non-empty. Let $x$ be a point of $E_0$, let $x'\in E_0$ be such that $p(x') =p(x)$; there exists an element $g\in G$ such that $x\cdot g=x'$. Since the connected components $E_0$ and $E_0\cdot g$ then have a common point, they are equal, whence $g\in G_0$. Thus, the group $G_0$ operates transitively in the fibre of the B-space $E_0$ at $p(x)$. Proposition 6 follows.

The mapping $\lambda_0$ is surjective and two elements of $(B'\times_BE)\times F$ have the same image under $\lambda_0$ if and only if they belong to the same orbit for the operation of G in $(B'\times_BE)\times F$. It follows that the mapping $\lambda$ is bijective. Since the mapping $\pi$ is open, the same is true of the mapping Id$_{B'}\times_B\pi ($I, p. 17, prop. 8), hence of $\lambda_0$ and of $\lambda$ (TG, I, p. 32, prop. 3), which proves that $\lambda$ is a homeomorphism.

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.