Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Lie algebra of the automorphism group

Statement

Assume countable choice. For a finite-dimensional real or complex semisimple Lie algebra g, the group Aut⁡(g) is a closed Lie subgroup of GL⁡(g) and

Lie⁡(Aut⁡(g))=Der⁡(g)=ad⁡(g).

Facts & Assumptions

Given: Countable choice and such a real or complex Lie algebra.

[A1]

Countable choice is the principle recorded in The Axiom of Countable Choice (ACω).

[L1]

A closed subgroup of a finite-dimensional Lie group is an embedded Lie subgroup; its published proof uses [A1] (Cartan closed subgroup theorem).

[L2]

Every derivation of g is inner (Derivations of semisimple Lie algebras are inner).

Proof

technique · polynomial equations and differentiation
1.1A1L1algebra

Choose a basis of g. The equations A[x,y]=[Ax,Ay] for basis pairs are finitely many polynomial equations in the matrix entries of A. Their common zero set inside GL⁡(g) is exactly Aut⁡(g) and is closed. By [L1] it is an embedded Lie subgroup; for a complex algebra, apply [L1] first to the underlying real group.

1.2L1algebra

A tangent vector at the identity is represented by A(t)=I+tD+o(t). Differentiating the bracket equation gives D[x,y]=[Dx,y]+[x,Dy], so the tangent algebra is contained in Der⁡(g). Conversely, for a derivation D, the linear vector field A↦DA is tangent to the defining equations, or equivalently its local flow exp⁡(tD) preserves the bracket by differentiating exp⁡(tD)[x,y]−[exp⁡(tD)x,exp⁡(tD)y]; hence every derivation is tangent. When g is complex, the ambient group consists of complex-linear maps and the resulting space of complex-linear derivations is stable under multiplication by i; exponential charts therefore give the embedded subgroup its corresponding complex Lie-subgroup structure.

2.1A1L2step 1.11.2∎

Step 1.2 identifies the Lie algebra with Der⁡(g), and [L2] identifies that with ad⁡(g). If g=0, the automorphism group is the one-point group and all tangent algebras are zero. Countable choice is used only through [L1], not in the polynomial or differentiation steps.

Depends on

Used by

Dependency tree · two levels

24 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