TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Lie's theorem

Statement

Let $g$ be a finite-dimensional solvable Lie algebra over an algebraically closed field $k$ of characteristic zero. Every nonzero finite-dimensional $g$ -module $V$ contains a common eigenvector: there are $0 \neq w \in V$ and $χ \in g^{*}$ such that $y w = χ (y) w$ for every $y \in g$ .

Facts & Assumptions

Given: The algebraically closed characteristic-zero field $k$ , a finite-dimensional solvable $k$ -Lie algebra $g$ , and a nonzero finite-dimensional representation on $V$ .

[L1]

A nonzero finite-dimensional solvable Lie algebra has a codimension-one ideal (Codimension-one ideal in a nonzero solvable Lie algebra).

[L2]

A representation is linear and satisfies $[x, h] v = x (h v) - h (x v)$ (Representations of Lie algebras).

[L3]

Every endomorphism of a nonzero finite-dimensional vector space over an algebraically closed field has an eigenvalue (Every endomorphism of a nonzero finite-dimensional vector space over an algebraically closed field has an eigenvalue).

[L4]

For finite-dimensional endomorphisms, $tr (A B) = tr (B A)$ (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ ).

Proof

technique · induction on $\dim\mathfrak g$

1.1basegiven

If $g = 0$ , any nonzero $w \in V$ is a common eigenvector with the zero functional.

1.2ihgiven

Assume $g \neq 0$ and the theorem for solvable Lie algebras of smaller dimension.

2.1L1L2step 1.2algebra

By [L1], choose a codimension-one ideal $h$ and write $g = h \oplus k x$ . Its derived series is contained termwise in that of $g$ , so $h$ is solvable. Step 1.2 gives $0 \neq v \in V$ and $λ \in h^{*}$ with $h v = λ (h) v$ for every $h \in h$ .

3.1L2step 2.1algebra

Put $W_{j} = span (v, x v, \dots, x^{j} v)$ and $W = \sum_{j \geq 0} W_{j}$ ; finite dimensionality makes $W$ finite-dimensional and $x$ -stable. Induction on $j$ , using $h x^{j} = x^{j} h + \sum_{i = 0}^{j - 1} x^{i} [h, x] x^{j - 1 - i}$ and $[h, x] \in h$ , shows $h W_{j} \subseteq W_{j}$ and $h x^{j} v \equiv λ (h) x^{j} v (m o d W_{j - 1})$ . Thus $W$ is $g$ -stable and every $h \in h$ acts upper triangularly on a basis extracted from the cyclic list, with constant diagonal $λ (h)$ .

4.1L2L4step 3.1algebra

Let $d = \dim W > 0$ . Because $W$ is stable, [L2] and [L4] give $0 = {tr}_{W} ([x, h]) = d λ ([x, h])$ for every $h \in h$ , where the last equality uses the constant diagonal from step 3.1. Characteristic zero makes $d \cdot 1_{k} \neq 0$ , so $λ ([x, h]) = 0$ . This is the exact use of the characteristic hypothesis.

5.1L2step 2.1step 4.1algebra

The nonzero common $h$ -weight space $V_{λ} = {u : h u = λ (h) u for all h \in h}$ contains $v$ . It is $x$ -stable: for $u \in V_{λ}$ , [L2] and step 4.1 give $h (x u) = x (h u) + [h, x] u = λ (h) x u + λ ([h, x]) u = λ (h) x u$ .

6.1L3step 2.1step 5.1discharge-induction∎

By algebraic closure and [L3], $x ∣_{V_{λ}}$ has a nonzero eigenvector $w$ , say $x w = a w$ . Then $h w = λ (h) w$ for $h \in h$ , and for $y = h + t x$ we have $y w = (λ (h) + t a) w$ . This defines the required linear functional $χ$ . Algebraic closure is used only in [L3], characteristic zero only in step 4.1, and all choices are a finite sequence of existential choices rather than AC.

Depends on

Dependency tree · 2 levels

Sources

Knapp, Lie Groups Beyond an Introduction, Theorem 1.25