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.

Dimension formula from roots

Statement

Assume the Axiom of Choice. Let h be a Cartan subalgebra of a finite-dimensional complex semisimple Lie algebra g with root set Φ (Root and root space). Then dim⁡g=dim⁡h+∣Φ∣. Moreover all Cartan subalgebras of g have the same dimension, so the right-hand side is independent of the chosen Cartan subalgebra, and this common dimension is the quantity rank⁡g of Regular element and rank.

Facts & Assumptions

Given: The Axiom of Choice and such g and h, with root set Φ.

[A1]

The Axiom of Choice is The Axiom of Choice and supplies the countable choice (The Axiom of Countable Choice (ACω)) used in [L3].

[L1]

g=h⊕⨁α∈Φgα is a direct sum with Φ finite and dim⁡gα=1 for every root (Root-space decomposition, Roots of a complex semisimple Lie algebra form a reduced crystallographic root system, Root and root space).

[L2]

Any two Cartan subalgebras of g are conjugate, hence of the same dimension (Conjugacy of Cartan subalgebras).

[L3]

Under countable choice, g viewed as a real Lie algebra integrates to a connected Lie group; its adjoint representation is smooth with differential ad⁡, and a smooth submersion is open (Lie's third fundamental theorem, Adjoint is a smooth Lie-group representation, The differential of Ad is ad, Every submersion is an open map).

Proof

technique · direct
1.1L1algebra

By [L1] the vector space g is the direct sum of h and one one-dimensional space for each of the ∣Φ∣ roots; dimensions are additive over direct sums, so dim⁡g=dim⁡h+∣Φ∣.

1.2L1algebra

Let h∘ be the complement in h of the finitely many root hyperplanes ker⁡α. A finite union of proper linear subspaces cannot cover a complex vector space, so h∘ is nonempty (and equals {0} when g=0). For H∈h∘, [L1] gives gH=ker⁡(ad⁡H)=h, because ad⁡H acts by the nonzero scalar α(H) on every gα.

2.1A1L1L3step 1.2algebra

Let G be the connected real Lie group supplied by [L3] for the underlying real Lie algebra of g, and define F:G×h∘⟶g by F(g,H)=Ad⁡gH. At (e,H) its differential is (Y,K)↦[Y,H]+K by [L3]. The root decomposition [L1] and the inequalities α(H)≠0 give [g,H]=⨁α∈Φgα, so this differential is onto. Translation in G and composition with Ad⁡g show the same at every (g,H); hence F is a submersion. By [L3] its image U is a nonempty open subset of g, and every point of U has centralizer dimension dim⁡h by step 1.2 and conjugation invariance.

3.1L3step 2.1algebra

Put r=rank⁡g and n=dim⁡g. In a fixed basis the entries of ad⁡x depend linearly on x. Choose x0 with dim⁡ker⁡(ad⁡x0)=r and an (n−r)×(n−r) minor nonzero at x0. The nonvanishing set of this minor is a nonempty dense open subset R of the complex vector space g; at every point of R, the adjoint map has rank at least n−r, and maximality of n−r forces kernel dimension exactly r. Thus R consists of regular elements. Since R is dense and U from step 2.1 is nonempty open, choose x∈R∩U. Then r=dim⁡gx=dim⁡h.

4.1L2step 1.1step 3.1∎

By [L2], all Cartan subalgebras have this same dimension; step 3.1 identifies it with rank⁡g. Substituting in step 1.1 yields dim⁡g=rank⁡g+∣Φ∣, including the zero algebra.

Depends on

Used by

Dependency tree · two levels

72 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