Let $H$ be a closed subgroup of a Lie group $G$. Then $H$ acts on $G$ by left translation. The action is:
(i): free
(ii): proper
Proof: (i) is clear. For (ii), we need to show that the preimage of compact sets under $p: H \times G \rightarrow G \times G, (h,g) \mapsto (hg,g)$ are compact. The image $S$ of $p$ is the set of $(g_1,g_2) \in G \times G$ such that $Hg_1 = Hg_2$. Then $S$ is closed, as it the preimage of the diagonal map of
$$G \times G \rightarrow H \backslash G \times H \backslash G$$
Now $p: H \times G \rightarrow S$ is a bijection with continuous inverse $p^{-1}: S \rightarrow H \times G$ given by $(g_1,g_2) \mapsto (g_1g_2^{-1},g_2)$. Thus if $K \subseteq G \times G$ is compact, so is $S \cap K$, then so is $p^{-1}(S \cap K) = p^{-1}(K)$.
General theory of Lie groups then tells us that the quotient $H \backslash G$ has a unique manifold structure such that the quotient map
$$\pi: G \rightarrow H \backslash G$$
is a submersion, and $\pi$ becomes a principal fibre bundle with $H$ as a fibre. This should imply that local trivial sections exist everywhere: $H \backslash G$ is covered by open sets $U$ such that $\pi^{-1}(U)$ looks like $H \times U$ with the action $h'.(h,u) = (h'h,u)$.
I have never thought about the quotient map of a group onto a coset space as looking anything like a principal fibre bundle (unless we have something like $G = H \times H'$). Suppose I did not know anything about $H \backslash G$ having a manifold structure. Is it possible to see directly that $\pi: G \rightarrow H \backslash G$ has local trivial sections?
Best Answer
The construction of such a section is actually part of the standard proof that $H\backslash G$ is a smooth manifold. Consider a linear subspace $V$ in the Lie algebra $\mathfrak g$ of $G$ that is complementary to the Lie subalgebra $\mathfrak h$ corresponding to $H$. Then one shows that there is a neighborhood $W$ of $0$ in $V$ such that $\exp(W)$ intersects $H$ only in the neutral element $e$. Possibily shrinking $W$, $\psi(X):=H\exp(X)$ defines a diffeomorphism from $W$ onto an open neighborhood of $o:=He\in H\backslash G$ (which is the inverse of a standard chart for the manifold structure on that space). The trivializing section around $o$ is then defined by $\sigma(\psi(X)):=\exp(X)$. Then you just transport this around using right translations on $G$ and $H\backslash G$ by elements of $G$.