Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

A compact-group moment map can be averaged to an equivariant one when the affine obstruction vanishes

Statement

Assume the Axiom of Choice and ACω. Let a compact Lie group G act symplectically on a connected symplectic manifold (M,ω), and suppose that an infinitesimal moment map μ:Mg is supplied, so that its components satisfy dμξ=ιξMω and depend linearly on ξ. Then the Haar average

μˉ(p):=Gg1μ(gp)dμG(g)

is a coadjoint-equivariant moment map for the action. It differs from μ by a constant covector, which need not be coadjoint-fixed unless μ was already equivariant; this constant makes the affine non-equivariance cocycle of μ a coboundary. The averaging uses the supplied component Hamiltonians and does not produce one when none is given: the existence of an infinitesimal moment map remains an assumption, and no component one-form ιξMω is proved exact here.

Facts & Assumptions

Given: the Axiom of Choice, ACω, a compact Lie group acting symplectically on connected (M,ω), and a supplied infinitesimal moment map μ.

[A1]

The Axiom of Choice is The Axiom of Choice and ACω is countable choice.

[A2]

AC provides the normalized Haar measure; ACω is inherited from the fundamental-field interface; the supplied moment map is an assumption, not a consequence of the averaging.

[F1]

G carries a normalized Haar probability measure invariant under left and right translations and inversion, and integrals of integrable functions are invariant under these substitutions. Normalized Haar measure on a compact Lie group, Haar integration is translation and conjugation invariant.

[F2]

μ is an infinitesimal moment map: dμξ=ιξMω for all ξ, and μ(gp) is smooth in (g,p). Moment map, component Hamiltonians and infinitesimal moment maps.

[F3]

Fundamental fields are equivariant: (Adgξ)M(gp)=d(ag)pξM(p), and the action preserves ω. Adjoint intertwines the exponential map, Fundamental vector fields for a left action.

[F4]

Two Hamiltonians for the same vector field differ by a locally constant function, hence by a constant on a connected manifold. Hamiltonians for a fixed vector field differ by a locally constant function.

[F5]

The defect c(ξ,η)={μξ,μη}μ[ξ,η] of an infinitesimal moment map on connected M is constant and is a two-cocycle. Equivariance always implies c=0; the converse for a disconnected group requires the additional component-group condition. The nonequivariance defect of an infinitesimal moment map is a constant Lie-algebra two-cocycle.

Proof

technique · direct
1.1

The integrand (g,p)g1μ(gp) is smooth, being a composition of the smooth action, the smooth coadjoint action and μ; since G is compact, integrating the finitely many components of this g-valued function against the normalized Haar measure defines a smooth map μˉ:Mg.

A2F1F2
1.2

Equivariance: for hG and pM, make the right-translation substitution k=gh, so g=kh1 and g1=hk1. Right invariance of Haar then gives μˉ(hp)=Gh(k1μ(kp))dμG(k)=hμˉ(p). No equivariance of the original infinitesimal moment map is used.

step 1.1F1F2
2.1

Component equations: for fixed gG and ξg, the function pg1μ(gp),ξ=μAdgξ(gp) has differential dμgpAdgξ(d(ag)pv)=ωgp((Adgξ)M(gp),d(ag)pv)=ωp(ξM(p),v) by [F2] and [F3], independently of g. Integrating over G gives dμˉpξ(v)=ωp(ξM(p),v), the component moment equation for μˉ.

step 1.1F2F3
3.1

By step 2.1 the averaged map satisfies the component moment equations, and by step 1.2 it is coadjoint equivariant; hence μˉ is an equivariant moment map for the action.

step 1.2step 2.1
4.1

For each ξ, step 2.1 and [F2] show that μˉξ and μξ are Hamiltonians for the same vector field, so [F4] and connectedness make their difference constant. Linearity in ξ therefore gives a constant covector δ:=μˉμg. Since μˉ is equivariant, its bracket defect vanishes; expanding its defect and using that constants are Poisson-central gives 0=c(ξ,η)δ([ξ,η]). Thus the constant cocycle c of [F5] is the coboundary represented by δ. In general δ need not be coadjoint-fixed, because μ need not be equivariant.

step 2.1step 3.1F2F4F5
5.1

The construction began from the supplied linear family of component Hamiltonians; no step here produces such a family when the closed one-forms ιξMω have no primitives, so averaging trivializes only the affine obstruction of a supplied infinitesimal moment map.

step 4.1A2A1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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