Tensor Symmetry
Exercise PLAN-306
primary source nl only. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- V is finite-dimensional, so finite-dimensional subspaces are closed.
- A single-vector power repeats the same vector v in each of the n factors.
Question
Let V be a finite-dimensional complex vector space and let the symmetric subspace of its n-fold tensor power be the set of tensors fixed by every permutation of the n factors. Prove that this symmetric subspace equals the span of the n-fold powers of single vectors v of V.
Hint: mathematical route
The symmetric subspace of a tensor power is spanned by the n-fold powers of single vectors, proved by polarization and a closedness argument.
- Single-vector powers are permutation invariant, so their span lies in the symmetric subspace.
- Symmetrized basis tensors span the symmetric subspace.
- Each symmetrizer is a polarization: a mixed derivative of a single-vector power.
- Derivatives are limits of difference quotients in the closed finite-dimensional span, so the symmetric subspace lies in W.
Reference solution
Call the span of the single-vector powers W. One inclusion is immediate: each n-fold power of a single vector is unchanged by any factor permutation, so W is contained in the symmetric subspace. For the reverse inclusion, start from the standard spanning set of the symmetric subspace obtained by symmetrizing basis tensors: for a basis of V the symmetrized basis tensors, each a sum over all permutations of a fixed arrangement of basis vectors, span the symmetric subspace. These symmetrized tensors are polarizations: each equals a mixed partial derivative, evaluated at the origin, of the single-vector power of a vector of the form (first basis vector plus t_2 times second plus ... plus t_n times last), differentiated once in each of t_2, ..., t_n. Each such derivative is a limit of difference quotients of elements that are themselves n-fold powers of single vectors, all of which lie in W. Because V is finite-dimensional, W is a finite-dimensional and hence closed subspace, so these limits remain in W. Therefore every symmetrizer, and thus the whole symmetric subspace, lies in W, giving equality.
Assessment rubric
- Proves the easy inclusion that each single-vector power is permutation invariant, so the span W sits inside the symmetric subspace (1 weight)
- Recalls that symmetrized basis tensors span the symmetric subspace (1 weight)
- Expresses each symmetrized tensor as a mixed partial derivative (polarization) of a single-vector power (1 weight)
- Argues the derivative is a limit of difference quotients of single-vector powers in W, which is closed, so the symmetric subspace lies in W (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)
- Operator and semigroup theory (frozen curriculum anchor; see graph 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.
Sources and provenance
- website/research/sources.json
leditzky-2025-repth-qit
Source SHA-256:9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae· MIT metadata only - Primary source
Contract: 5782b744701d9d5573539b4b70696805f88528ae16daf12227e5cea80493d274
Item digest: 2c32e94daf140024914e71c5bb19e6cb754e24a522a54d1322c60d4271403a04
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.