CorollaryStatement: 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.

Opposite root spaces pair nondegenerately

Statement

Assume the Axiom of Choice. Let $α$ be a root of the finite-dimensional complex semisimple Lie algebra $g$ with respect to a Cartan subalgebra $h$ (Root and root space). Then $- α$ is a root, and the Killing form restricts to a nondegenerate pairing $g_{α} \times g_{- α} \to C$ ; in particular $g_{- α} \neq 0$ and $B$ is nonzero on $g_{α} \times g_{- α}$ .

Facts & Assumptions

Given: The Axiom of Choice, such $g, h$ and a root $α$ .

[A1]

The Axiom of Choice is The Axiom of Choice; it licenses the orthogonality and root-space decomposition used in [L1] and [L2].

[L1]

$B (g_{γ}, g_{δ}) = 0$ whenever $γ + δ \neq 0$ , and $B ∣_{h}$ is nondegenerate (Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra).

[L2]

$g = h \oplus ⨁_{γ \in Φ} g_{γ}$ is a direct sum (Root-space decomposition), and $B$ is nondegenerate on the semisimple algebra $g$ (Cartan's semisimplicity criterion).

Proof

technique · direct

1.1

Let $0 \neq x \in g_{α}$ . By nondegeneracy of $B$ there is $y \in g$ with $B (x, y) \neq 0$ ; write $y = y_{0} + \sum_{γ} y_{γ}$ according to [L2]. By [L1] all summands vanish in the pairing with $x$ except possibly $y_{- α}$ , whose weight space would make $- α$ a root; hence $B (x, y_{- α}) \neq 0$ , so $- α$ is a root and $g_{- α} \neq 0$ .

A1L1L2algebra

2.1

The restriction of $B$ to $g_{α} \oplus g_{- α}$ is nondegenerate: if $x \in g_{α}$ pairs to zero with all of $g_{- α}$ , then it pairs to zero with every weight space and with $h$ by [L1], hence with $g$ , so $x = 0$ ; the same argument applies to $g_{- α}$ . Since $g_{α} \neq 0$ by definition of a root, this nondegenerate pairing is nonzero.

L1L2step 1.1algebra∎

Depends on

Used by

If alpha and beta are roots then alpha plus beta is always a root False statement
Chevalley basis and real structure constants Lemma
The Killing length of a root is nonzero Lemma
The bracket of opposite root spaces is the root line Proposition
Existence and uniqueness up to isomorphism of the split real form Theorem
Existence of a compact real form Theorem
Roots of a complex semisimple Lie algebra form a reduced crystallographic root system Theorem
The root sl₂ triple Theorem

Dependency tree · two levels

18 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., Chapter II (standard reference, not scraped)