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 .
Let be a finite-dimensional real Lie group with Lie algebra and dual (Linear functionals and the algebraic dual ). For the coadjoint map is the linear map
so that for every . The coadjoint action of on is
The family , , is the coadjoint representation. The coadjoint orbit of and its coadjoint stabilizer are the orbit and stabilizer, in the sense of Orbits, stabilizers, and orbit maps of smooth actions, of this action:
The maps are invertible, with : composing gives , and because is a group homomorphism (Adjoint is a smooth Lie-group representation), which identifies the composite with . Hence
so the coadjoint action is a left action; the inverse in the definition is exactly what makes it left rather than right. The action is jointly smooth. Indeed, in a fixed basis of and its dual, the matrix of is the transpose of the matrix of ; the matrix entries of are smooth because is a smooth representation and inversion in is smooth (Lie group), and the coordinates of 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 at gives the infinitesimal formula
for the fundamental vector field of Fundamental vector fields for a left action: the derivative of is (Adjoint exponential identity), and . 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 convention, but of no further structure, is involved; the coadjoint action applies verbatim to disconnected , to , whose orbit is the singleton , and to abelian , where it is trivial.
Here 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
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Conjugation and the adjoint representation of a Lie group
- Adjoint is a smooth Lie-group representation
- Linear functionals and the algebraic dual $V^*=\mathcal L(V,F)$
- Smooth left actions of Lie groups
- Orbits, stabilizers, and orbit maps of smooth actions
- Lie group
- Fundamental vector fields for a left action
- Adjoint exponential identity
Used by
- Semisimple Hamiltonian actions have a unique equivariant moment map when one exists Corollary
- Zero-level symplectic reduction and the dimension formula Corollary
- Moment map, component Hamiltonians and infinitesimal moment maps Definition
- Symplectic and Hamiltonian Lie-group actions Definition
- The Kirillov--Kostant--Souriau form on a coadjoint orbit Definition
- Angular momentum as the moment map for rotations of a cotangent bundle Example
- Circle rotation on complex n-space and its quadratic moment map Example
- Grassmannians from unitary symplectic reduction Example
- The two-sphere as a coadjoint orbit of SO(3) Example
- An infinitesimal moment map is automatically equivariant False statement
- Moment maps are unique without normalization False statement
- The general reduced dimension is dim M minus two dim G False statement
- The KKS formula is independent of the Lie-algebra representatives Lemma
- Equivariant symplectomorphisms preserve moment maps up to a coadjoint-fixed covector Proposition
- For connected groups, equivariance is equivalent to the moment-map Poisson bracket identity Proposition
- Moment maps for one action form an affine space over coadjoint-fixed covectors Proposition
- Reduction commutes with products Proposition
- The coadjoint-orbit inclusion is an equivariant moment map Proposition
- The dimension of a regular reduced space at a nonzero value Proposition
- The moment level is invariant under the coadjoint stabilizer Proposition
- The shifting trick identifies reduction at a value with a zero reduction Proposition
- Coadjoint orbits are symplectic manifolds Theorem
- Reduction in stages for free proper regular actions Theorem
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
- Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)
- Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)