The canonical principal-bundle candidate G to G/H

Assume ${\mathrm{A}\mathrm{C}}_{\omega }$, let $H$ be a closed subgroup of a finite-dimensional real Lie group $G$, and give $G\mathrm{/}H$ the quotient manifold structure of Quotient manifold by a closed Lie subgroup. The map

$q:G\to G\mathrm{/}H,q(g)=gH,$

together with the smooth right action

$G\times H\to G,(g,h)⟼g\cdot h=gh,$

is the canonical principal-$H$-bundle candidate over $G\mathrm{/}H$.

The action is free, and its orbits are precisely the fibres of $q$: $gH=g^{\mathrm{\prime }}H$ exactly when $g^{\mathrm{\prime }}=gh$ for a unique $h\in H$. A smooth principal trivialization over $U\subseteq G\mathrm{/}H$ means a diffeomorphism over $U$

$\mathrm{\Theta }:q^{-1}(U)⟶U\times H$

that is $H$-equivariant for $(x,h)\cdot k=(x,hk)$. Thus, if $\mathrm{\Theta }(g)=(q(g),h)$, then $\mathrm{\Theta }(gk)=(q(g),hk)$. This is the smooth version of the right-principal convention in Principal g bundle and associated fiber bundle and of the local-trivialization convention in Smooth fibre bundles and local trivializations. The next theorem proves that such charts cover $G\mathrm{/}H$; their existence is not built into this definition. Countable choice is used only to supply the quotient manifold.