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.
For connected groups, equivariance is equivalent to the moment-map Poisson bracket identity
Statement
Assume . Let a symplectic left action of on a symplectic manifold be given, and let satisfy the component moment equations for every .
- If is coadjoint equivariant, then on all of for all .
- Conversely, if is connected and on all of for all , then is coadjoint equivariant.
Thus, for connected and connected , coadjoint equivariance of a map satisfying the component moment equations is equivalent to the moment-map Poisson bracket identity. For a general group the bracket identity is equivalent to equivariance under the identity component , and equivariance under all of requires in addition equivariance under one representative of each coset of . Connectivity of is not used by either implication; it is used only when the bracket identity is to be checked at a single point, because the nonequivariance defect is then constant on by the companion lemma below.
Facts & Assumptions
Given: , a symplectic action of on , and a map satisfying the component moment equations.
is countable choice; it is used only through the fundamental-field and exponential interfaces cited in [F1]--[F7], and no further choice is made.
The component moment equations read . Moment map, component Hamiltonians and infinitesimal moment maps.
and the Poisson bracket is bilinear and alternating, so by [F2]. Poisson bracket on a symplectic manifold.
The coadjoint action is , and . The coadjoint representation, action and orbits.
. Consequently and for the library fundamental field. Adjoint intertwines the exponential map, Fundamental vector fields for a left action.
The image of contains an open neighborhood of , and a subgroup containing an open neighborhood of the identity is open and closed; a connected space has no clopen subsets other than and itself. The exponential map is a local diffeomorphism at zero, For a topological space the following agree: no separation exists, the only clopen subsets are and , and every continuous map to the two-point discrete space is constant.
A curve in solving a linear ODE with continuous coefficients and vanishing at one point is identically zero on its interval. The Grönwall estimate for two solutions of a Lipschitz ODE.
Proof
Fix and . By the moment equation for , the identity and the Poisson convention,
Assume conversely that is connected and that the bracket identity holds on all of . Fix and define by , the equivariance defect at . Then is smooth and , and equivariance of is exactly the assertion .
Fix and , and put . By [F6], and therefore the curve has velocity at ; hence using the moment equation, [F3] and the bracket identity.
Assume is equivariant, and fix . For all real , equivariance and [F4] give The -derivative of the left side at is , because has velocity at , and step 1.1 identifies it with . The -derivative of the right side at is by [F5]. Since were arbitrary, claim 1 holds.
With the same as in step 1.3, the second term of contributes by [F5]. Since , step 1.3 can be rewritten as , and the identity gives
Fix and consider as a curve in the finite-dimensional space , with by step 1.2. For each fixed , step 2.2 applied with expresses as a linear functional of with smooth coefficients, so solves a linear ODE with continuous coefficients on every compact interval; by [F8] and the curve vanishes identically. Hence vanishes on the whole exponential image .
If for some , then the same argument applied to the curve shows : the defect curve solves the same linear ODE and vanishes at . The exponential image contains an open neighborhood of by [F7], is closed under inversion because runs through with , and the subgroup generated by is open (a union of translates of ) and closed (its complement is a union of cosets, each open). Since is connected, by [F7]. Every element of is therefore a finite product of elements of , and induction over the factors using the vanishing statement proves . Thus is coadjoint equivariant, which is claim 2.
Finally let be arbitrary and let be its identity component, a connected Lie group with Lie algebra and the same fundamental vector fields on . Claims 1 and 2 applied with replaced by show that the bracket identity is equivalent to equivariance under . Writing each as with a representative of and , equivariance under all of is equivalent to equivariance under together with for all representatives and all .
Depends on
- Moment map, component Hamiltonians and infinitesimal moment maps
- Moment map components generate the negative infinitesimal action
- Poisson bracket on a symplectic manifold
- Adjoint intertwines the exponential map
- Adjoint is a smooth Lie-group representation
- The differential of Ad is ad
- The coadjoint representation, action and orbits
- Symplectic and Hamiltonian Lie-group actions
- The exponential map is a local diffeomorphism at zero
- The Grönwall estimate for two solutions of a Lipschitz ODE
- For a topological space the following agree: no separation exists, the only clopen subsets are $\varnothing$ and $X$, and every continuous map to the two-point discrete space is constant
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Fundamental vector fields for a left action
Used by
Dependency tree · two levels
54 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
- Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)
- Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)