Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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.

The coadjoint representation, action and orbits

Definition

Assume ACω.

Let G be a finite-dimensional real Lie group with Lie algebra g=TeG and dual g=L(g,R) (Linear functionals and the algebraic dual V=L(V,F)). For gG the coadjoint map is the linear map

Adg:gg,Adgα:=αAdg1,

so that Adgα,ξ=α,Adg1ξ for every ξg. The coadjoint action of G on g is

G×gg,(g,α)gα:=Adgα.

The family Ad:GGL(g), gAdg, is the coadjoint representation. The coadjoint orbit of αg and its coadjoint stabilizer are the orbit and stabilizer, in the sense of Orbits, stabilizers, and orbit maps of smooth actions, of this action:

Gα={Adgα:gG},Gα={gG:Adgα=α}.

The maps Adg are invertible, with (Adg)1=Adg1: composing AdgAdh gives ααAdh1Adg1, and Adh1Adg1=Adh1g1 because Ad is a group homomorphism (Adjoint is a smooth Lie-group representation), which identifies the composite with Adgh. Hence

Adgh=AdgAdh,Ade=idg,

so the coadjoint action is a left action; the inverse g1 in the definition is exactly what makes it left rather than right. The action is jointly smooth. Indeed, in a fixed basis of g and its dual, the matrix of Adg is the transpose of the matrix of Adg1; the matrix entries of gAdg1 are smooth because Ad is a smooth representation and inversion in G is smooth (Lie group), and the coordinates of (g,α)αAdg1 are these smooth matrix entries paired with the coordinates of α (Conjugation and the adjoint representation of a Lie group). Thus the coadjoint action is a smooth left action in the sense of Smooth left actions of Lie groups, and the orbit and stabilizer above are those of a smooth action.

Differentiating the curve texpG(tξ)α at t=0 gives the infinitesimal formula

ξg(α)(η)=ddt0expG(tξ)α,η=α([ξ,η]),ηg,

for the fundamental vector field ξg(α)=ddt0expG(tξ)α of Fundamental vector fields for a left action: the derivative of AdexpG(tξ)=etadξ is adξ (Adjoint exponential identity), and adξη=[ξ,η]. Equivalently (ξα)(η)=α([η,ξ]) if one writes the infinitesimal coadjoint action, but the formulation above is the one used in this library. A definition of the dual spaces, of the adjoint representation, of orbits and of the exp(tξ) convention, but of no further structure, is involved; the coadjoint action applies verbatim to disconnected G, to α=0, whose orbit is the singleton {0}, and to abelian G, where it is trivial.

Here ACω is countable choice and is used only through the supplied fundamental-vector-field convention and the adjoint-exponential identity; no further choice is made in this definition.

Depends on

Used by

Dependency tree · two levels

37 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