Cotangent reduction for a principal bundle at zero

Freeness makes the stabilizer trivial, so $j_q$ is injective by [F5]. Since $b$ is constant along orbits, $\mathrm{im}{j}_q\subseteq \ker d{b}_q$. Both spaces have dimension $\dim G$ by injectivity and the quotient dimension/submersion assertion in [F2], so they are equal. By [F1], $\mu (q,p)=0$ exactly when $p$ annihilates $\mathrm{im}{j}_q=\ker d{b}_q$.

On vertical fibre variations $\delta p\in T_q^{\ast }Q$, the derivative of $\mu$ is $(d\mu {)}_{(q,p)}(0,\delta p)=-\delta p\circ j_q$. This is surjective onto ${\mathfrak{g}}^{\ast }$: a linear functional on $j_q(\mathfrak{g})$ extends to $T_{q}Q$ by completing a finite basis. Thus $\mu$ is a submersion everywhere, and zero is a regular value. Equivariance in [F1] makes $Z$ invariant, since every linear coadjoint map fixes zero. The assumed free proper lifted action restricts to a free proper action on $Z$: $Z$ is closed as the inverse image of zero, and the action-map preimage of a compact subset of $Z\times Z$ is the same compact preimage as in $T^{\ast }Q\times T^{\ast }Q$. Consequently [F4] supplies $Z\mathrm{/}G$ and its reduced form; its quotient map $\pi :Z\to Z\mathrm{/}G$ is a surjective submersion by [F2].

At $(q,p)\in Z$, surjectivity of $d{b}_q$ and the annihilator description in step 1.1 give a unique $\beta \in T_{b(q)}^{\ast }B$ with $p=(d{b}_q{)}^{\ast }\beta$: define $\beta (v)=p(\tilde{v})$ for any lift, independent of the lift because their difference lies in $\ker d{b}_q$. Define $\mathrm{\Psi }(q,p)=(b(q),\beta )$. It is smooth: in submersion coordinates $b(x,y)=x$, covectors in $Z$ have precisely the form $(p_x,0)$, and $\mathrm{\Psi }(x,y,p_x,0)=(x,p_x)$. Since $b\circ a_g=b$, the cotangent lift transports $(d{b}_q{)}^{\ast }\beta$ to $(d{b}_{gq}{)}^{\ast }\beta$. Thus $\mathrm{\Psi }$ is invariant, onto, and its fibres are exactly the $G$-orbits: representatives of the same point of $B$ differ by the action, and the pullback covector at each representative is unique.

The induced map $\bar{\mathrm{\Psi }}:Z\mathrm{/}G\to T^{\ast }B$ is therefore bijective. It is smooth, since local sections of $\pi$ express it locally as $\mathrm{\Psi }$ composed with a smooth section. To see its inverse is smooth, let $s:U\to Q$ be a local section of $b$ supplied by [F2]. On $T^{\ast }U$, the inverse is $(x,\beta )\mapsto \pi (s(x),(d{b}_{s(x)}{)}^{\ast }\beta )$, a smooth expression which lands in $Z$ by step 1.1. Smoothness into $Z$ also follows from the submersion covector coordinates of step 2.2. These expressions cover the target and agree by uniqueness of the orbit, proving that $\bar{\mathrm{\Psi }}$ is a diffeomorphism.

For $z=(q,p)\in Z$ and $v\in T_{z}Z$, put $\mathrm{\Psi }(z)=(b(q),\beta )$. The correctly typed projection identity is ${\tau }_B\circ \mathrm{\Psi }=b\circ {\tau }_Q\circ \iota$. Therefore $({\mathrm{\Psi }}^{\ast }{\lambda }_B{)}_z(v)=\beta (d{b}_{q}d({\tau }_Q\circ \iota {)}_{z}v)=p(d({\tau }_Q\circ \iota {)}_{z}v)=({\iota }^{\ast }{\lambda }_Q{)}_z(v)\mathrm{.}$ Here $p=(d{b}_q{)}^{\ast }\beta$ by step 2.2, and the tangent vector is a tangent to the level, the domain of $\mathrm{\Psi }$. Applying $-d$ gives ${\mathrm{\Psi }}^{\ast }{\omega }_B={\iota }^{\ast }{\omega }_Q$.

Since $\mathrm{\Psi }=\bar{\mathrm{\Psi }}\circ \pi$, steps 2.1 and 4.1 give ${\pi }^{\ast }({\bar{\mathrm{\Psi }}}^{\ast }{\omega }_B)={\pi }^{\ast }{\omega }^{\mathrm{r}\mathrm{e}\mathrm{d}}$. Pullback by a surjective submersion is injective on forms: at each base point, choose a point above it and lift every finite tuple of tangent vectors by the surjective differential to evaluate the form. Hence ${\bar{\mathrm{\Psi }}}^{\ast }{\omega }_B={\omega }^{\mathrm{r}\mathrm{e}\mathrm{d}}$, proving the canonical symplectomorphism. If $Q$ is empty both spaces are empty. If $G$ is trivial the construction is the identity; if $\dim G=0$ the derivative surjectivity onto its zero-dimensional dual is vacuous and the same descent works. Zero covectors cause no exception. No connection or choice of horizontal distribution enters the map, and the local sections used to prove smoothness do not enter its definition.