TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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 from a chosen positive root system

Statement

Let $Φ^{+}$ be a positive system in the root set from Root-space decomposition relative to a Cartan subalgebra and put

$n^{+} : = ⨁_{α \in Φ^{+}} g_{α}, n^{-} : = ⨁_{α \in Φ^{+}} g_{- α} .$

Then

$g = n^{-} \oplus h \oplus n^{+}$

as a direct sum of vector spaces, $n^{\pm}$ are Lie subalgebras, and multiplication induces a vector-space isomorphism

$U (n^{-}) \otimes U (h) \otimes U (n^{+}) \tilde{\to} U (g) .$

Facts & Assumptions

Given: A Cartan subalgebra $h$ of a complex semisimple Lie algebra $g$ and a choice of positive roots $Φ^{+} \subseteq Φ$ .

Proof

technique · direct

1.1

The decomposition in Root-space decomposition relative to a Cartan subalgebra groups the positive, zero, and negative root spaces, so it immediately gives the direct-sum decomposition $g = n^{-} \oplus h \oplus n^{+}$ .

given

1.2

If $x \in g_{α}$ and $y \in g_{β}$ with $α, β \in Φ^{+}$ , then Brackets of root spaces add their roots shows $[x, y] \in g_{α + β}$ , which is again positive or zero. Because no sum of positive roots is zero, $n^{+}$ is a Lie subalgebra, and the same argument gives the same for $n^{-}$ .

algebra

2.1

Choose ordered bases of $n^{-}$ , $h$ , and $n^{+}$ and concatenate them in that order. The ordered PBW monomials from PBW gives an ordered monomial basis for the enveloping algebra are then exactly products of a monomial in $U (n^{-})$ , one in $U (h)$ , and one in $U (n^{+})$ , so multiplication gives the stated vector-space isomorphism.

step 1.1step 1.2∎

Depends on

Used by

Highest-weight vectors and cyclic highest-weight modules Definition
The Harish-Chandra projection Definition
The Weyl vector rho for a chosen positive system Definition

Dependency tree · two levels

7 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

Pavel Etingof, Lie Groups and Lie Algebras I (standard reference, not scraped)