Alphabeta Math
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.

Weyl's complete reducibility theorem

Statement

Every finite-dimensional representation of a finite-dimensional semisimple Lie algebra over any characteristic-zero field is completely reducible.

Facts & Assumptions

Given: A finite-dimensional semisimple characteristic-zero Lie algebra g, a finite-dimensional g-module V, and a submodule WV.

[L1]

A representation is completely reducible when it is an algebraic direct sum of irreducible representations; the zero representation is the empty sum (Irreducible, completely reducible, and faithful representations).

[L2]

A Casimir element from a nondegenerate invariant form acts as an intertwiner (The Casimir operator is basis-independent and intertwining).

[L3]

Over an algebraically closed field, every intertwiner of a finite- dimensional irreducible module is scalar (Schur’s lemma for irreducible Lie-algebra representations).

[L4]

The Killing form of a semisimple characteristic-zero algebra is nondegenerate (Cartan's semisimplicity criterion).

[L5]

A semisimple algebra is perfect (Semisimple Lie algebras are centerless and perfect).

[L6]

Cartan's solvability criterion applies to the trace form of any finite-dimensional representation (Cartan's solvability criterion).

[L7]

A nondegenerate invariant form and its dual bases define the Casimir operator used below (Casimir operator relative to an invariant form).

[L8]

A quotient of a semisimple algebra is semisimple (Ideals and quotients of semisimple Lie algebras).

[L9]

Every representation trace form is symmetric and invariant (Trace forms are symmetric and invariant).

[L10]

The radical of an invariant symmetric form is an ideal (Orthogonal complements under invariant forms are ideals).

Proof

technique · Casimir splitting and induction
1.1

We first work over an algebraically closed field. Every one-dimensional g-module is trivial: its representation kills [g,g], which equals g by [L5].

L5algebra
2.1

Suppose V/W is one-dimensional and W is simple. Replace g by its image h in gl(V); the kernel is an ideal and [L8] makes the quotient h semisimple. If h=0 the action is trivial and every line complementary to W is invariant, so assume h0. By [L9] its trace form on V is invariant and symmetric, so [L10] makes its radical an ideal; [L6] makes that radical solvable, hence zero. Form its Casimir C as in [L7]. It kills the trivial quotient V/W, while [L2] and [L3] say that it acts on W by a scalar a. Moreover trV(C)=dimh, by summing the dual-basis identities. Characteristic zero makes this nonzero, so a0. Consequently kerC is an invariant line complementary to W. This, together with W=0, is the induction base.

L2L3L6L7L8L9L10step 1.1base
3.1

Retain dim(V/W)=1 but allow arbitrary W, and assume the assertion for submodules of smaller dimension. If W is not simple, choose a nonzero proper submodule W. By the induction hypothesis, W/W has a complement V/W in V/W. Now V/W is one-dimensional, and another induction application splits V=WL. The line L is disjoint from W and complements it in V.

step 2.1IH
4.1

For general WV, give Homk(V,W) the action (xf)(v)=xf(v)f(xv). Let V1 consist of maps whose restriction to W is a scalar multiple of the identity, and W1 of maps vanishing on W. They are submodules and V1/W1 is one-dimensional. Step 3.1 gives an invariant line L=kf complementary to W1. By step 1.1, L is trivial, so f intertwines the action. Its restriction to W is a nonzero scalar—otherwise fW1—and after rescaling it is the identity. Therefore kerf is an invariant complement to W.

step 1.13.1
5.1

For an arbitrary characteristic-zero ground field, choose bases of g and V adapted to W, and let k0 be the subfield generated over Q by their finitely many structure and action coefficients. Nondegeneracy of the Killing matrix shows that the resulting k0-form of g is semisimple. Embed the finitely generated field k0 in C. Steps 1.1–4.1 over C produce an equivariant projection P:VCWC restricting to the identity. The conditions PW=1 and Pρ(x)=ρ(x)P for the chosen finite bases form a finite linear system over k0. Row reduction shows that consistency over C already gives a k0-solution; extending it to the original field gives an invariant kernel complementary to W. Since W was arbitrary, every submodule has an invariant complement. Induction on dimV now gives the direct-sum condition in [L1]: for V0, choose a nonzero submodule S of least dimension, which is irreducible; if SV, split V=ST and decompose the smaller module T by induction. For V=0 the empty direct sum is [L1]'s convention. Every descent, embedding, and row reduction uses only finite data, so no choice principle is used.

L1L4step 3.1discharge-induction: step 2.1induction

Depends on

Used by

Dependency tree · two levels

30 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