PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Comoment maps act on observables by Poisson derivations

Statement

Let $g$ be a real Lie algebra, let $(M, ω)$ be a symplectic manifold, and let $J : g \to C^{\infty} (M, R)$ be a comoment map as defined in Symplectic comoment maps and Hamiltonian observable actions. Then $ρ_{J} (ξ) F = {J (ξ), F}$ defines a real Lie-algebra representation of $g$ on $C^{\infty} (M, R)$ , and every $ρ_{J} (ξ)$ is a Poisson derivation: for all $F, G \in C^{\infty} (M, R)$ ,

$ρ_{J} (ξ) (F G) = ρ_{J} (ξ) (F) G + F ρ_{J} (ξ) (G),$

$ρ_{J} (ξ) {F, G} = {ρ_{J} (ξ) (F), G} + {F, ρ_{J} (ξ) (G)} .$

In the library Hamiltonian-field convention, the same observable operator is $ρ_{J} (ξ) F = - X_{J (ξ)} (F)$ for every $ξ$ and $F$ .

There is also the following moment-map branch. Assume ${A C}_{ω}$ . If a finite-dimensional real Lie group $G$ acts symplectically on $(M, ω)$ and $μ$ is an equivariant moment map in the library convention, then $J (ξ) = μ^{ξ}$ is a comoment map and $ρ_{J} (ξ) F = ξ_{M} (F)$ . This forward implication needs no connectedness assumption on $G$ . The first assertion for an arbitrary comoment map is choice-free; this branch carries only the countable-choice assumption required by the stated moment-map suppliers.

Facts & Assumptions

Given: A real Lie algebra $g$ , a symplectic manifold $(M, ω)$ , and a real-linear comoment map $J$ ; for the final moment-map branch also ${A C}_{ω}$ , a symplectic left $G$ -action, and an equivariant moment map $μ$ .

[A1]

${A C}_{ω}$ is the Axiom of Countable Choice. It is used only in the moment-map branch, through the cited moment-map suppliers; the general comoment calculation makes no choice. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

A comoment map is real-linear and satisfies $J ([ξ, η]) = {J (ξ), J (η)}$ ; its observable operator is $ρ_{J} (ξ) F = {J (ξ), F}$ . Symplectic comoment maps and Hamiltonian observable actions

[F2]

The symplectic Poisson bracket satisfies the Jacobi identity. The Poisson bracket satisfies the Jacobi identity

[F3]

The bracket is real-bilinear and skew, and is a derivation in each argument. The Poisson bracket is bilinear, skew, and a derivation in each entry

[F4]

The sign convention is ${F, G} = X_{G} (F) = - X_{F} (G)$ , with $ι_{X_{H}} ω = d H$ . Poisson bracket on a symplectic manifold

[F5]

Moment components $μ^{ξ} = ⟨ μ, ξ ⟩$ depend linearly on $ξ$ and satisfy $d μ^{ξ} = - ι_{ξ_{M}} ω$ ; equivariance is an additional condition. Moment map, component Hamiltonians and infinitesimal moment maps

[F6]

For an equivariant moment map, the forward identity ${μ^{ξ}, μ^{η}} = μ^{[ξ, η]}$ holds for every $G$ , without a connectedness assumption. For connected groups, equivariance is equivalent to the moment-map Poisson bracket identity

[F7]

For every moment-map component, $X_{μ^{ξ}} = - ξ_{M}$ . Moment map components generate the negative infinitesimal action

[F8]

A representation of a Lie algebra is a linear Lie-algebra homomorphism to the endomorphism algebra with its commutator. Representations of Lie algebras

Proof

1.1givenF1F3algebra

For $a, b \in R$ and $ξ, η \in g$ , real-linearity of $J$ and bilinearity of the Poisson bracket give $ρ_{J} (a ξ + b η) = a ρ_{J} (ξ) + b ρ_{J} (η)$ ; bilinearity also makes each $ρ_{J} (ξ)$ a real-linear operator on $C^{\infty} (M, R)$ .

1.2givenF1F3

The derivation rule in the second bracket entry gives $ρ_{J} (ξ) (F G) = {J (ξ), F G} = {J (ξ), F} G + F {J (ξ), G}$ , which is the product rule.

1.3givenF1F2F3

Apply Jacobi to $J (ξ), F, G$ and use skew-symmetry to obtain $ρ_{J} (ξ) {F, G} = {J (ξ), {F, G}} = {{J (ξ), F}, G} + {F, {J (ξ), G}}$ , the required Poisson-bracket derivation rule.

1.4givenA1F5F6

In the moment-map branch, [F5] gives linearity of $J (ξ) = μ^{ξ}$ and the component moment equations, while equivariance and [F6] give ${μ^{ξ}, μ^{η}} = μ^{[ξ, η]}$ . Thus these components satisfy the comoment definition. This use of [F6] requires [A1], but does not require that $G$ be connected.

2.1givenF1F2F3F8step 1.1algebra

For every $F \in C^{\infty} (M, R)$ , Jacobi and skew-symmetry give $[ρ_{J} (ξ), ρ_{J} (η)] F = {J (ξ), {J (η), F}} - {J (η), {J (ξ), F}} = {{J (ξ), J (η)}, F} = {J ([ξ, η]), F} = ρ_{J} ([ξ, η]) F$ . Together with step 1.1, this is the representation condition in [F8].

3.1givenA1F1F4F7step 1.4∎

For any comoment map, [F1] and [F4] give $ρ_{J} (ξ) F = {J (ξ), F} = - X_{J (ξ)} (F)$ , with no choice assumption. In the moment-map branch of step 1.4, substitute $J (ξ) = μ^{ξ}$ ; under [A1], [F7] changes $- X_{μ^{ξ}} (F)$ to $ξ_{M} (F)$ . This proves both the general Hamiltonian-field sign and the stated moment-map action on observables.

Depends on

Used by

Quadratic sl2 comoment action on the symplectic plane Example

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)
Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)