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.

Triangular decomposition

Statement

Assume the Axiom of Choice. Let $g$ be a finite-dimensional complex semisimple Lie algebra with Cartan subalgebra $h$ and a chosen positive system, and let $n^{\pm}$ and $b = h \oplus n^{+}$ be as in Positive and negative nilpotent subalgebras and the Borel. Then:

(i) $g = n^{-} \oplus h \oplus n^{+}$ is a direct sum of vector spaces;

(ii) $n^{+}$ and $n^{-}$ are nilpotent Lie subalgebras and $b$ is a solvable Lie subalgebra in which $n^{+}$ is an ideal, so that $b$ is the semidirect sum $h ⋉ n^{+}$ .

Facts & Assumptions

Given: The Axiom of Choice, such $g, h$ , a positive system $Φ^{+}$ with negative roots $Φ^{-} = - Φ^{+}$ , and the subspaces $n^{\pm}$ , $b$ of Positive and negative nilpotent subalgebras and the Borel.

[A1]

The Axiom of Choice is assumed; it enters through the root-space theory supplying [L1] (The Axiom of Choice).

[L1]

$Φ$ is finite and $g = h \oplus ⨁_{α \in Φ} g_{α}$ is a direct sum over distinct eigenspaces (Root-space decomposition); also $[g_{α}, g_{β}] \subseteq g_{α + β}$ with $g_{γ} = 0$ when $γ \notin Φ \cup {0}$ (Brackets of root spaces).

[L2]

$n^{\pm}$ are nilpotent Lie subalgebras, $b = h \oplus n^{+}$ is a Lie subalgebra containing $n^{+}$ as the sum of the root spaces $g_{α}$ with $α \in Φ^{+}$ , $[h, g_{α}] \subseteq g_{α}$ , and $Φ = Φ^{+} ⊔ Φ^{-}$ (Positive and negative nilpotent subalgebras and the Borel).

[L3]

A Lie algebra is nilpotent when its lower central series reaches $0$ , and solvable when its derived series reaches $0$ (Lower central series and nilpotent Lie algebras, Derived series and solvable Lie algebras).

Proof

technique · direct

1.1

By [L1] the sum $h + \sum_{α \in Φ} g_{α}$ is direct over the distinct eigenspaces, and $Φ = Φ^{+} ⊔ Φ^{-}$ by [L2]; since $n^{\pm} = \sum_{\pm α \in Φ^{+}} g_{α}$ , the subspace $n^{-} + h + n^{+}$ is the direct sum of the spaces $g_{α}$ ( $α \in Φ$ ) and $g_{0} = h$ , hence equals $g$ directly. This proves (i).

A1L1L2

1.2

The subalgebras $n^{\pm}$ are nilpotent by [L2]; this is the nilpotent part of (ii).

L2L3

1.3

$b$ is a subalgebra by [L2], and its derived algebra satisfies $[b, b] \subseteq [h, h] + [h, n^{+}] + [n^{+}, n^{+}] \subseteq n^{+}$ , because $[h, h] = 0$ , $[h, g_{α}] \subseteq g_{α}$ for $α \in Φ^{+}$ by [L2], and $[n^{+}, n^{+}] \subseteq n^{+}$ by [L2].

A1L2

2.1

By step 1.3 the derived series of $b$ satisfies $b^{(0)} = b$ , $b^{(1)} \subseteq n^{+}$ , and inductively $b^{(k)} \subseteq γ_{k} (n^{+})$ for every $k \geq 1$ , because $b^{(k + 1)} = [b^{(k)}, b^{(k)}] \subseteq [n^{+}, γ_{k} (n^{+})] = γ_{k + 1} (n^{+})$ by monotonicity of the bracket and the definition of the lower central series (Lower central series and nilpotent Lie algebras); since $n^{+}$ is nilpotent, $γ_{k} (n^{+}) = 0$ for some $k$ by [L3], hence $b^{(k)} = 0$ and $b$ is solvable.

L2L3step 1.3

3.1

Finally $n^{+}$ is an ideal of $b$ , since it is a subspace of $b$ with $[b, n^{+}] \subseteq [h, n^{+}] + [n^{+}, n^{+}] \subseteq n^{+}$ by step 1.3 and Lie subalgebras, ideals, and center; because moreover $b = h + n^{+}$ with $h \cap n^{+} = 0$ by step 1.1, the algebra $b$ is the semidirect sum of $h$ and the ideal $n^{+}$ , which together with steps 1.1, 1.2 and 2.1 proves both assertions. ∎

Depends on

Used by

Highest weight modules lie below the top weight Lemma
Simple-root integrability bounds the dominant cyclic module Lemma
The dominant cyclic generator survives Lemma
The highest-weight space is one-dimensional Proposition

Dependency tree · two levels

21 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

Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)