[proofplan]
The proof constructs the two maps explicitly and verifies that each construction has the required smooth structure. A reduction $Q \subset P$ determines, fibre by fibre, a single right $H$-orbit inside each principal $G$-fibre $P_m$, hence a point of $(P/H)_m$; local sections of the principal $H$-bundle $Q \to M$ prove smoothness. Conversely, a section of $P/H$ selects one right $H$-orbit in each fibre of $P$, and its inverse image under the quotient map is shown locally to be $U \times H$ after choosing a local lift of the corresponding map $U \to G/H$. The two constructions are inverse because both remember exactly the same data: one right $H$-orbit in every fibre of $P$.
[/proofplan]
[step:Define the quotient map and the local model for $P/H$]
Let
\begin{align*}
\rho: P &\to P/H
\end{align*}
denote the smooth quotient map for the restricted right action of $H$ on $P$, so $\rho(u) = [u]_H$ for $u \in P$. Since $H$ is closed in $G$, the homogeneous space $G/H$ is a smooth manifold and the projection
\begin{align*}
q_G: G &\to G/H
\end{align*}
is a smooth principal right $H$-bundle (citing a result not yet in the wiki: Closed Subgroup Theorem and homogeneous space construction).
Let $U \subset M$ be an [open set](/page/Open%20Set) over which $P$ is trivial, and fix a smooth principal $G$-bundle trivialization
\begin{align*}
\Psi: \pi^{-1}(U) &\to U \times G.
\end{align*}
Thus there is a smooth map
\begin{align*}
\Psi_G: \pi^{-1}(U) &\to G
\end{align*}
such that $\Psi(u) = (\pi(u), \Psi_G(u))$, and $\Psi_G(u g) = \Psi_G(u) g$ for all $u \in \pi^{-1}(U)$ and $g \in G$. This trivialization induces a smooth bundle trivialization
\begin{align*}
\overline{\Psi}: \bar{\pi}^{-1}(U) &\to U \times G/H
\end{align*}
defined by
\begin{align*}
\overline{\Psi}([u]_H) = (\pi(u), \Psi_G(u)H).
\end{align*}
The definition is independent of the representative $u$ because $\Psi_G(u h)H = \Psi_G(u)hH = \Psi_G(u)H$ for every $h \in H$.
[/step]
[step:Send a reduction to the section determined by its fibrewise $H$-orbits]
Let $Q \subset P$ be a reduction of $P$ to $H$. For each $m \in M$, the fibre $Q_m = Q \cap P_m$ is a right $H$-torsor. Define
\begin{align*}
\sigma_Q: M &\to P/H
\end{align*}
by choosing any $u \in Q_m$ and setting
\begin{align*}
\sigma_Q(m) = [u]_H.
\end{align*}
This is well-defined: if $u, v \in Q_m$, then the principal right $H$-action on $Q_m$ is transitive, so there exists $h \in H$ with $v = u h$, and therefore $[v]_H = [u h]_H = [u]_H$.
It is a section of $\bar{\pi}$ because
\begin{align*}
\bar{\pi}(\sigma_Q(m)) = \bar{\pi}([u]_H) = \pi(u) = m.
\end{align*}
To prove smoothness, let $U \subset M$ be an open set admitting a smooth local section
\begin{align*}
\tau: U &\to Q
\end{align*}
of the principal right $H$-bundle $Q \to M$. Let
\begin{align*}
\iota: Q &\to P
\end{align*}
be the smooth inclusion. For $m \in U$,
\begin{align*}
\sigma_Q(m) = \rho(\iota(\tau(m))).
\end{align*}
Hence
\begin{align*}
\sigma_Q|_U = \rho \circ \iota \circ \tau.
\end{align*}
The right-hand side is a composition of smooth maps, so $\sigma_Q$ is smooth on $U$. Since such open sets cover $M$, $\sigma_Q$ is smooth on $M$.
[/step]
[step:Recover an $H$-subbundle from a section of $P/H$]
Let
\begin{align*}
\sigma: M &\to P/H
\end{align*}
be a smooth section of $\bar{\pi}$. Define
\begin{align*}
Q_\sigma = \{u \in P : \rho(u) = \sigma(\pi(u))\}.
\end{align*}
For every $m \in M$, define the fibre
\begin{align*}
(Q_\sigma)_m = Q_\sigma \cap P_m.
\end{align*}
Because $\sigma(m) \in (P/H)_m$, there exists $u \in P_m$ with $\rho(u) = \sigma(m)$, so $(Q_\sigma)_m$ is nonempty. If $u \in (Q_\sigma)_m$ and $h \in H$, then
\begin{align*}
\rho(u h) = \rho(u) = \sigma(m),
\end{align*}
so $u h \in (Q_\sigma)_m$. Conversely, if $u, v \in (Q_\sigma)_m$, then $\rho(u) = \rho(v)$, so $v = u h$ for some $h \in H$. Since the right $G$-action on $P_m$ is free, this $h$ is unique. Therefore each fibre $(Q_\sigma)_m$ is a right $H$-torsor.
It remains to prove that $Q_\sigma$ is a smooth principal right $H$-subbundle of $P$.
[guided]
We begin with a smooth section
\begin{align*}
\sigma: M &\to P/H.
\end{align*}
The intended subbundle is the set of all points of $P$ whose right $H$-orbit is the orbit selected by $\sigma$. Thus we define
\begin{align*}
Q_\sigma = \{u \in P : \rho(u) = \sigma(\pi(u))\},
\end{align*}
where
\begin{align*}
\rho: P &\to P/H
\end{align*}
is the quotient map $u \mapsto [u]_H$.
First we check the fibrewise algebra. For $m \in M$, define
\begin{align*}
(Q_\sigma)_m = Q_\sigma \cap P_m.
\end{align*}
Since $\sigma$ is a section, $\sigma(m)$ lies in the fibre $(P/H)_m$. By the definition of the quotient bundle, every point of $(P/H)_m$ is the right $H$-orbit of at least one point of $P_m$. Hence there exists $u \in P_m$ such that $\rho(u) = \sigma(m)$, and therefore $(Q_\sigma)_m$ is nonempty.
The set $(Q_\sigma)_m$ is stable under the right action of $H$. Indeed, if $u \in (Q_\sigma)_m$ and $h \in H$, then $\pi(u h) = \pi(u) = m$, and the quotient map is constant on right $H$-orbits:
\begin{align*}
\rho(u h) = [u h]_H = [u]_H = \rho(u) = \sigma(m).
\end{align*}
Thus $u h \in (Q_\sigma)_m$.
Now suppose $u, v \in (Q_\sigma)_m$. Then
\begin{align*}
\rho(u) = \sigma(m) = \rho(v).
\end{align*}
Equality in the quotient $P/H$ means exactly that $u$ and $v$ differ by the right action of an element of $H$, so there exists $h \in H$ such that $v = u h$. This element is unique because the original right action of $G$ on the principal bundle $P$ is free, and $H \le G$. Therefore $(Q_\sigma)_m$ is a right $H$-torsor.
The remaining issue is smoothness. A fibrewise torsor is not yet a principal subbundle; we must show that locally it looks like $U \times H$ by smooth $H$-equivariant trivializations. Let $U \subset M$ be an open set over which $P$ is trivial, and fix a principal $G$-bundle trivialization
\begin{align*}
\Psi: \pi^{-1}(U) &\to U \times G.
\end{align*}
Write $\Psi(u) = (\pi(u), \Psi_G(u))$, where
\begin{align*}
\Psi_G: \pi^{-1}(U) &\to G
\end{align*}
is smooth and satisfies $\Psi_G(u g) = \Psi_G(u)g$. The induced trivialization of the quotient bundle is
\begin{align*}
\overline{\Psi}: \bar{\pi}^{-1}(U) &\to U \times G/H,
\end{align*}
with
\begin{align*}
\overline{\Psi}([u]_H) = (\pi(u), \Psi_G(u)H).
\end{align*}
Because $\sigma$ is smooth, its expression in this quotient trivialization has the form
\begin{align*}
\overline{\Psi}(\sigma(m)) = (m, f(m))
\end{align*}
for a smooth map
\begin{align*}
f: U &\to G/H.
\end{align*}
The projection
\begin{align*}
q_G: G &\to G/H
\end{align*}
is a smooth principal right $H$-bundle, so it admits smooth local sections. Therefore, after replacing $U$ by a smaller open neighbourhood $V \subset U$ if necessary, there exists a smooth map
\begin{align*}
\ell: V &\to G
\end{align*}
such that
\begin{align*}
q_G(\ell(m)) = f(m)
\end{align*}
for every $m \in V$.
We now describe $Q_\sigma$ over $V$. A point $u \in \pi^{-1}(V)$ belongs to $Q_\sigma$ exactly when
\begin{align*}
\rho(u) = \sigma(\pi(u)).
\end{align*}
Applying the quotient trivialization gives, with $m = \pi(u)$,
\begin{align*}
(m, \Psi_G(u)H) = (m, f(m)) = (m, \ell(m)H).
\end{align*}
Thus $\Psi_G(u)H = \ell(m)H$, which is equivalent to the existence of a unique $h \in H$ such that
\begin{align*}
\Psi_G(u) = \ell(m)h.
\end{align*}
This proves that $Q_\sigma \cap \pi^{-1}(V)$ is parametrized by $V \times H$.
Define
\begin{align*}
\Theta_V: V \times H &\to Q_\sigma \cap \pi^{-1}(V)
\end{align*}
by
\begin{align*}
\Theta_V(m,h) = \Psi^{-1}(m,\ell(m)h).
\end{align*}
The map $\Theta_V$ is smooth because $\Psi^{-1}$, $\ell$, and multiplication in $G$ are smooth. Its inverse sends $u \in Q_\sigma \cap \pi^{-1}(V)$ to $(\pi(u),h)$, where $h \in H$ is the unique element satisfying $\Psi_G(u)=\ell(\pi(u))h$; this inverse is smooth because in the trivialization it is just
\begin{align*}
(m,\ell(m)h) \mapsto (m,h).
\end{align*}
Finally, $\Theta_V$ is right $H$-equivariant:
\begin{align*}
\Theta_V(m,hk) = \Psi^{-1}(m,\ell(m)hk) = \Theta_V(m,h)k
\end{align*}
for all $m \in V$ and $h,k \in H$. Therefore $Q_\sigma$ is locally a smooth principal right $H$-bundle over $M$, embedded in $P$ as an $H$-equivariant subbundle.
[/guided]
Choose $U \subset M$ and $\Psi$ as above. In the induced quotient trivialization, write
\begin{align*}
\overline{\Psi}(\sigma(m)) = (m, f(m))
\end{align*}
for a smooth map
\begin{align*}
f: U &\to G/H.
\end{align*}
Since $q_G: G \to G/H$ is a smooth principal right $H$-bundle, after shrinking to an open set $V \subset U$ there is a smooth lift
\begin{align*}
\ell: V &\to G
\end{align*}
with $q_G \circ \ell = f|_V$.
Define
\begin{align*}
\Theta_V: V \times H &\to Q_\sigma \cap \pi^{-1}(V)
\end{align*}
by
\begin{align*}
\Theta_V(m,h) = \Psi^{-1}(m,\ell(m)h).
\end{align*}
For $m \in V$ and $h \in H$, the point $\Theta_V(m,h)$ lies in $Q_\sigma$ because its quotient coordinate is
\begin{align*}
\ell(m)hH = \ell(m)H = f(m).
\end{align*}
Conversely, if $u \in Q_\sigma \cap \pi^{-1}(V)$ and $m=\pi(u)$, then
\begin{align*}
\Psi_G(u)H = f(m) = \ell(m)H,
\end{align*}
so there is a unique $h \in H$ with $\Psi_G(u)=\ell(m)h$. Hence $u=\Theta_V(m,h)$. This proves that $\Theta_V$ is bijective. In the coordinates given by $\Psi$, its inverse is $(m,\ell(m)h) \mapsto (m,h)$, so $\Theta_V$ is a diffeomorphism. It is right $H$-equivariant because
\begin{align*}
\Theta_V(m,hk) = \Theta_V(m,h)k
\end{align*}
for all $h,k \in H$. Therefore $Q_\sigma$ is a smooth principal right $H$-subbundle of $P$.
[/step]
[step:Verify that the two constructions are inverse]
Let $Q \subset P$ be a reduction, and form $\sigma_Q$ and then $Q_{\sigma_Q}$. For $u \in P$ with $m=\pi(u)$,
\begin{align*}
u \in Q_{\sigma_Q}
\end{align*}
if and only if
\begin{align*}
[u]_H = \sigma_Q(m).
\end{align*}
By definition of $\sigma_Q(m)$, this means that $[u]_H = [v]_H$ for some $v \in Q_m$. Equivalently, $u = v h$ for some $h \in H$. Since $Q_m$ is stable under the right action of $H$, this is equivalent to $u \in Q_m$. Hence $Q_{\sigma_Q}=Q$.
Conversely, let $\sigma: M \to P/H$ be a smooth section, and form $Q_\sigma$ and then $\sigma_{Q_\sigma}$. For each $m \in M$, choose any $u \in (Q_\sigma)_m$. By the definition of $Q_\sigma$,
\begin{align*}
[u]_H = \rho(u) = \sigma(m).
\end{align*}
Therefore
\begin{align*}
\sigma_{Q_\sigma}(m) = [u]_H = \sigma(m).
\end{align*}
Thus $\sigma_{Q_\sigma}=\sigma$. The two assignments are inverse bijections between reductions of $P$ to $H$ and smooth sections of $P/H \to M$.
[/step]
