TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Every irreducible representation of a finite group is a quotient of the regular representation

Statement

Let $G$ be a finite group and let $V$ be an irreducible representation of $G$ over a field $k$ . Then there is a surjective morphism from the regular representation of $G$ over $k$ onto $V$ .

Facts & Assumptions

Given: A finite group $G$ , a field $k$ , and an irreducible representation $V$ of $G$ over $k$ .

[L1]

Under the group-ring dictionary, subrepresentations are exactly $k [G]$ -submodules, and irreducible representations are exactly simple $k [G]$ -modules (Under the dictionary, subrepresentations are exactly submodules and irreducible representations are exactly simple modules).

[L2]

The regular representation is the action of $G$ on $k [G]$ by left multiplication on the basis vectors $[g]$ (The trivial representation, the regular representation, and permutation representations from finite $G$ -sets).

[L3]

$G$ -equivariant maps are exactly $k [G]$ -module homomorphisms (For a commutative ring $R$ , $R$ -linear $G$ -actions are exactly the compatible left $R [G]$ -module structures).

Proof

technique · direct

1.1

By [L1], the representation $V$ is a simple $k [G]$ -module.

L1given

2.1

Choose $0 \neq v \in V$ . The submodule $k [G] v$ is nonzero, so simplicity from step 1.1 forces $k [G] v = V$ .

step 1.1L1givenchoose

3.1

Define $ϕ : k [G] \to V$ by $ϕ (a) : = a \cdot v$ . Then $ϕ$ is a $k [G]$ -module homomorphism, and its image is exactly $k [G] v = V$ by step 2.1. So $ϕ$ is surjective.

step 2.1L3givenalgebra

4.1

By [L2] and [L3], the map $ϕ$ is a surjective morphism from the regular representation onto $V$ . Hence $V$ is a quotient of the regular representation.

step 3.1L2L3∎

Depends on

Used by

Every irreducible representation of a finite group has degree at most |G| Corollary

Dependency tree · two levels

14 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

Peter Webb, A Course in Finite Group Representation Theory, Theorem 2.1.1 and its regular-module corollaries (standard reference, not scraped)