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.
Fundamental vector fields form a Lie-algebra homomorphism
Statement
Assume . For a smooth left action of on , with the standing convention
one has
Thus is a Lie-algebra homomorphism.
Facts & Assumptions
Given: , a smooth left action of a finite-dimensional real Lie group on a smooth manifold , and .
The fundamental-field convention uses and gives smooth vector fields. The Axiom of Countable Choice (), Fundamental vector fields for a left action.
Pushforward by a diffeomorphism transports a smooth vector field by its differential. Pushforwards and pullbacks of vector fields by a diffeomorphism.
The inverse-time-flow definition of the Lie derivative satisfies . The Lie derivative of a vector field, The Lie derivative of a vector field equals the Lie bracket.
The identity differential of the group adjoint representation is , so . The differential of Ad is ad.
Conjugation intertwines the exponential map: for every and . Adjoint intertwines the exponential map.
Proof
For , write . Since the identity differential of the exponential is the identity, , so is linear. The curve has velocity at every time, because ; hence is the global flow of .
For fixed , [F4] gives ; differentiating this identity in its action on gives . Apply this with , which acts as by step 1.1, to obtain .
By [F2], the derivative at of the left side in step 2.1 is . By [F3] and linearity from step 1.1, the derivative of the right side is . This proves the formula. The action need not be effective, free, or transitive; if either vector is zero or the group is zero-dimensional, both sides vanish. All flows used are global, so there is no endpoint issue. Countable choice is inherited exactly through [A1], [F1], [F3], and [F4].
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Fundamental vector fields for a left action
- Pushforwards and pullbacks of vector fields by a diffeomorphism
- The Lie derivative of a vector field
- The Lie derivative of a vector field equals the Lie bracket
- The differential of Ad is ad
- Adjoint intertwines the exponential map
Used by
Dependency tree · two levels
33 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
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)
- Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I (standard reference, not scraped)