QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-113

intermediate · proof · test_public

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. For the trivial representation, define P := (1/|G|) sum_{g in G} phi(g). Prove that (a) P is idempotent (P^2 = P), (b) im P = V^G := {|v> : phi(g)|v> = |v> for all g}, and (c) P commutes with every phi(h). Then explain, by taking the trace, why tr P equals the multiplicity of the trivial representation in V (the number of independent G-invariant vectors), connecting to the general character-projection formula P_W = (dim W / |G|) sum_g conj(chi_W(g)) phi(g).

      Hint: mathematical route

      Averaging the representation over G gives the orthogonal projection onto the invariant vectors V^G, whose trace counts the trivial-representation multiplicity, the trivial case of the character projection formula.

      1. Reindexing g -> hg gives phi(h) P = P (and P phi(h) = P), so P commutes with the representation.
      2. P^2 = (1/|G|) sum_g phi(g) P = P, so P is idempotent.
      3. im P subset V^G (image vectors fixed) and V^G subset im P (invariant vectors satisfy P|v>=|v>), so im P = V^G.
      4. As an orthogonal projection tr P = dim V^G = multiplicity of the trivial irrep, the chi_triv case of the character projector.
      Reference solution

      (a) and (c) together: for any h in G, phi(h) P = (1/|G|) sum_g phi(h)phi(g) = (1/|G|) sum_g phi(hg) = (1/|G|) sum_{g'} phi(g') = P, reindexing g' = hg (a bijection of G); likewise P phi(h) = P by reindexing on the right. So phi(h) P = P = P phi(h) for all h, which gives both that P commutes with every phi(h) and that P is left/right absorbing for the group action. Idempotency follows: P^2 = (1/|G|) sum_g phi(g) P = (1/|G|) sum_g P = P, using phi(g) P = P from the previous line. (b) If |v> in im P, write |v> = P|w>; then phi(h)|v> = phi(h) P|w> = P|w> = |v> for all h, so |v> in V^G, giving im P subset V^G. Conversely if |v> in V^G then phi(g)|v> = |v> for all g, so P|v> = (1/|G|) sum_g phi(g)|v> = (1/|G|) sum_g |v> = |v>, hence |v> in im P; thus V^G subset im P. Therefore im P = V^G. (b continued, trace) Since P is idempotent and (being an average of the unitaries phi(g) in a suitable invariant inner product) an orthogonal projection, its trace equals the dimension of its image: tr P = dim im P = dim V^G, which is precisely the number of independent G-invariant vectors, i.e. the multiplicity of the trivial representation in V. This is the chi_W = chi_triv = 1 case of the general formula P_W = (dim W/|G|) sum_g conj(chi_W(g)) phi(g): the trivial representation has dimension 1 and character identically 1, so P_triv = (1/|G|) sum_g phi(g) = P, and its trace recovers the multiplicity, consistent with the character inner-product formula for multiplicities.

      Assessment rubric
      1. Proves phi(h) P = P = P phi(h) via reindexing, giving both commutation with phi(h) and absorption (1 weight)
      2. Deduces idempotency P^2 = P from phi(g) P = P (1 weight)
      3. Proves im P = V^G by double inclusion (image vectors are invariant; invariant vectors are fixed by P) (1 weight)
      4. Explains tr P = dim V^G = multiplicity of the trivial representation, as the chi_triv case of P_W = (dim W/|G|) sum_g conj(chi_W(g)) phi(g) (1 weight)

      Graph-grounded prerequisites

      These are support/source anchors, not an automatically extracted theorem-dependency proof.

      • Harmonic analysis (frozen curriculum anchor; see graph registry)
      • Operator and semigroup theory (frozen curriculum anchor; see graph registry)
      • Matrix analysis (frozen curriculum anchor; see graph registry)

      Download the shared core 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.

      Read the Lean track and existing diagnostic warmups

      Sources and provenance

      Contract: 6e1489eb0437f011edf446e7339d375bda404d1517a65c12d3db88e88eeeeb96

      Item digest: 86e1d04d033535a8c92558d1206d86b9032daab481cb0b41dfbdc72641fd4800

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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