CounterexampleConstruction: Literature-sourcedVerification: 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.

Positive-characteristic failure of Lie's theorem

Counterexample

Let $k$ be a field of characteristic $p > 0$ . The solvable Lie algebra $a = k x \oplus k y$ with $[x, y] = y$ has a $p$ -dimensional irreducible module $V$ with basis $v_{0}, \dots, v_{p - 1}$ and action

$x v_{i} = i v_{i}, y v_{i} = v_{i + 1},$

where the second index is read modulo $p$ . In particular, the action has no common eigenline, so Lie's theorem fails in positive characteristic.

Facts & Assumptions

Given: A field $k$ of characteristic $p > 0$ , the displayed affine algebra, and the displayed operators $X, Y$ on $V$ .

[L1]

Lie's theorem assumes an algebraically closed field of characteristic zero and concludes the existence of a common eigenvector (Lie's theorem).

[L2]

Solvability is termination of the derived series (Derived series and solvable Lie algebras).

[L3]

A representation carries brackets to operator commutators (Representations of Lie algebras).

[L4]

A nonzero representation is irreducible when it has no nonzero proper stable subspace (Irreducible, completely reducible, and faithful representations).

Refutation

technique · counterexample

1.1

The only nonzero basis bracket of $a$ spans $k y$ , and $[k y, k y] = 0$ . Hence $a^{(1)} = k y$ and $a^{(2)} = 0$ , so $a$ is solvable by [L2].

L2givenalgebra

1.2

For $0 \leq i < p - 1$ , $(X Y - Y X) v_{i} = (i + 1 - i) v_{i + 1} = Y v_{i}$ . At the wraparound index, $(X Y - Y X) v_{p - 1} = (0 - (p - 1)) v_{0} = v_{0} = Y v_{p - 1}$ in characteristic $p$ ; this includes $p = 2$ . Thus $[X, Y] = Y$ , and the other basis-bracket identities are automatic, so $x \mapsto X$ , $y \mapsto Y$ is a representation by [L3].

L3givenalgebra

2.1

Let $0 \neq W \subseteq V$ be stable under $X$ and $Y$ , and choose a nonzero $w = \sum_{j} c_{j} v_{j} \in W$ with $c_{i} \neq 0$ . The scalars $0, 1, \dots, p - 1$ are distinct in $k$ . Therefore the Lagrange polynomial $P_{i} (T) = \prod_{j \neq i} (T - j) / (i - j)$ is defined and satisfies $P_{i} (X) w = c_{i} v_{i} \in W$ . Hence $v_{i} \in W$ . Repeated application of the cyclic operator $Y$ puts every basis vector $v_{j}$ in $W$ , so $W = V$ . By [L4], $V$ is irreducible.

L4step 1.2algebra

3.1

Since $p \geq 2$ , this irreducible module has dimension greater than one. A common eigenvector would span a nonzero proper stable line, contradicting step 2.1. Thus the solvable algebra in step 1.1 and the representation in step 1.2 violate the common-eigenvector conclusion when characteristic zero is removed from [L1]. Every selection is from fixed finite coordinates, so no choice principle is used.

L1step 1.1step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Etingof, Lie Groups and Lie Algebras, positive-characteristic counterexample (standard reference, not scraped)