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.

Engel triangularization theorem

Statement

Let $V$ be finite-dimensional over any field, and let $ρ : g \to g l (V)$ be nil. Then there is a flag

$0 = V_{0} \subset V_{1} \subset \dots \subset V_{n} = V$

with $\dim V_{i} = i$ and $ρ (g) V_{i} \subseteq V_{i - 1}$ . Equivalently, there is a basis in which every $ρ (x)$ is strictly upper triangular.

Facts & Assumptions

Given: A nil representation of a Lie algebra $g$ on a finite-dimensional vector space $V$ .

[L1]

On a nonzero finite-dimensional nil module there is a nonzero vector annihilated by all of $g$ (Engel's common-zero-vector lemma).

[L2]

An invariant subspace and its quotient carry the restricted and induced representations (Subrepresentations, quotient representations, and intertwiners).

[L3]

The canonical projection onto a vector-space quotient is linear and surjective (The quotient vector space $V / W$ and its canonical projection).

Proof

technique · induction on $\dim V$

1.1basegiven

If $V = 0$ , the empty flag has the required property and the empty basis gives the matrix assertion.

1.2ihgiven

Assume $V \neq 0$ and the theorem for all nil modules of dimension smaller than $\dim V$ .

1.3L1L2

By [L1], choose $0 \neq v \in V$ with $g v = 0$ , and set $V_{1} = k v$ . This is an invariant one-dimensional subspace annihilated by $g$ .

2.1L2L3step 1.2step 1.3

Every induced operator on $V / V_{1}$ is nilpotent, since a power of $ρ (x)$ that vanishes on $V$ also vanishes on the quotient. By [L2] and step 1.2, the quotient has a flag $0 = {\overline{V}}_{1} \subset \dots \subset {\overline{V}}_{n} = V / V_{1}$ with $g {\overline{V}}_{i} \subseteq {\overline{V}}_{i - 1}$ . Taking inverse images under the projection [L3] and adjoining $0 \subset V_{1}$ gives the required flag of $V$ .

3.1step 1.1step 2.1discharge-induction∎

Choose vectors adapted to the flag, in the finite sequential sense. The containment $ρ (g) V_{i} \subseteq V_{i - 1}$ says every matrix sends the $i$ th basis vector into the span of earlier vectors, hence is strictly upper triangular in this ordering. Conversely a common strictly upper-triangular basis supplies exactly this flag. The zero case was covered in step 1.1.

Depends on

Dependency tree · 2 levels

Sources

Knapp, Lie Groups Beyond an Introduction, Theorem 1.35