Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Poisson Algebras, Symplectic Brackets, and Hamiltonian Actions: Examples and Counterexamples

1 · Prerequisites

2 · Summary

This companion includes the newly computed quadratic ${s l}_{2} (R)$ comoment action and routes readers to existing canonical computations and boundary examples. The new carrier is homed here; the older linked items retain their existing homes and proofs.

Companion: poisson-algebras-and-hamiltonian-representations.

Worked computations

Quadratic sl2 comoment action on the symplectic plane defines the real traceless-matrix Lie algebra explicitly, verifies its quadratic comoment map and observable brackets, and checks the induced commutators on an arbitrary smooth function.
Poisson brackets in canonical coordinates computes the canonical brackets ${q^{i}, q^{j}} = 0$ , ${p_{i}, p_{j}} = 0$ , and ${q^{i}, p_{j}} = δ_{j}^{i}$ from the library coordinate formula.
Circle rotation on complex n-space and its quadratic moment map checks the component moment equation for scalar circle rotation on $C^{n}$ and obtains the sign-sensitive moment map $μ (z) = - \frac{1}{2} ∣ z ∣^{2} + c$ in the library fundamental-field convention.
Angular momentum as the moment map for rotations of a cotangent bundle derives $μ (q, p) = q \times p$ for the cotangent lift of the $S O (3)$ action on $R^{3}$ and checks equivariance under the coadjoint action.

Failure cases and boundary conditions

An infinitesimal moment map is automatically equivariant refutes the claim that the component moment equations alone force equivariance: the counterexample uses translations of $R^{2}$ with an abelian group and a nonconstant infinitesimal moment map.
Every symplectic action is Hamiltonian refutes the claim that every symplectic action admits a moment map: the translation action on the symplectic torus would require a global primitive of $d y$ , but that one-form has nonzero period.

These carriers supply their own hypotheses, sign conventions, calculations, and proofs. In particular, the examples do not remove the connected-group condition in For connected groups, equivariance is equivalent to the moment-map Poisson bracket identity or the distinction between a symplectic action and a Hamiltonian action.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Quadratic sl2 comoment action on the symplectic plane

Example

Let $M = R^{2}$ with coordinates $(q, p)$ and $ω = d q \land d p$ . Let $g = {s l}_{2} (R) = {(\begin{array}{cc} a & b \\ c & - a \end{array}) : a, b, c \in R}$ with bracket $[A, B] = A B - B A$ . Use the basis $H = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ , $E = (\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array})$ , and $F = (\begin{array}{cc} 0 & 0 \\ 1 & 0 \end{array})$ . Define the real-linear map $J : g \to C^{\infty} (M, R)$ by

$J (H) = - q p, J (E) = \frac{q^{2}}{2}, J (F) = - \frac{p^{2}}{2} .$

Write $\partial_{q}$ and $\partial_{p}$ for the coordinate derivative operators. Then $J$ is a comoment map under Symplectic comoment maps and Hamiltonian observable actions, and its observable operators are

$ρ_{J} (H) = q \partial_{q} - p \partial_{p}, ρ_{J} (E) = q \partial_{p}, ρ_{J} (F) = p \partial_{q} .$

These operators give the real three-dimensional matrix Lie algebra its observable representation. By Comoment maps act on observables by Poisson derivations, they preserve both pointwise multiplication and the Poisson bracket on all smooth functions; the Verification also checks the commutators on an arbitrary smooth test function and gives explicit product and bracket-preservation calculations.

Facts & Assumptions

Given: The standard symplectic plane $(R^{2}, d q \land d p)$ , the real traceless $2 \times 2$ matrices with the commutator bracket, the displayed basis, and the map $J$ in the Example. Assume ${A C}_{ω}$ only when applying the coordinate-formula supplier.

[A1]

${A C}_{ω}$ is the Axiom of Countable Choice; it is the sole choice assumption used by the coordinate-formula supplier. No arbitrary-index choice is used here. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

A symplectic form is closed and restricts to a nondegenerate alternating form on every tangent space. Symplectic form and symplectic manifold

[F2]

A finite-dimensional real symplectic vector space has an alternating bilinear form whose map to the dual is an isomorphism; equivalently, only the zero vector pairs to zero with every vector. Symplectic vector space

[F3]

For a real vector space $V$ , ${End}_{R} (V)$ has the commutator Lie bracket, and a Lie-algebra representation is a bracket-preserving linear map into it. Representations of Lie algebras

[F4]

A real Lie algebra has a bilinear alternating bracket satisfying Jacobi. Lie algebras over a field

[F5]

In canonical $(q, p)$ coordinates and under ${A C}_{ω}$ , ${A, B} = A_{q} B_{p} - A_{p} B_{q}$ . Coordinate formula for the Poisson bracket

[F6]

The comoment identity and observable action are $J ([ξ, η]) = {J (ξ), J (η)}$ and $ρ_{J} (ξ) A = {J (ξ), A}$ . Symplectic comoment maps and Hamiltonian observable actions

[F7]

A comoment map defines a Lie-algebra representation on functions, and each operator is a Poisson derivation. Comoment maps act on observables by Poisson derivations

Verification

1.1givenF1F2algebra

The form $ω = d q \land d p$ is smooth and alternating, and $d ω = 0$ because $d (d q) = d (d p) = 0$ . For $v = a \partial_{q} + b \partial_{p}$ , $ι_{v} ω = a d p - b d q$ ; if this is zero, then $a = b = 0$ . Thus $ω$ is nondegenerate at every point and is symplectic by [F1]–[F2].

1.2givenF3F4algebra

Every real traceless matrix is uniquely $a H + b E + c F$ , so $(H, E, F)$ is a basis of the stated vector space. Matrix multiplication gives $H E = E$ , $E H = - E$ , $H F = - F$ , $F H = F$ , $E F = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ , and $F E = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array})$ . Consequently $[H, E] = 2 E$ , $[H, F] = - 2 F$ , and $[E, F] = H$ ; the span is closed under commutators. The ambient endomorphism algebra has the commutator Lie bracket by [F3], and the closed subspace therefore inherits its bilinearity, alternation, and Jacobi identity by [F4]. This verifies the stated ${s l}_{2} (R)$ convention without identifying it with the library's complex ${s l}_{2} (C)$ .

1.3givenA1F4F5F6algebra

Differentiating the three quadratic functions gives $(\partial_{q} J (H), \partial_{p} J (H)) = (- p, - q)$ , $(\partial_{q} J (E), \partial_{p} J (E)) = (q, 0)$ , and $(\partial_{q} J (F), \partial_{p} J (F)) = (0, - p)$ . By [F5], ${J (H), J (E)} = q^{2} = 2 J (E) = J ([H, E])$ , ${J (H), J (F)} = p^{2} = - 2 J (F) = J ([H, F])$ , and ${J (E), J (F)} = - q p = J (H) = J ([E, F])$ . The matrix bracket is alternating by [F4], and swapping the inputs in the coordinate formula [F5] negates the Poisson bracket; both are bilinear. Since $(H, E, F)$ is a basis, these three pairs, their reversals, and the zero diagonal pairs establish the comoment identity for every $ξ, η \in g$ .

1.4givenA1F5F6F7algebra

Applying [F5] to arbitrary $u \in C^{\infty} (R^{2}, R)$ gives $ρ_{J} (H) u = q u_{q} - p u_{p}$ , $ρ_{J} (E) u = q u_{p}$ , and $ρ_{J} (F) u = p u_{q}$ . The result in [F7] supplies the two Poisson-derivation identities for every pair of smooth functions.

2.1givenstep 1.2algebra

Write $u_{q p} = \partial_{q} \partial_{p} u$ and $u_{p q} = \partial_{p} \partial_{q} u$ ; for smooth $u$ these are equal. Direct composition gives $[ρ_{J} (H), ρ_{J} (E)] u = (q u_{p} + q^{2} u_{q p} - p q u_{p p}) - (q^{2} u_{p q} - q u_{p} - p q u_{p p}) = 2 q u_{p} = 2 ρ_{J} (E) u$ , $[ρ_{J} (H), ρ_{J} (F)] u = (p q u_{q q} - p u_{q} - p^{2} u_{q p}) - (p u_{q} + p q u_{q q} - p^{2} u_{p q}) = - 2 p u_{q} = - 2 ρ_{J} (F) u$ , and $[ρ_{J} (E), ρ_{J} (F)] u = (q u_{q} + p q u_{q p}) - (p u_{p} + p q u_{p q}) = q u_{q} - p u_{p} = ρ_{J} (H) u$ . These are exactly the three matrix brackets from step 1.2; bilinearity extends them from basis elements to all of $g$ .

2.2givenA1F5step 1.4algebra

For $u = p$ and $v = q + p$ , $ρ_{J} (E) (u v) = q \partial_{p} (p (q + p)) = q (q + 2 p) = q^{2} + 2 p q$ , while $ρ_{J} (E) (u) v + u ρ_{J} (E) (v) = q (q + p) + p q = q^{2} + 2 p q$ . Thus the product rule is directly verified on this nontrivial pair.

3.1givenA1F5F7step 1.4algebra∎

For $u = q^{2} / 2$ and $v = p^{2} / 2$ , the coordinate bracket gives ${u, v} = q p$ , so $ρ_{J} (H) {u, v} = 0$ . Also $ρ_{J} (H) u = q^{2}$ and $ρ_{J} (H) v = - p^{2}$ , whence ${ρ_{J} (H) u, v} + {u, ρ_{J} (H) v} = {q^{2}, p^{2} / 2} + {q^{2} / 2, - p^{2}} = 2 q p - 2 q p = 0$ . This checks bracket preservation directly on a nonconstant pair, while [F7] establishes it for all smooth functions.