Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Complete reducibility for compact Lie groups

Statement

Assume the Axiom of Choice. Every finite-dimensional continuous complex representation of a compact Lie group is a direct sum of irreducible representations.

Facts & Assumptions

Given: Assume the Axiom of Choice, a compact Lie group G and a finite-dimensional complex representation π:G→GL⁡(V).

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through [L1].

[L1]

Every finite-dimensional continuous complex representation of G preserves some positive-definite Hermitian inner product, so it may be regarded as unitary for that inner product (Finite-dimensional compact-group representations are unitarizable, Continuous and unitary representations).

[L2]

A subrepresentation of π is a linear subspace stable under every π(g); π is irreducible when V≠0 and there is no nonzero proper subrepresentation, and a direct sum of subrepresentations V=V1⊕⋯⊕Vm is a decomposition into representations by restriction (Continuous and unitary representations).

[L3]

For every subspace W of a finite-dimensional inner-product space V, one has V=W⊕W⊥ and dim⁡W+dim⁡W⊥=dim⁡V (For a subspace W of a finite-dimensional inner product space, V=W⊕W⊥, In finite dimension, W⊥⊥=W and dim⁡W+dim⁡W⊥=dim⁡V). A proper subspace of a finite-dimensional space has smaller dimension, and the zero representation is the direct sum of the empty family. [finite-dimensional linear algebra, empty-sum convention]

Proof

technique · direct
1.1L2L3

We argue by induction on n=dim⁡V, assuming the assertion for all representation spaces of dimension <n. If n=0 then V is the empty direct sum of irreducibles by [L3]; otherwise V has a nonzero subrepresentation, and choosing among the nonzero subrepresentations one of least positive dimension gives an irreducible subrepresentation W, since any nonzero proper subrepresentation of W would be a nonzero subrepresentation of V of strictly smaller positive dimension by [L3].

1.2L1L2

By [L1] fix a G-invariant positive-definite Hermitian inner product on V and let W⊥ be the orthogonal complement of W; then W⊥ is a subrepresentation, because for w′∈W⊥, w∈W and g∈G unitarity and invariance of W give ⟨π(g)w′,w⟩=⟨w′,π(g)−1w⟩ with π(g)−1w=π(g−1)w∈W, so ⟨π(g)w′,w⟩=0.

2.1A1L2L3step 1.1step 1.2∎

Since W≠0, [L3] gives dim⁡W⊥=dim⁡V−dim⁡W<dim⁡V, so the inductive hypothesis applies to the subrepresentation W⊥ and exhibits it as a direct sum of irreducible subrepresentations; adjoining the irreducible summand W gives V=W⊕W⊥ as a direct sum of irreducibles by [L2]. The Axiom of Choice entered only through [L1].

Depends on

Used by

Dependency tree · two levels

20 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