LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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.

The averaging operator projects onto the fixed subspace

Statement

Let $ρ : G \to GL (V)$ be a finite-dimensional representation of a finite group $G$ over $C$ . The averaging operator

$P : = \frac{1}{∣ G ∣} \sum_{g \in G} ρ (g)$

satisfies $P^{2} = P$ and has image exactly $V^{G}$ ; consequently $tr P = \dim V^{G}$ .

Facts & Assumptions

Given: A finite group $G$ and a finite-dimensional complex representation $ρ : G \to GL (V)$ .

[F1]

The fixed subspace is $V^{G} = {v \in V : g \cdot v = v for every g \in G}$ (The fixed subspace $V^{G}$ of a representation).

[A2]

If $T$ is a projection of a finite-dimensional vector space, meaning $T^{2} = T$ , then $V = im T \oplus \ker T$ , $T$ restricts to the identity on $im T$ , and in a basis adapted to that decomposition the matrix of $T$ is block diagonal with an identity block and a zero block.

Proof

technique · direct

1.1

For $h \in G$ , $ρ (h) P = \frac{1}{∣ G ∣} \sum_{g} ρ (h g)$ $= \frac{1}{∣ G ∣} \sum_{g} ρ (g) = P$ , because left translation by $h$ permutes $G$ , so the sums run over the same index set.

givenalgebra

2.1

Hence for every $v \in V$ , the vector $P v$ satisfies $h \cdot (P v) = ρ (h) P v = P v$ for every $h \in G$ , so $P v \in V^{G}$ by [F1]; thus $im P \subseteq V^{G}$ .

F1step 1.1given

3.1

If $v \in V^{G}$ , then $ρ (g) v = v$ for every $g$ by [F1], so $P v = \frac{1}{∣ G ∣} \sum_{g} v = \frac{∣ G ∣}{∣ G ∣} v = v$ . Thus $V^{G} \subseteq im P$ , and with step 2.1, $im P = V^{G}$ exactly.

F1step 2.1algebra

4.1

For $v \in V^{G}$ , step 3.1 gives $P (P v) = P v = v = P v$ ; for general $v$ , $P v \in V^{G}$ by step 2.1, so $P^{2} v = P (P v) = P v$ . Hence $P^{2} = P$ .

step 2.1step 3.1algebra

5.1

By [A2] applied to $P$ from step 4.1, $V = im P \oplus \ker P$ and the matrix of $P$ in an adapted basis has an identity block of size $\dim (im P)$ and a zero block. Its trace is therefore $\dim (im P)$ , and step 3.1 identifies $im P$ with $V^{G}$ .

A2step 4.1step 3.1algebra∎

Depends on

The fixed subspace $V^G$ of a representation

Used by

The class-function inner product ⟨χ_V,χ_W⟩ equals dimHom_G(W,V) Theorem

Dependency tree · two levels

3 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, Lemma 3.2.2 (standard reference, not scraped)