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.

Root reflections are induced by inner automorphisms

Statement

Assume the Axiom of Choice. Let α be a root of the finite-dimensional complex semisimple Lie algebra g with respect to a Cartan subalgebra h (Root and root space), let eα,fα,hα be the triple of The root sl2 triple, and let G be a connected simply connected real Lie group with Lie algebra g. Then

τα:=Ad⁡exp⁡G(eα)Ad⁡exp⁡G(−fα)Ad⁡exp⁡G(eα)

is an inner automorphism of g with τα(h)=h, τα(hα)=−hα, τα(x)=x for x∈ker⁡α, and τα(gβ)=gsα(β) for every root β; thus τα induces the reflection sα of Root reflection defined by a coroot on the root system.

Facts & Assumptions

Given: The Axiom of Choice, such g,h, a root α, the triple (eα,fα,hα), and a connected simply connected group G with Lie algebra g.

[A1]

The Axiom of Choice is The Axiom of Choice; it implies the countable choice used by [L3] and [L4] through The Axiom of Countable Choice (ACω).

[L1]

The triple satisfies [eα,fα]=hα, [hα,eα]=2eα, [hα,fα]=−2fα, and α(hα)=2 (The root sl2 triple, Coroot of a Lie-algebra root).

[L2]

The root spaces are the eigenspaces of ad⁡h, [gγ,gδ]⊆gγ+δ, and h=g0=Cg(h) is a maximal toral subalgebra, in particular abelian (Root and root space, Brackets of root spaces, Root-space decomposition, Cartan subalgebras are exactly maximal toral subalgebras, Toral and maximal toral subalgebras).

[L3]

Under countable choice, a connected simply connected real Lie group G with Lie algebra g exists (Lie's third fundamental theorem, The Axiom of Countable Choice (ACω)).

[L4]

Under countable choice, Ad⁡:G→GL⁡(g) is a smooth homomorphism with Ad⁡gh=Ad⁡gAd⁡h, Ad⁡e=I, values in the automorphisms of g, and Ad⁡exp⁡GX=ead⁡X, where etB denotes the unique solution of E′=B∘E, E(0)=I; moreover d(Ad⁡)eX=ad⁡X (Adjoint exponential identity, The differential of Ad is ad, Adjoint is a smooth Lie-group representation, Conjugation and the adjoint representation of a Lie group, The Axiom of Countable Choice (ACω)).

[L5]

Linear initial-value problems have unique solutions (Linear matrix ODEs have unique global solutions on a fixed interval).

Proof

technique · direct
1.1L4L5algebra

First, a vanishing criterion: if X,x∈g satisfy [X,x]=0, then Ad⁡exp⁡GX(x)=x. Indeed the curve t↦Ad⁡exp⁡G(tX) is a homomorphism in t with derivative satisfying U′(t)=ad⁡X∘U(t), by [L4] and the chain rule, and U(0)=I; hence u(t)=U(t)x solves u′=ad⁡Xu with u(0)=x, and so does the constant curve x because [X,x]=0. Uniqueness [L5] gives Ad⁡exp⁡GX(x)=x.

1.2L4L5algebra

Similarly, if ad⁡X is nilpotent and (ad⁡X)n=0, then Ad⁡exp⁡GX=ead⁡X=∑k<n(ad⁡X)kk!. Indeed the polynomial curve E(t)=∑k<ntk(ad⁡X)kk! satisfies E′(t)=ad⁡X∘E(t) and E(0)=I by termwise differentiation. Uniqueness [L5] therefore identifies it with etad⁡X, and setting t=1 gives the displayed formula.

1.3L4algebra

τα is an inner automorphism: by [L4] each factor Ad⁡exp⁡G(±eα), Ad⁡exp⁡G(−fα) is an automorphism of g, and Ad⁡ is multiplicative, so τα=Ad⁡g for g=exp⁡G(eα)exp⁡G(−fα)exp⁡G(eα)∈G.

2.1L1L2step 1.1algebra

If x∈ker⁡α⊆h, then [eα,x]=α(x)eα=0 and [fα,x]=−α(x)fα=0 by [L2], so step 1.1 applied to X=eα,−fα gives τα(x)=x.

2.2L1L5step 1.2algebra

The operator ad⁡eα is nilpotent on Chα⊕Ceα: indeed [eα,hα]=−2eα and [eα,eα]=0 by [L1]; likewise ad⁡−fα is nilpotent on Chα⊕Cfα. Using step 1.2 we compute Ad⁡exp⁡G(eα)(hα)=hα−2eα, then Ad⁡exp⁡G(−fα)(hα−2eα)=−hα−2eα from [−fα,hα]=−2fα and [−fα,eα]=hα, and finally Ad⁡exp⁡G(eα)(−hα−2eα)=−hα; hence τα(hα)=−hα.

3.1A1L1L2step 2.1step 2.2algebra∎

Consequently τα preserves h=ker⁡α⊕Chα: it fixes ker⁡α pointwise by step 2.1 and negates hα by step 2.2. For a root β and x∈gβ, the element τα(x) satisfies [H,τα(x)]=τα([τα−1(H),x])=β(τα−1(H))τα(x) for H∈h; since τα−1∣h=τα∣h is the identity on ker⁡α and negation on hα, the functional H↦β(τα−1(H)) agrees with β on ker⁡α and takes the value −β(hα) at hα, hence equals β−β(hα)α=sα(β) because α(hα)=2 and α vanishes on ker⁡α. Therefore τα(gβ)⊆gsα(β), and since τα is an automorphism and sα is an involution, dimensions agree and equality holds; the Axiom of Choice was used only through [L3] and [L4], that is, through [A1].

Depends on

Used by

Dependency tree · two levels

90 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