Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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 ACω. Let a symplectic left action of G on a symplectic manifold (M,ω) be given, and let μ:Mg satisfy the component moment equations dμξ=ιξMω for every ξg.

  1. If μ is coadjoint equivariant, then {μξ,μη}=μ[ξ,η] on all of M for all ξ,ηg.
  2. Conversely, if G is connected and {μξ,μη}=μ[ξ,η] on all of M for all ξ,η, then μ is coadjoint equivariant.

Thus, for connected G and connected M, 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 G0, and equivariance under all of G requires in addition equivariance under one representative of each coset of G/G0. Connectivity of M 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 M by the companion lemma below.

Facts & Assumptions

Given: ACω, a symplectic action of G on (M,ω), and a map μ:Mg satisfying the component moment equations.

[A1]

ACω is countable choice; it is used only through the fundamental-field and exponential interfaces cited in [F1]--[F7], and no further choice is made.

[F1]

The component moment equations read dμξ=ιξMω. Moment map, component Hamiltonians and infinitesimal moment maps.

[F2]

Xμξ=ξM for every ξ. Moment map components generate the negative infinitesimal action.

[F3]

{F,G}=ω(XF,XG) and the Poisson bracket is bilinear and alternating, so ω(ξM,ηM)={μξ,μη} by [F2]. Poisson bracket on a symplectic manifold.

[F4]

The coadjoint action is (gα)(ζ)=α(Adg1ζ), and ddt0expG(tξ)α,ζ=α,[ξ,ζ]. The coadjoint representation, action and orbits.

[F5]

ddt0AdexpG(tξ)ζ=[ξ,ζ], and Adg[ξ,ζ]=[Adgξ,Adgζ]. The differential of Ad is ad, Adjoint is a smooth Lie-group representation.

[F6]

expG(Adgζ)=gexpG(ζ)g1. Consequently hexpG(sξ0)=expG(sAdhξ0)h and dds0expG(sζ)x=ζM(x) for the library fundamental field. Adjoint intertwines the exponential map, Fundamental vector fields for a left action.

[F7]

The image of expG contains an open neighborhood of e, 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 X, and every continuous map to the two-point discrete space is constant.

[F8]

A curve in Rn solving a linear ODE v(s)=B(s)v(s) 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

technique · direct
1.1

Fix ξ,ζg and pM. By the moment equation for ζ, the identity Xμζ=ζM and the Poisson convention, dμpζ(ξM(p))=ωp(ζM(p),ξM(p))=ωp(ξM(p),ζM(p))={μξ,μζ}(p).

F1F2F3
1.2

Assume conversely that G is connected and that the bracket identity holds on all of M. Fix mM and define u:Gg by u(g):=μ(gm)gμ(m), the equivariance defect at m. Then u is smooth and u(e)=0, and equivariance of μ is exactly the assertion u0.

givenF4
1.3

Fix hG and ξ0,ξg, and put Θ:=[ξ0,Adh1ξ]. By [F6], hexpG(sξ0)=expG(sAdhξ0)h and therefore the curve shexpG(sξ0)m has velocity (Adhξ0)M(hm) at s=0; hence dds0μξ(hexpG(sξ0)m)=ωhm(ξM,(Adhξ0)M)={μξ,μAdhξ0}(hm)=μ[ξ,Adhξ0](hm), using the moment equation, [F3] and the bracket identity.

F1F3F6given
2.1

Assume μ is equivariant, and fix ξ,ζ,p. For all real t, equivariance and [F4] give μζ(expG(tξ)p)=expG(tξ)μ(p),ζ=μ(p),AdexpG(tξ)ζ. The t-derivative of the left side at 0 is dμpζ(ξM(p)), because texpG(tξ)p has velocity ξM(p) at t=0, and step 1.1 identifies it with {μξ,μζ}(p). The t-derivative of the right side at 0 is μ(p),[ξ,ζ]=μ[ξ,ζ](p) by [F5]. Since ξ,ζ,p were arbitrary, claim 1 holds.

step 1.1F4F5given
2.2

With the same h,ξ0,ξ as in step 1.3, the second term of u contributes dds0μ(m),Ad(hexpG(sξ0))1ξ=μ(m),[ξ0,Adh1ξ]=μ(m),Θ by [F5]. Since [ξ,Adhξ0]=Adh[Adh1ξ,ξ0]=AdhΘ, step 1.3 can be rewritten as μ[ξ,Adhξ0](hm)=μ(hm),AdhΘ, and the identity hμ(m),AdhΘ=μ(m),Θ gives dds0u(hexpG(sξ0)),ξ=μ(hm),AdhΘ+μ(m),Θ=u(h),AdhΘ.

step 1.3F4F5
3.1

Fix ξ0g and consider v(s):=u(expG(sξ0)) as a curve in the finite-dimensional space g, with v(0)=u(e)=0 by step 1.2. For each fixed ξ, step 2.2 applied with h=expG(sξ0) expresses ddsv(s),ξ as a linear functional of v(s) with smooth coefficients, so v solves a linear ODE with continuous coefficients on every compact interval; by [F8] and v(0)=0 the curve v vanishes identically. Hence u vanishes on the whole exponential image expG(g).

step 1.2step 2.2F8
4.1

If u(h)=0 for some hG, then the same argument applied to the curve su(hexpG(sξ0)) shows u(hexpG(g))={0}: the defect curve solves the same linear ODE and vanishes at s=0. The exponential image contains an open neighborhood U of e by [F7], is closed under inversion because ξ runs through g with ξ, and the subgroup H generated by U is open (a union of translates of U) and closed (its complement is a union of cosets, each open). Since G is connected, H=G by [F7]. Every element of G is therefore a finite product of elements of expG(g), and induction over the factors using the vanishing statement proves u0. Thus μ is coadjoint equivariant, which is claim 2.

step 3.1F7
5.1

Finally let G be arbitrary and let G0 be its identity component, a connected Lie group with Lie algebra g and the same fundamental vector fields on M. Claims 1 and 2 applied with G replaced by G0 show that the bracket identity is equivalent to equivariance under G0. Writing each gG as g=gcg0 with gc a representative of gG0 and g0G0, equivariance under all of G is equivalent to equivariance under G0 together with μ(gcm)=gcμ(m) for all representatives gc and all mM.

step 2.1step 4.1A1

Depends on

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