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

Quantum Information / Tensor Symmetry

Tensor Symmetry

Exercise PLAN-302

advanced · 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

  • The representation is of a finite group on a finite-dimensional complex space; the pieces V_alpha are pairwise inequivalent irreducibles.
  • Direct sums are over the distinct irreducible types alpha; the identity is taken on the indicated factor.

Question

Let a finite group act on a finite-dimensional space V with isotypical decomposition V = direct sum over alpha of (V_alpha tensor C^{n_alpha}) into pairwise inequivalent irreducible pieces V_alpha appearing with multiplicity n_alpha. Let A be the algebra of operators generated by the representation. Prove that the commutant A' equals the direct sum over alpha of (1 on V_alpha, tensored with End(C^{n_alpha})), and deduce that the double commutant equals A.

Hint: mathematical route

For an isotypical representation the commutant is the sum of multiplicity-space endomorphism algebras and the double commutant recovers A.

  1. Central isotypical projections lie in A, forcing elements of A' to be block diagonal.
  2. On each block A acts as endomorphisms of V_alpha with the multiplicity factor untouched.
  3. The tensor commutant lemma gives A' as the direct sum of multiplicity-space endomorphism algebras.
  4. Taking the commutant of A' blockwise returns End(V_alpha) tensor identity, so the double commutant equals A.
Reference solution

The isotypical projections onto the summands V_alpha tensor C^{n_alpha} lie in A, so any element b of the commutant A' commutes with each such projection and is therefore block diagonal: b is a direct sum of pieces b_alpha, each an endomorphism of V_alpha tensor C^{n_alpha}. On the alpha block the algebra A restricts to (End(V_alpha) tensored with the identity on the multiplicity space): the irreducible action on V_alpha with the multiplicity factor left untouched. By the commutant lemma for a tensor product, the commutant of (End(V_alpha) tensor identity) inside End(V_alpha tensor C^{n_alpha}) is (identity on V_alpha, tensored with End(C^{n_alpha})); hence each b_alpha has this form and A' is the stated direct sum. Conversely every such operator commutes with A, so this is an equality. Applying the same commutant lemma a second time: the commutant of (identity on V_alpha tensor End(C^{n_alpha})) inside each block is (End(V_alpha) tensor identity), and summing over alpha shows the double commutant equals the direct sum of (End(V_alpha) tensor identity), which is A. Thus the bicommutant recovers A.

Assessment rubric
  1. Uses that the isotypical projections lie in A to show any element of A' is block diagonal across the alpha summands (1 weight)
  2. Identifies the restriction of A to the alpha block as endomorphisms of V_alpha with an untouched multiplicity factor (1 weight)
  3. Applies the tensor commutant lemma to get the multiplicity-space form of each block, hence A' is the stated direct sum (1 weight)
  4. Applies the commutant lemma a second time to the description of A' and sums over alpha to conclude the double commutant equals A (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: 0ceba1be0865dc81c5e24b6a5a526cbc3e1b2f262ae7efb734c256207e9db8ac

Item digest: eb90a4aa9096df7cd80102628985d2c7e4cf136eef91dcbf0eff10fed5c1451a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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