Exercise PLAN-116

Isotypical components are unique but splitting a multiplicity-greater-than-one component into individual irreducible subspaces is not, as shown by two distinct trivial-line splittings of the symmetric subspace of (C^2)^{(x)2}.

1. Proposition 3.22 fixes the isotypical components, not the internal irreducible splitting of a multiplicity > 1 component.
2. Vtriv = Sym^2(C^2) (the +1 eigenspace of F) is the unique 3-dim trivial-isotypical component with trivial S_2 action.
3. Since S_2 acts as identity on Vtriv, every line is a trivial subrep; two different line-splittings of Vtriv both valid.
4. Non-uniqueness comes from the freedom to change basis of the multiplicity space; multiplicity-free decompositions are unique.

The student's reading is wrong: it is the isotypical components that are unique, not the splitting of a multiplicity-greater-than-one component into individual irreducible subspaces. Take the S_2 action on (C^2)^{(x)2} with phi((12)) = F. The symmetric subspace Vtriv = Sym^2(C^2) is the +1 eigenspace of F, a 3-dimensional space on which S_2 acts trivially; it is the trivial-isotypical component and is uniquely determined (it equals the +1 eigenspace of F, basis-independent). But because S_2 acts as the identity on all of Vtriv, EVERY one-dimensional subspace of Vtriv is an irreducible (trivial) subrepresentation, and Vtriv can be written as a direct sum of three trivial lines in infinitely many ways. Concretely, one splitting is Vtriv = span(|00>) (+) span(|11>) (+) span((|01>+|10>)/sqrt 2); a genuinely different splitting is Vtriv = span((|00>+|11>)/sqrt 2) (+) span((|00>-|11>)/sqrt 2) (+) span((|01>+|10>)/sqrt 2). Both are decompositions of Vtriv into three irreducible (trivial) subrepresentations, but the first line span(|00>) of the first splitting is not among the lines of the second splitting, so the two decompositions into irreducibles are different. This does not contradict Proposition 3.22: the isotypical component Vtriv itself is identical in both (it is the full +1 eigenspace of F), and only its internal basis / line-by-line splitting changed. The source of the non-uniqueness is multiplicity: when an irrep occurs with multiplicity n >= 2, the choice of the n individual copies corresponds to a choice of basis of the n-dimensional multiplicity space, and any invertible change of that basis gives an equally valid finer decomposition. Uniqueness is recovered precisely in the multiplicity-free case.

1. Diagnoses the over-reading: isotypical components are unique, but the splitting of a multiplicity >= 2 component into irreducible subspaces is not (1 weight)
2. Identifies Vtriv = Sym^2(C^2) as the unique trivial-isotypical component (the +1 eigenspace of F), 3-dimensional with trivial action (1 weight)
3. Exhibits two genuinely different direct-sum splittings of Vtriv into trivial lines and notes a line in one is absent from the other (1 weight)
4. Attributes the non-uniqueness to multiplicity (choice of basis of the multiplicity space) and notes uniqueness holds in the multiplicity-free case, consistent with Proposition 3.22 (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: 51057561f0fc75f037dd19eed229350d6fd6055dd9466110f4154df9df57252f

Item digest: ab9df40fd93fe05c0101d8c2d0d0b36cb55443c64c0780a092a57db7377c5e67

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.