[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$. 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]

[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]

[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]