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

Quantum Information / Tensor Symmetry

Tensor Symmetry

Exercise PLAN-311

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

  • lambda has exactly two parts with lambda_1 at least lambda_2 at least zero.
  • The determinant representation sends a unitary to its determinant; the degree-m symmetric power of C^2 has dimension m plus one.

Question

For the two-dimensional unitary group, the irreducible pieces appearing in tensor powers of C^2 are indexed by partitions lambda = (lambda_1, lambda_2) with two parts. Prove that the dimension of the piece associated with such a partition equals lambda_1 minus lambda_2 plus one, and explain how this follows both from the semistandard-tableau count and from the explicit description of the piece as a determinant power times a symmetric power.

Hint: mathematical route

The two-dimensional unitary irreducible piece for a two-part partition has dimension lambda_1 minus lambda_2 plus one, from both tableau counting and the determinant-times-symmetric-power form.

  1. The dimension is the number of two-letter semistandard tableaux of shape lambda.
  2. Columns are forced 1 over 2; only the lambda_1 minus lambda_2 extra first-row cells vary.
  3. The piece is a one-dimensional determinant power times a degree-m symmetric power.
  4. The degree-m symmetric power of C^2 has dimension m plus one, agreeing with the count.
Reference solution

Semistandard count: the dimension equals the number of semistandard Young tableaux of shape lambda with entries from the two-letter alphabet {1,2}, that is fillings weakly increasing along rows and strictly increasing down columns. In the two-row shape the two cells of any column must be 1 above 2, which is forced; the only freedom is in the first row, which has lambda_1 minus lambda_2 cells beyond the part covered by the second row, and those cells must be weakly increasing in {1,2}, so they are some number of 1s followed by 2s. The number of such choices is lambda_1 minus lambda_2 plus one, giving the dimension. Explicit description: the piece is isomorphic to the determinant representation raised to the power lambda_2, tensored with the degree-m symmetric power of C^2, where m equals lambda_1 minus lambda_2. The determinant factor is one-dimensional, so it does not change the dimension; the symmetric power of degree m of a two-dimensional space has dimension m plus one. Hence the dimension is m plus one equal to lambda_1 minus lambda_2 plus one, matching the tableau count. Both routes agree because tensoring by the one-dimensional determinant shifts the highest weight without changing dimension, and the symmetric power is exactly the semistandard content of the first-row freedom.

Assessment rubric
  1. States the dimension equals the number of two-letter semistandard tableaux of shape lambda (1 weight)
  2. Shows the columns are forced to be 1 over 2 and the only freedom is the lambda_1 minus lambda_2 extra first-row cells, giving lambda_1 minus lambda_2 plus one fillings (1 weight)
  3. Gives the determinant-power-times-symmetric-power description and notes the determinant factor is one-dimensional (1 weight)
  4. Concludes the symmetric power of degree lambda_1 minus lambda_2 has dimension lambda_1 minus lambda_2 plus one, matching the tableau count (1 weight)

Graph-grounded prerequisites

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

  • Tensor networks (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: f63793eecf47d3f11605051b5d5b9b93d6a12fb81a38b37edfde45c811d7749b

Item digest: a540284076b09a2f0fe5e2a88254a5329ad87d91586c481043740ab5db00e80a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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