LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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).

[F2]

An idempotent endomorphism has trace equal to the dimension of its image as a field scalar (The trace of an idempotent is its rank as a field scalar).

Proof

technique · direct

1.1givenalgebra

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.

2.1F1step 1.1given

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}$ .

3.1F1step 2.1algebra

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.

4.1step 2.1step 3.1algebra

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$ .

5.1F2step 4.1step 3.1∎

Apply [F2] to the idempotent $P$ from step 4.1. Over $C$ this gives $tr P = \dim (im P)$ , and step 3.1 identifies $im P$ with $V^{G}$ .

Depends on

Used by

Dependency tree · two levels

7 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)