Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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 ACω. For a smooth left action of G on M, with the standing convention

XM(x)=ddt0exp(tX)x,

one has

[XM,YM]=[X,Y]M.

Thus XXM is a Lie-algebra homomorphism.

Facts & Assumptions

Given: ACω, a smooth left action of a finite-dimensional real Lie group G on a smooth manifold M, and X,Yg.

[A1]

The fundamental-field convention uses exp(tX) and gives smooth vector fields. The Axiom of Countable Choice (ACω), Fundamental vector fields for a left action.

[F1]

Pushforward by a diffeomorphism transports a smooth vector field by its differential. Pushforwards and pullbacks of vector fields by a diffeomorphism.

[F2]

The inverse-time-flow definition of the Lie derivative satisfies LUV=[U,V]. The Lie derivative of a vector field, The Lie derivative of a vector field equals the Lie bracket.

[F3]

The identity differential of the group adjoint representation is ad, so ddt0Adexp(tX)Y=[X,Y]. The differential of Ad is ad.

[F4]

Conjugation intertwines the exponential map: gexpG(Z)g1=expG(AdgZ) for every gG and Zg. Adjoint intertwines the exponential map.

Proof

technique · differentiate the equivariance of fundamental fields along their action flows
1.1

For pM, write ap(g)=gp. Since the identity differential of the exponential is the identity, XM(p)=d(ap)eX, so XXM is linear. The curve Φt(p)=exp(tX)p has velocity XM at every time, because exp((t+s)X)=exp(sX)exp(tX); hence Φ is the global flow of XM.

A1algebra
2.1

For fixed gG, [F4] gives gexp(tY)g1=exp(tAdgY); differentiating this identity in its action on gp gives (g)YM=(AdgY)M. Apply this with g=exp(tX), which acts as Φt by step 1.1, to obtain (Φt)YM=(Adexp(tX)Y)M.

A1F1F4step 1.1algebra
3.1

By [F2], the derivative at t=0 of the left side in step 2.1 is LXMYM=[XM,YM]. By [F3] and linearity from step 1.1, the derivative of the right side is (adXY)M=[X,Y]M. 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].

A1F1F2F3F4step 1.1step 2.1

Depends on

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