PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)

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.

Under Choice, the Killing form pairs only opposite root spaces

Statement

Assume the Axiom of Choice. Let $B$ be the Killing form from The Killing form of a semisimple Lie algebra, and let $x \in g_{α}$ , $y \in g_{β}$ for the root-space decomposition of Root-space decomposition relative to a Cartan subalgebra. If $α + β \neq 0$ , then

$B (x, y) = 0.$

In particular, $B$ pairs nontrivially only opposite root spaces and restricts nondegenerately to $h$ .

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice), roots $α, β$ of a Cartan subalgebra $h$ , vectors $x \in g_{α}$ , $y \in g_{β}$ , and the Killing form $B$ .

[L1]

Under the given Choice premise, an arbitrary Cartan subalgebra has the displayed finite root-space direct sum (Root-space decomposition relative to a Cartan subalgebra).

[L2]

The Killing form is invariant and globally nondegenerate on a finite-dimensional complex semisimple Lie algebra (The Killing form is invariant and nondegenerate on a complex semisimple Lie algebra).

Proof

technique · direct

1.1L2givenalgebra

For any $h \in h$ , invariance from [L2] gives $0 = B ([h, x], y) + B (x, [h, y]) = (α (h) + β (h)) B (x, y)$ .

2.1L1step 1.1

If $α + β \neq 0$ , choose $h \in h$ with $(α + β) (h) \neq 0$ ; then step 1.1 forces $B (x, y) = 0$ . Also, [L1] identifies $h$ as the zero-weight space. For $h_{0} \in h$ , the same invariance argument with $x = h_{0}$ and $y \in g_{α}$ gives $B (h_{0}, y) = 0$ , so $h$ is orthogonal to every nonzero root space.

3.1L1L2step 2.1∎

If $h_{0} \in h$ is orthogonal to $h$ , then step 2.1 makes it orthogonal to every nonzero root space. Under Choice, the complete direct sum in [L1] makes it orthogonal to all of $g$ , and global nondegeneracy in [L2] gives $h_{0} = 0$ . Thus $B ∣_{h}$ is nondegenerate.

Depends on

Used by

Dependency tree · two levels

8 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)