Alphabeta Math
TheoremStatement: 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.

Jordan decomposition lies inside a complex semisimple Lie algebra

Statement

Assume the Axiom of Choice. Every element x of a finite-dimensional complex semisimple Lie algebra g has a unique abstract Jordan decomposition x=xs+xn, and ad⁡xs, ad⁡xn are the additive Jordan–Chevalley parts of ad⁡x.

Facts & Assumptions

Given: The Axiom of Choice, a finite-dimensional complex semisimple Lie algebra g, and an element x∈g.

[A1]

The Axiom of Choice is The Axiom of Choice; it is inherited through [L1] and [L2], with [L2] itself using the operator theorem [L1].

[L1]

Under the Axiom of Choice, every endomorphism of a finite-dimensional vector space over a perfect field has a unique additive Jordan–Chevalley decomposition into commuting semisimple and nilpotent parts (Over a perfect field, every endomorphism has a unique commuting semisimple-plus-nilpotent decomposition, polynomial in the endomorphism).

[L2]

Under the Axiom of Choice, if ad⁡x=S+N is that additive decomposition, there are unique ys,yn∈g with S=ad⁡ys and N=ad⁡yn; they give the unique abstract Jordan decomposition of x. Conversely, any abstract Jordan decomposition has adjoints S,N (Jordan–Chevalley parts agree under the adjoint representation).

[L3]

An abstract Jordan decomposition is a decomposition x=xs+xn with commuting parts whose adjoints are semisimple, respectively nilpotent (Abstract Jordan decomposition).

Proof

technique · direct
1.1A1L1L2L3

The endomorphism ad⁡x of the finite-dimensional complex vector space g has an additive Jordan–Chevalley decomposition by [L1]. Applying clause (ii) of [L2] to it produces elements ys,yn∈g such that x=ys+yn, [ys,yn]=0, ad⁡ys is semisimple and ad⁡yn is nilpotent, and such that ad⁡ys, ad⁡yn are the additive parts of ad⁡x. By [L3] this is an abstract Jordan decomposition of x.

2.1A1L1L2L3step 1.1∎

Let x=u+v be any abstract Jordan decomposition. Clause (i) of [L2] identifies ad⁡u and ad⁡v with the additive Jordan–Chevalley parts of ad⁡x, which are the parts ad⁡ys and ad⁡yn produced in step 1.1; uniqueness of the abstract decomposition in [L2] then gives u=ys and v=yn. For g=0 the only element is 0 and the decomposition 0=0+0 satisfies the definition vacuously; the Axiom of Choice enters only through [L1] and [L2].

Depends on

Used by

Dependency tree · two levels

16 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