[proofplan] The proof first constructs the reduced space as a smooth quotient: regularity makes $J^{-1}(\mu)$ a submanifold, and the free proper action of $G_\mu$ makes the orbit space smooth. The main calculation identifies the kernel of the pulled-back two-form $i_\mu^*\omega$ with the tangent spaces to the $G_\mu$-orbits. This kernel computation proves that $i_\mu^*\omega$ is precisely the kind of invariant horizontal form that descends through the quotient map. The descended form is closed because $\omega$ is closed, and it is nondegenerate because the only vectors killed by $i_\mu^*\omega$ are exactly the vertical quotient directions. [/proofplan]

[step:Construct the level set and quotient manifold] Set \begin{align*} N:=J^{-1}(\mu). \end{align*} Since $\mu$ is a regular value of the smooth map $J:M\to\mathfrak g^*$, the regular-level-set consequence of the [Implicit Function Theorem](/theorems/52) applies, and $N$ is an embedded submanifold of $M$ with \begin{align*} T_xN=\ker dJ_x \end{align*} for every $x\in N$. The stabilizer $G_\mu$ is a Lie subgroup of $G$ because it is the stabilizer of $\mu$ for the smooth coadjoint action of $G$ on $\mathfrak g^*$. Since the induced action of this Lie group $G_\mu$ on $N$ is free and proper by hypothesis, the smooth quotient construction for free proper Lie group actions applies, so \begin{align*} M_\mu:=N/G_\mu \end{align*} has a unique smooth manifold structure for which the quotient projection $\pi_\mu:N\to M_\mu$ is a surjective submersion. For each $\xi\in\mathfrak g$, let $\xi_M\in\mathfrak X(M)$ denote the infinitesimal action vector field defined by $\xi_M(x)=\left.\frac{d}{dt}\right|_{t=0}\exp(t\xi)\cdot x\in T_xM$ for $x\in M$. The vertical tangent space of $\pi_\mu$ at $x\in N$ is \begin{align*} \ker d(\pi_\mu)_x=\{\xi_M(x):\xi\in\mathfrak g_\mu\}, \end{align*} where $\mathfrak g_\mu=\{\xi\in\mathfrak g:\operatorname{ad}_\xi^*\mu=0\}$ is the Lie algebra of $G_\mu$. Here, for each $\xi\in\mathfrak g$, the infinitesimal coadjoint action is the [linear map](/page/Linear%20Map) $\operatorname{ad}_\xi^*:\mathfrak g^*\to\mathfrak g^*$ defined by \begin{align*} \operatorname{ad}_\xi^*\lambda:=\left.\frac{d}{dt}\right|_{t=0}\operatorname{Ad}_{\exp(t\xi)}^*\lambda \end{align*} for $\lambda\in\mathfrak g^*$. [/step]

[step:Identify the kernel of the pulled-back two-form with the orbit directions]Let $\alpha:=i_\mu^*\omega\in\Omega^2(N)$. We prove that for every $x\in N$, \begin{align*} \ker \alpha_x=\{\xi_M(x):\xi\in\mathfrak g_\mu\}. \end{align*} First let $\xi\in\mathfrak g_\mu$ and let $v\in T_xN$. We use the Hamiltonian momentum-map convention fixed in the theorem statement: for $J_\xi:M\to\mathbb R$ defined by $J_\xi(y)=J(y)(\xi)$ and for the equivariant convention $J(g\cdot y)=\operatorname{Ad}_g^*J(y)$, the infinitesimal momentum identity is $\iota_{\xi_M}\omega=dJ_\xi$. Hence \begin{align*} \alpha_x(\xi_M(x),v)=\omega_x(\xi_M(x),v)=d(J_\xi)_x(v)=dJ_x(v)(\xi). \end{align*} Because $v\in T_xN=\ker dJ_x$, the last term is zero. Hence $\xi_M(x)\in\ker\alpha_x$. Conversely, take $v\in\ker\alpha_x$. Then $v\in T_xN=\ker dJ_x$, and \begin{align*} \omega_x(v,w)=0 \end{align*} for every $w\in T_xN=\ker dJ_x$. Define the linear map $L_x:\mathfrak g\to T_xM$ by $L_x(\xi)=\xi_M(x)$. For every $w\in T_xM$ and every $\xi\in\mathfrak g$, the momentum map identity gives \begin{align*} dJ_x(w)(\xi)=d(J_\xi)_x(w)=\omega_x(\xi_M(x),w)=\omega_x(L_x(\xi),w). \end{align*} Thus $\ker dJ_x=(\operatorname{Range}L_x)^\omega$, where the symplectic orthogonal is taken inside the symplectic [vector space](/page/Vector%20Space) $(T_xM,\omega_x)$. Since $\mu$ is a regular value, $dJ_x:T_xM\to\mathfrak g^*$ is surjective. We claim that $L_x$ is injective. If $L_x(\xi)=0$, then for every $w\in T_xM$, \begin{align*} dJ_x(w)(\xi)=\omega_x(L_x(\xi),w)=0. \end{align*} Surjectivity of $dJ_x$ means that every element of $\mathfrak g^*$ occurs as $dJ_x(w)$ for some $w\in T_xM$, so $\lambda(\xi)=0$ for every $\lambda\in\mathfrak g^*$. Hence $\xi=0$, and $L_x$ is injective. Therefore \begin{align*} \dim \operatorname{Range}L_x=\dim\mathfrak g. \end{align*} The finite-dimensional symplectic orthogonal identity then gives \begin{align*} (\ker dJ_x)^\omega=((\operatorname{Range}L_x)^\omega)^\omega=\operatorname{Range}L_x. \end{align*} Since $v$ annihilates $\ker dJ_x$ under $\omega_x$, we have $v\in(\ker dJ_x)^\omega$, so there exists $\xi\in\mathfrak g$ such that \begin{align*} v=\xi_M(x). \end{align*} Because $v\in T_xN=\ker dJ_x$, we have $dJ_x(\xi_M(x))=0$. To compute this derivative from equivariance, consider the curve $c:\mathbb R\to M$ defined by $c(t)=\exp(t\xi)\cdot x$. Then $c(0)=x$ and $c'(0)=\xi_M(x)$. Equivariance of $J$ gives $J(c(t))=\operatorname{Ad}_{\exp(t\xi)}^*J(x)$ for all $t$ for which the expression is defined. Differentiating at $t=0$ and using $J(x)=\mu$ gives \begin{align*} 0=dJ_x(\xi_M(x))=\left.\frac{d}{dt}\right|_{t=0}\operatorname{Ad}_{\exp(t\xi)}^*J(x)=\operatorname{ad}_\xi^*\mu. \end{align*} Hence $\xi\in\mathfrak g_\mu$, and $v$ is tangent to the $G_\mu$-orbit through $x$.[/step]

[guided]We want to understand exactly which tangent vectors are killed by the restricted two-form $\alpha=i_\mu^*\omega$. This is the key point because quotienting by $G_\mu$ removes precisely the tangent directions to the $G_\mu$-orbits. Thus the desired form on the quotient can be nondegenerate only if the degeneracy of $\alpha$ is exactly vertical. Fix $x\in N=J^{-1}(\mu)$. Since $\mu$ is a regular value of $J:M\to\mathfrak g^*$, the tangent space to the level set is \begin{align*} T_xN=\ker dJ_x. \end{align*} For each $\xi\in\mathfrak g$, the notation $\xi_M\in\mathfrak X(M)$ denotes the infinitesimal action vector field defined by $\xi_M(z)=\left.\frac{d}{dt}\right|_{t=0}\exp(t\xi)\cdot z\in T_zM$ for $z\in M$. Let $\xi\in\mathfrak g_\mu$, and let $v\in T_xN$. Before evaluating $\alpha_x$ on $\xi_M(x)$, we verify that this infinitesimal action vector is tangent to $N$. Define the curve $c:\mathbb R\to M$ by $c(t)=\exp(t\xi)\cdot x$. Equivariance gives $J(c(t))=\operatorname{Ad}_{\exp(t\xi)}^*\mu$, so \begin{align*} \left.\frac{d}{dt}\right|_{t=0}J(c(t))=\operatorname{ad}_\xi^*\mu=0 \end{align*} because $\xi\in\mathfrak g_\mu$. Hence $\xi_M(x)=c'(0)\in\ker dJ_x=T_xN$. The function associated to $\xi$ by the momentum map is $J_\xi:M\to\mathbb R$, defined by $J_\xi(y)=J(y)(\xi)$. We are using the convention that equivariance means $J(g\cdot y)=\operatorname{Ad}_g^*J(y)$ and the Hamiltonian momentum-map identity is \begin{align*} \iota_{\xi_M}\omega=dJ_\xi. \end{align*} Evaluating this identity at $x$ on the vector $v$ gives \begin{align*} \alpha_x(\xi_M(x),v)=\omega_x(\xi_M(x),v)=d(J_\xi)_x(v)=dJ_x(v)(\xi). \end{align*} Since $v\in T_xN=\ker dJ_x$, the element $dJ_x(v)\in\mathfrak g^*$ is zero, so $dJ_x(v)(\xi)=0$. Therefore every vector tangent to a $G_\mu$-orbit lies in $\ker\alpha_x$. The harder direction is to show that there are no additional kernel vectors. Suppose $v\in\ker\alpha_x$. Then $v\in T_xN$ and \begin{align*} \omega_x(v,w)=0 \end{align*} for every $w\in T_xN=\ker dJ_x$. Define the infinitesimal action map $L_x:\mathfrak g\to T_xM$ by $L_x(\xi)=\xi_M(x)$, and define \begin{align*} \operatorname{Range}L_x:=\{L_x(\xi):\xi\in\mathfrak g\}\subset T_xM. \end{align*} For every $w\in T_xM$ and every $\xi\in\mathfrak g$, the momentum map identity gives \begin{align*} dJ_x(w)(\xi)=d(J_\xi)_x(w)=\omega_x(L_x(\xi),w). \end{align*} This formula says exactly that a vector $w$ lies in $\ker dJ_x$ if and only if it is symplectically orthogonal to every infinitesimal orbit vector $L_x(\xi)$. Hence \begin{align*} \ker dJ_x=(\operatorname{Range}L_x)^\omega. \end{align*} Now use finite-dimensional symplectic linear algebra. Since $dJ_x$ is surjective, $\ker dJ_x$ has codimension $\dim\mathfrak g$. We also need to justify that $\operatorname{Range}L_x$ has dimension $\dim\mathfrak g$, which is equivalent to injectivity of $L_x$. Suppose $L_x(\xi)=0$. Then for every $w\in T_xM$, \begin{align*} dJ_x(w)(\xi)=\omega_x(L_x(\xi),w)=0. \end{align*} Because $dJ_x:T_xM\to\mathfrak g^*$ is surjective, every $\lambda\in\mathfrak g^*$ has the form $\lambda=dJ_x(w)$ for some $w\in T_xM$. Hence $\lambda(\xi)=0$ for every $\lambda\in\mathfrak g^*$, so $\xi=0$. Thus $L_x$ is injective and $\dim\operatorname{Range}L_x=\dim\mathfrak g$. Therefore taking the symplectic orthogonal twice gives \begin{align*} (\ker dJ_x)^\omega=((\operatorname{Range}L_x)^\omega)^\omega=\operatorname{Range}L_x. \end{align*} Because $v$ annihilates $\ker dJ_x$ under $\omega_x$, we have $v\in(\ker dJ_x)^\omega$, so there exists $\xi\in\mathfrak g$ such that \begin{align*} v=\xi_M(x). \end{align*} It remains to prove that this $\xi$ actually belongs to $\mathfrak g_\mu$, not just to $\mathfrak g$. Since $v\in T_xN=\ker dJ_x$, we have $dJ_x(v)=0$, and substituting $v=\xi_M(x)$ gives $dJ_x(\xi_M(x))=0$. To compute this derivative, define the curve $c:\mathbb R\to M$ by $c(t)=\exp(t\xi)\cdot x$. Then $c(0)=x$ and $c'(0)=\xi_M(x)$. Equivariance of $J$ gives \begin{align*} J(c(t))=\operatorname{Ad}_{\exp(t\xi)}^*J(x) \end{align*} for all $t$ for which the expression is defined. Differentiating at $t=0$ and using $J(x)=\mu$ gives \begin{align*} 0=dJ_x(\xi_M(x))=\left.\frac{d}{dt}\right|_{t=0}\operatorname{Ad}_{\exp(t\xi)}^*J(x)=\operatorname{ad}_\xi^*\mu. \end{align*} Thus $\xi\in\mathfrak g_\mu$. Therefore \begin{align*} \ker\alpha_x=\{\xi_M(x):\xi\in\mathfrak g_\mu\}, \end{align*} which is exactly the vertical tangent space of the quotient projection.[/guided]

[step:Show that the restricted two-form is basic for the quotient map] The form $\alpha=i_\mu^*\omega$ is horizontal because the previous step gives \begin{align*} \ker d(\pi_\mu)_x=\ker\alpha_x \end{align*} for every $x\in N$. It is also $G_\mu$-invariant. Indeed, for each $g\in G_\mu$, let $\Phi_g:M\to M$ be the diffeomorphism defined by the action, and let $\Phi_g^N:N\to N$ be its restriction to $N$. The restriction is well-defined because $J(\Phi_g(x))=\operatorname{Ad}_g^*J(x)=\operatorname{Ad}_g^*\mu=\mu$ for $x\in N$. Since the action is symplectic, $\Phi_g^*\omega=\omega$, and therefore \begin{align*} (\Phi_g^N)^*\alpha=(\Phi_g^N)^*i_\mu^*\omega=i_\mu^*\Phi_g^*\omega=i_\mu^*\omega=\alpha. \end{align*} Thus $\alpha$ is horizontal and invariant. [/step]

[step:Descend the restricted two-form to the reduced space] For $y\in M_\mu$, choose $x\in N$ with $\pi_\mu(x)=y$. For tangent vectors $u,v\in T_yM_\mu$, choose $a,b\in T_xN$ satisfying \begin{align*} d(\pi_\mu)_x(a)=u \end{align*} and \begin{align*} d(\pi_\mu)_x(b)=v. \end{align*} Define a bilinear alternating form at $y$ by \begin{align*} (\omega_\mu)_y(u,v):=\alpha_x(a,b). \end{align*} This definition is independent of the chosen lifts because replacing $a$ or $b$ by another lift changes it by a vector in $\ker d(\pi_\mu)_x=\ker\alpha_x$. It is independent of the representative $x$ in the orbit as follows. Suppose $x'=g\cdot x$ for some $g\in G_\mu$, and let $a',b'\in T_{x'}N$ be arbitrary lifts of $u,v$. The vectors $d(\Phi_g^N)_x(a)$ and $d(\Phi_g^N)_x(b)$ are also lifts of $u,v$, because $\pi_\mu\circ\Phi_g^N=\pi_\mu$. By the lift-independence already proved at the point $x'$, replacing $a',b'$ by these pushforward lifts does not change the value. Then $G_\mu$-invariance of $\alpha$ gives \begin{align*} \alpha_{x'}(d(\Phi_g^N)_x(a),d(\Phi_g^N)_x(b))=\alpha_x(a,b). \end{align*} Hence $\omega_\mu$ is a well-defined two-form on $M_\mu$. Smoothness follows from the fact that $\pi_\mu:N\to M_\mu$ is a surjective submersion: on every coordinate neighbourhood admitting a smooth local section $s:U\to N$ of $\pi_\mu$, the restriction of $\omega_\mu$ to $U$ is $s^*\alpha$, hence smooth. By construction, \begin{align*} \pi_\mu^*\omega_\mu=\alpha=i_\mu^*\omega. \end{align*} Uniqueness follows because $\pi_\mu$ is a surjective submersion: if $\beta\in\Omega^2(M_\mu)$ satisfies $\pi_\mu^*\beta=0$, then evaluating at lifts of tangent vectors through the surjective maps $d(\pi_\mu)_x:T_xN\to T_{\pi_\mu(x)}M_\mu$ gives $\beta=0$. [/step]

[step:Verify that the descended form is closed and nondegenerate] Since $\omega$ is symplectic, $d\omega=0$. Therefore \begin{align*} \pi_\mu^*(d\omega_\mu)=d(\pi_\mu^*\omega_\mu)=d(i_\mu^*\omega)=i_\mu^*(d\omega)=0. \end{align*} Because pullback by a surjective submersion is injective on differential forms, $d\omega_\mu=0$. It remains to prove nondegeneracy. Let $y\in M_\mu$, and let $u\in T_yM_\mu$ satisfy \begin{align*} (\omega_\mu)_y(u,v)=0 \end{align*} for every $v\in T_yM_\mu$. Choose $x\in N$ with $\pi_\mu(x)=y$, and choose $a\in T_xN$ with $d(\pi_\mu)_x(a)=u$. For every $b\in T_xN$, set $v=d(\pi_\mu)_x(b)$. Then \begin{align*} \alpha_x(a,b)=(\omega_\mu)_y(u,v)=0. \end{align*} Thus $a\in\ker\alpha_x$. By the kernel computation, $\ker\alpha_x=\ker d(\pi_\mu)_x$, so \begin{align*} u=d(\pi_\mu)_x(a)=0. \end{align*} Hence $\omega_\mu$ is nondegenerate. Since $\omega_\mu$ is smooth, closed, and nondegenerate, it is a symplectic form on $M_\mu$, and the identity $\pi_\mu^*\omega_\mu=i_\mu^*\omega$ holds by construction. [/step]