Representation Qit
Exercise PLAN-103
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
Let (phi, V) be a representation of a finite group G over a field whose characteristic does not divide |G|, and let W be a G-invariant subspace with some (not necessarily invariant) projection P_W onto W (P_W^2 = P_W, im P_W = W). Define Q_W := (1/|G|) sum_{g in G} phi(g) P_W phi(g)^{-1}. Prove that Q_W commutes with every phi(g), that im Q_W = W and Q_W is a projection, and conclude that ker Q_W is a G-invariant complement, so V = W (+) ker Q_W as representations. Indicate where the hypothesis on the characteristic is used.
Hint: mathematical route
Averaging a projection over the group produces an equivariant projection onto the invariant subspace whose kernel is an invariant complement, provided |G| is invertible in the field.
- phi(h)Q_W phi(h)^{-1} = (1/|G|) sum_g phi(hg)P_W phi(hg)^{-1}; reindexing g->hg shows this equals Q_W.
- Hence Q_W commutes with every phi(h).
- Invariance of W makes each phi(g)P_W phi(g)^{-1} have image in W, so im Q_W subset W.
- For w in W each term returns w; the normalized average (needing |G| invertible, i.e. char not dividing |G|) gives Q_W w = w.
- Thus im Q_W = W, Q_W^2 = Q_W, and commuting with phi makes ker Q_W invariant: V = W (+) ker Q_W.
Reference solution
Equivariance: for h in G, phi(h) Q_W phi(h)^{-1} = (1/|G|) sum_g phi(h)phi(g) P_W phi(g)^{-1} phi(h)^{-1} = (1/|G|) sum_g phi(hg) P_W phi(hg)^{-1}. Reindexing g' = hg (a bijection of G) shows this equals Q_W, so phi(h) Q_W = Q_W phi(h) for all h. Image in W: invariance means phi(g)^{-1} maps V into V, P_W maps into W, and phi(g) maps W into W, so each term phi(g) P_W phi(g)^{-1} has image in W; the average does too, giving im Q_W subset W. Q_W fixes W pointwise: for w in W, phi(g)^{-1} w in W, P_W fixes it, and phi(g) phi(g)^{-1} w = w, so each term returns w; the normalized average (1/|G|) sum_g w = w. This normalization is exactly where the characteristic hypothesis enters: 1/|G| must exist in the field, i.e. |G| must be invertible, which holds iff the characteristic does not divide |G|. Hence Q_W|_W = id_W, so Q_W maps everything into W and acts as the identity there, giving Q_W^2 = Q_W: a projection onto W. Finally, since Q_W commutes with all phi(g), both im Q_W = W and ker Q_W are G-invariant, and V = im Q_W (+) ker Q_W = W (+) ker Q_W. Thus W has a G-invariant complement and the decomposition is of representations.
Assessment rubric
- Proves phi(h) Q_W phi(h)^{-1} = Q_W via the reindexing g -> hg, i.e. Q_W commutes with phi (1 weight)
- Shows im Q_W subset W (each averaged term lands in W by invariance) and Q_W fixes W pointwise, hence im Q_W = W and Q_W^2 = Q_W (1 weight)
- Identifies that the normalization 1/|G| requires |G| invertible, i.e. char does not divide |G| (1 weight)
- Concludes ker Q_W is a G-invariant complement giving V = W (+) ker Q_W as representations (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
- Operator and semigroup theory (frozen curriculum anchor; see graph registry)
- Matrix analysis (frozen curriculum anchor; see graph registry)
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: bb6f4bec4721a466c7a4dca570c26354bb2773a6b052bfdabedf4acb2ea6cb0a
Item digest: da4e2877f4284ace0995f01785a6c7c6c5c209746ca8a2c28b52e5252370b82f
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 5. This is not measured graph distance or model difficulty.