Representation Qit
Exercise PLAN-110
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 finite-dimensional complex representation of a finite group G, and let ( phi_U, U) be a complex irreducible representation of G. Recall that Hom_G(U, V) is the space of intertwiners f: U -> V, i.e. linear maps satisfying f . phi_U(g) = phi(g) . f for all g, and that Hom_G is additive in each argument: Hom_G(X, Y (+) Z) ~ Hom_G(X, Y) (+) Hom_G(X, Z). Prove that dim Hom_G(U, V) equals the multiplicity k of U in the isotypical decomposition of V. You should use Schur's Lemma to evaluate Hom_G(U, U) and Hom_G(U, F) where F collects the irreducible summands of V inequivalent to U.
Hint: mathematical route
The multiplicity of an irreducible U in V equals dim Hom_G(U, V): additivity splits the intertwiner space, Schur makes self-intertwiners one-dimensional and cross-intertwiners zero.
- V ~ U^{(+)k} (+) F and additivity give Hom_G(U, V) ~ ((+)_{i=1}^k Hom_G(U,U)) (+) Hom_G(U, F).
- Schur (ii) over C: Hom_G(U, U) = C 1_U, dimension 1.
- Schur (i) plus inequivalence: Hom_G(U, W) = 0 for irreducible W !~ U, so Hom_G(U, F) = 0.
- Summing, dim Hom_G(U, V) = k.1 + 0 = k, the multiplicity of U in V.
Reference solution
Decompose V ~ V_U (+) F, where V_U ~ U^{(+)k} is the isotypical component of U (U appearing with multiplicity k) and F is the direct sum of all irreducible summands of V inequivalent to U. By additivity of Hom_G in the second argument, Hom_G(U, V) ~ Hom_G(U, U^{(+)k}) (+) Hom_G(U, F) ~ ((+)_{i=1}^{k} Hom_G(U, U)) (+) Hom_G(U, F). Now evaluate the pieces with Schur's Lemma. First, Hom_G(U, U) is the space of G-equivariant endomorphisms of the irreducible U over C; by Schur (ii) every such endomorphism is a scalar multiple of 1_U, so Hom_G(U, U) = C . 1_U has dimension 1. Second, for any irreducible summand W of F, W is inequivalent to U, so by Schur (i) any equivariant map U -> W is either zero or an isomorphism; an isomorphism would make U ~ W, contradicting inequivalence, so the only equivariant map is 0. Hence Hom_G(U, W) = 0 for each such W, and by additivity Hom_G(U, F) = 0. Combining, dim Hom_G(U, V) = sum_{i=1}^{k} dim Hom_G(U, U) + dim Hom_G(U, F) = k . 1 + 0 = k. Therefore the dimension of the intertwiner space Hom_G(U, V) equals the multiplicity of U in V, which realizes the multiplicity space of U as the space of intertwiners from U into V.
Assessment rubric
- Decomposes V ~ U^{(+)k} (+) F and uses additivity of Hom_G to split Hom_G(U, V) accordingly (1 weight)
- Uses Schur (ii) to show Hom_G(U, U) = C 1_U is one-dimensional (1 weight)
- Uses Schur (i) and inequivalence to show Hom_G(U, W) = 0 for every irreducible summand W of F, hence Hom_G(U, F) = 0 (1 weight)
- Concludes dim Hom_G(U, V) = k, the multiplicity of U in V (multiplicity space realized as intertwiners) (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: cee296fe82abf1e6339294fdc26d65f67fb66af71dea301344a499dd30fbe96d
Item digest: 9b9f633d427e365f4b941d9ba0ac65a7198e50c1ed20cb2f793d3398242285ab
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.