5.2 Rotation Observables

Definition 16 Momentum maps, comoment maps, and rotation observables

✓

Suppose a Lie algebra \(\mathfrak g\) acts on a phase space \(M\) by infinitesimal symmetries. A momentum map is a map

\[ \mu \colon M \longrightarrow \mathfrak g^* \]

such that pairing with \(\xi \in \mathfrak g\) gives the Hamiltonian for the infinitesimal motion generated by \(\xi \). The associated comoment map is the linear map

\[ \tilde\mu \colon \mathfrak g \longrightarrow C^\infty (M), \qquad \tilde\mu (\xi )(x) = \langle \mu (x), \xi \rangle . \]

Lean uses the comoment because the declarations are scalar observables.

In the Kepler problem we identify \(\mathfrak {so}(3)\) with \(\mathbb {R}^3\) using the cross product. For \(u \in \mathbb {R}^3\), define the scalar functions

\[ L_u = u \cdot L = u \cdot (q \times p), \qquad A_u = u \cdot A. \]

The map \(u \mapsto L_u\) is the rotational comoment built from the angular momentum.

Theorem 17 Rotational comoment

✓

The map \(u \mapsto L_u\) is an \(\mathfrak {so}(3)\)-comoment map. Concretely:

\begin{align*} \{ q_i, L_u\} & = (u \times q)_i, \\ \{ p_i, L_u\} & = (u \times p)_i, \\ \{ L_u, L_v\} & = L_{u \times v}, \\ \{ L_u, H\} & = 0. \end{align*}

Proof ▶

We first identify the infinitesimal motion generated by \(L_u\). Since

\[ L_u = (u \times q) \cdot p, \]

its derivative with respect to \(p_i\) is \((u \times q)_i\). Therefore

\[ \{ q_i, L_u\} = (u \times q)_i. \]

So the Hamiltonian flow of \(L_u\) rotates the position vector about the axis \(u\).

Next rewrite \(L_u\) as

\[ L_u = q \cdot (p \times u). \]

Then

\[ \frac{\partial L_u}{\partial q_i} = (p \times u)_i = -(u \times p)_i, \]

and therefore

\[ \{ p_i, L_u\} = (u \times p)_i. \]

So the same Hamiltonian simultaneously rotates the momentum vector about the same axis.

This proves the infinitesimal symmetry statement. To prove the comoment property, we must show that Poisson brackets of the functions \(L_u\) reproduce the Lie bracket on \(\mathfrak {so}(3)\). Apply the Leibniz rule to \(L = q \times p\):

\[ \{ L_u, L\} = \{ L_u, q\} \times p + q \times \{ L_u, p\} = (u \times q) \times p + q \times (u \times p) = u \times (q \times p) = u \times L. \]

Therefore \(\{ L_u, L_v\} = v \cdot \{ L_u, L\} = v \cdot (u \times L) = (u \times v) \cdot L = L_{u \times v}\). That is exactly the Lie bracket relation for \(\mathfrak {so}(3) \cong \mathbb {R}^3\) with bracket \(u \times v\).

Finally, \(L_u\) is conserved because it generates rotations and the Hamiltonian only depends on the rotation-invariant quantities \(\| p\| ^2\) and \(r = \| q\| \). Indeed,

\[ \{ \| p\| ^2, L_u\} = 2p \cdot (u \times p) = 0, \qquad \{ r, L_u\} = \frac{q}{r} \cdot (u \times q) = 0. \]

Hence \(\{ H, L_u\} = 0\), and by antisymmetry also \(\{ L_u, H\} = 0\).

Theorem 18 Poisson algebra of \(L\) and \(A\)

✓

Away from collision, for all \(u, v \in \mathbb {R}^3\):

\[ \{ L_u, L_v\} = L_{u \times v}, \qquad \{ L_u, A_v\} = A_{u \times v}, \qquad \{ A_u, A_v\} = -2mH\, L_{u \times v}. \]

Both \(L_u\) and \(A_u\) Poisson-commute with \(H\).

Proof ▶

The first identity is Theorem 17. The second follows because \(A\) is built from \(q\) and \(p\) by vector operations that commute with rotations. Since \(L_u\) rotates both \(q\) and \(p\), it also rotates every vector expression built from them. Explicitly, using the same Leibniz argument: \(\{ L_u, A\} = u \times A\), so \(\{ L_u, A_v\} = v \cdot (u \times A) = (u \times v) \cdot A = A_{u \times v}\).

For the third identity, \(\{ A_u, A_v\} = -2mH\, L_{u \times v}\), we expand \(A = F - m\mu U\). The right-hand side still contains the energy function \(H\). Only after restricting to a fixed-energy surface will that coefficient become a constant.

Write \(A = F - m\mu U\) where

\[ F = p \times L, \qquad U = \frac{q}{r}. \]

For constant \(u\), let \(F_u = u \cdot F\) and \(U_u = u \cdot U\). Expand:

\[ \{ A_u, A_v\} = \{ F_u, F_v\} - m\mu \bigl(\{ F_u, U_v\} + \{ U_u, F_v\} \bigr) + (m\mu )^2\{ U_u, U_v\} . \]

So we compute three smaller brackets.

Step 1: \(\{ F_u, F_v\} = -\| p\| ^2 L_{u \times v}\). Write \(F_u = \| p\| ^2 X_u - (q \cdot p) P_u\) where \(X_u = u \cdot q\) and \(P_u = u \cdot p\). From the canonical brackets and the Leibniz rule:

\begin{align*} \{ q \cdot p,\, X_u\} & = -X_u, \qquad \{ q \cdot p,\, P_u\} = P_u, \\ \{ \| p\| ^2,\, X_u\} & = -2P_u, \qquad \{ \| p\| ^2,\, P_u\} = 0. \end{align*}

Expanding \(\{ F_u, F_v\} \) by bilinearity and collecting all terms gives:

\[ \{ F_u, F_v\} = \| p\| ^2(P_u X_v - P_v X_u) = -\| p\| ^2\, L_{u \times v}. \]

Step 2: \(\{ F_u, U_v\} + \{ U_u, F_v\} = -(2/r)\, L_{u \times v}\). Using the Leibniz rule on \(U_v = X_v/r\):

\[ \{ F_u, U_v\} = \frac{\{ F_u, X_v\} }{r} + X_v\{ F_u, r^{-1}\} . \]

Computing \(\{ F_u, X_v\} \) and \(\{ F_u, r\} \) from the Leibniz rule, then adding the antisymmetric term \(\{ U_u, F_v\} \), all remaining terms cancel except:

\[ \{ F_u, U_v\} + \{ U_u, F_v\} = -\frac{2}{r}\, L_{u \times v}. \]

Step 3: \(\{ U_u, U_v\} = 0\). Both \(U_u\) and \(U_v\) depend only on \(q\), so all \(p\)-derivatives vanish and the bracket is zero.

Combining:

\begin{align*} \{ A_u, A_v\} & = -\| p\| ^2 L_{u \times v} + m\mu \cdot \frac{2}{r}\, L_{u \times v} \\ & = -\! \left(\| p\| ^2 - \frac{2m\mu }{r}\right)L_{u \times v} = -2mH\, L_{u \times v}. \end{align*}