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

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-102

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, and let <.|.> be any inner product on V. Define the averaged form <v|w>_G := (1/|G|) sum_{g in G} <phi(g) v | phi(g) w>. Prove that (a) <.|.>_G is again an inner product on V; (b) every phi(g) is unitary with respect to <.|.>_G, i.e. <phi(g) v | phi(g) w>_G = <v|w>_G; and (c) consequently, for any G-invariant subspace W, its orthogonal complement W^perp taken with respect to <.|.>_G is also G-invariant, so that V = W (+) W^perp as representations. Explain exactly where the ability to average over G is used.

      Hint: mathematical route

      Averaging an arbitrary inner product over a finite group yields a G-invariant inner product making the representation unitary, so orthogonal complements of invariant subspaces are invariant.

      1. Each term <phi(g)v|phi(g)w> is sesquilinear/Hermitian; the g=e term gives definiteness, so <.|.>_G is an inner product.
      2. <phi(h)v|phi(h)w>_G = (1/|G|) sum_g <phi(gh)v|phi(gh)w> by the homomorphism property.
      3. Reindexing g'=gh (a bijection of G) shows the average is unchanged, so phi(h) is unitary for <.|.>_G.
      4. Unitarity gives phi(g)^* = phi(g^{-1}); for u in W^perp, w in W, <phi(g)u|w>_G = <u|phi(g^{-1})w>_G = 0.
      5. Hence W^perp is G-invariant and V = W (+) W^perp as representations.
      Reference solution

      (a) Each summand <phi(g)v | phi(g)w> is sesquilinear in (v,w) because phi(g) is linear and <.|.> is sesquilinear, and a finite average of sesquilinear forms is sesquilinear; Hermitian symmetry is inherited termwise. For positivity, <v|v>_G = (1/|G|) sum_g <phi(g)v | phi(g)v> >= 0 as an average of nonnegative terms, and it vanishes only if every term is 0; the g = e term gives <v|v> = 0, hence v = 0 since <.|.> is definite. So <.|.>_G is a genuine inner product. (b) Fix h in G. Then <phi(h)v | phi(h)w>_G = (1/|G|) sum_g <phi(g)phi(h)v | phi(g)phi(h)w> = (1/|G|) sum_g <phi(gh)v | phi(gh)w> by the homomorphism property. As g ranges over G so does g' = gh (left translation is a bijection of G), so the sum equals <v|w>_G. Thus phi(h) preserves <.|.>_G and is unitary for it. (c) Let W be G-invariant and u in W^perp. For any g and w in W, <phi(g)u | w>_G = <u | phi(g)^* w>_G = <u | phi(g^{-1}) w>_G, using that the adjoint of the <.|.>_G-unitary phi(g) is phi(g)^{-1} = phi(g^{-1}). Invariance gives phi(g^{-1}) w in W, so the pairing is 0; hence phi(g)u in W^perp and W^perp is invariant. Then V = W (+) W^perp (nondegeneracy) with both summands invariant, a decomposition of representations. The averaging over G is used exactly twice: forming the normalized sum (1/|G|) sum_g requires it to be finite (compact groups replace it by Haar integration), and the reindexing g -> gh being a bijection is what makes the form G-invariant.

      Assessment rubric
      1. Shows <.|.>_G is sesquilinear, Hermitian, and positive-definite, using the g=e term for definiteness (1 weight)
      2. Proves G-invariance of <.|.>_G via the homomorphism property and the reindexing g -> gh being a bijection of G (1 weight)
      3. Deduces each phi(g) is unitary for <.|.>_G and uses phi(g)^* = phi(g^{-1}) to show W^perp is invariant when W is (1 weight)
      4. Concludes V = W (+) W^perp as representations and pinpoints the normalized average and reindexing as the essential ingredient (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)

      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: 4be28fa01317b8110e1a5e0161eeeaa5dba62404b5634e1571e05954b813eb0a

      Item digest: 4aa8a582922a72a46c4a3189cc1902dd7961a753460a2c5189793a0372a0dff8

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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