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

Quantum Information / Representation Qit

Representation Qit

Exercise PLAN-111

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 for X in L(V) define the symmetrized operator Xbar := (1/|G|) sum_{g in G} phi(g) X phi(g)^{-1}. (a) Prove that Xbar is G-invariant, i.e. phi(h) Xbar = Xbar phi(h) for all h in G. (b) Using Schur's Lemma, prove that if V = W_1 (+) W_2 is a multiplicity-free decomposition into two inequivalent irreducibles, then in a basis adapted to W_1, W_2 the operator Xbar is block diagonal with each diagonal block a scalar multiple of the identity, and the off-diagonal blocks vanish. Explain which part of Schur kills the off-diagonal blocks and which part scalarizes the diagonal blocks.

      Hint: mathematical route

      Group-averaging an operator produces an equivariant operator that, on a multiplicity-free decomposition into two inequivalent irreps, is block diagonal with scalar diagonal blocks (Schur ii) and vanishing off-diagonal blocks (Schur i).

      1. Reindexing g -> hg gives phi(h) Xbar phi(h)^{-1} = Xbar, so Xbar commutes with the representation.
      2. Block A_{ij} satisfies A_{ij} phi_j(h) = phi_i(h) A_{ij}: an intertwiner W_j -> W_i.
      3. Schur (i): off-diagonal intertwiners between inequivalent irreps vanish, A_{12}=A_{21}=0.
      4. Schur (ii) over C: each A_{ii} = lambda_i 1_{W_i}, so Xbar = lambda_1 1_{W_1} (+) lambda_2 1_{W_2}.
      Reference solution

      (a) For h in G, phi(h) Xbar phi(h)^{-1} = (1/|G|) sum_g phi(h)phi(g) X phi(g)^{-1}phi(h)^{-1} = (1/|G|) sum_g phi(hg) X phi(hg)^{-1}. Reindexing g' = hg (a bijection of G) leaves the average unchanged, so phi(h) Xbar phi(h)^{-1} = Xbar, i.e. phi(h) Xbar = Xbar phi(h). Thus Xbar commutes with the whole representation; it is G-equivariant. (b) Write Xbar in block form with respect to V = W_1 (+) W_2: Xbar = [[A_{11}, A_{12}], [A_{21}, A_{22}]], where A_{ij}: W_j -> W_i. Equivariance phi(h) Xbar = Xbar phi(h) restricted to blocks says A_{ij} phi_j(h) = phi_i(h) A_{ij} for all h, i.e. each A_{ij} is an intertwiner from the irreducible W_j to the irreducible W_i. For the off-diagonal blocks i != j: W_1 and W_2 are inequivalent irreducibles, so by Schur part (i) any intertwiner between them is zero; hence A_{12} = 0 and A_{21} = 0. For the diagonal blocks i = j: A_{ii} is an equivariant endomorphism of the irreducible W_i over C, so by Schur part (ii) A_{ii} = lambda_i . 1_{W_i} for some scalar lambda_i. Therefore Xbar = lambda_1 1_{W_1} (+) lambda_2 1_{W_2}, block diagonal with scalar blocks. Part (i) of Schur kills the off-diagonal blocks (maps between inequivalent irreps), and part (ii) scalarizes the diagonal blocks (equivariant endomorphisms of an irrep). This is exactly the small multiplicity-free instance of the general symmetrization result; with multiplicities the diagonal blocks would instead be 1_{W_k} tensored with an arbitrary operator on the multiplicity space.

      Assessment rubric
      1. Proves phi(h) Xbar phi(h)^{-1} = Xbar via the reindexing g -> hg, so Xbar is G-equivariant (1 weight)
      2. Translates the block A_{ij} into an intertwiner W_j -> W_i using equivariance (1 weight)
      3. Uses Schur (i) and inequivalence of W_1, W_2 to force the off-diagonal blocks A_{12} = A_{21} = 0 (1 weight)
      4. Uses Schur (ii) over C to make each diagonal block A_{ii} = lambda_i 1_{W_i}, giving the scalar block-diagonal form and naming which part of Schur does which (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: fc5b37f207f44c9f961a13d0ce0adb94e838a9080a2c185d593ef1ccddf07100

      Item digest: 5c86b4af86f4716aeec0f5399496dacdd9f853ece3b24ed6d0c0810ec154546e

      Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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