Marsden--Weinstein--Meyer symplectic reduction

If the level is empty, its quotient is the empty smooth manifold and the unique two-form on it is closed and nondegenerate vacuously, so the conclusion holds. Henceforth suppose the level is nonempty. The restricted form ${\iota }^{\ast }\omega$ is $G_{\alpha }$-invariant: for $h\in G_{\alpha }$ the action $a_h$ preserves the level by [F3], so $a_h{\mathrm{\mid }}_{{\mu }^{-1}(\alpha )}$ is a diffeomorphism of the level with $\iota \circ a_h{\mathrm{\mid }}_{\text{level}}=a_h\circ \iota$, and $(a_h{\mathrm{\mid }}_{\text{level}}{)}^{\ast }{\iota }^{\ast }\omega ={\iota }^{\ast }{a}_h^{\ast }\omega ={\iota }^{\ast }\omega$ because $a_h$ preserves $\omega$.

The restricted form is horizontal for the $G_{\alpha }$-action: by [F4] each vertical vector ${\xi }_M(p)$, $\xi \in {\mathfrak{g}}_{\alpha }$, lies in the kernel of $({\iota }^{\ast }\omega {)}_p$, so any contraction of ${\iota }^{\ast }\omega$ with a vertical entry vanishes.

By the descent lemma [F5] applied to the free proper $G_{\alpha }$-action on the level, there is a unique two-form ${\omega }_{\alpha }$ on $M_{\alpha }$ with ${\pi }^{\ast }{\omega }_{\alpha }={\iota }^{\ast }\omega$.

Closedness: ${\pi }^{\ast }(d{\omega }_{\alpha })=d({\pi }^{\ast }{\omega }_{\alpha })=d({\iota }^{\ast }\omega )={\iota }^{\ast }(d\omega )=0$ by [F6]; a form on the base with zero pullback vanishes by [F5], so $d{\omega }_{\alpha }=0$.

Nondegeneracy: let $v\in T_{[p]}{M}_{\alpha }$ with ${\omega }_{\alpha }(v,w)=0$ for all $w\in T_{[p]}{M}_{\alpha }$. Choose $\tilde{v}\in T_p{\mu }^{-1}(\alpha )$ with $d{\pi }_p\tilde{v}=v$; since $\pi$ restricted to the level is a submersion, every $\tilde{w}\in T_p{\mu }^{-1}(\alpha )$ is a lift of some $w$, so $({\iota }^{\ast }\omega {)}_p(\tilde{v},\tilde{w})={\omega }_{\alpha }(v,d{\pi }_p\tilde{w})=0$ for all $\tilde{w}\in T_p{\mu }^{-1}(\alpha )$. Hence $\tilde{v}\in \ker ({\iota }^{\ast }\omega {)}_p=T_p(G_{\alpha }\cdot p)$ by [F4], and therefore $v=d{\pi }_p\tilde{v}=0$ by [F4]. Thus ${\omega }_{\alpha }$ is pointwise nondegenerate.

Steps 3.1 and 3.2 show that ${\omega }_{\alpha }$ is closed and nondegenerate, hence symplectic on the manifold $M_{\alpha }$ of [F2]; step 2.1 gives existence and uniqueness of the form with ${\pi }^{\ast }{\omega }_{\alpha }={\iota }^{\ast }\omega$.