Tensor Symmetry
Exercise PLAN-308
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 basis vectors form a fixed basis of C^d.
- The totally antisymmetric subspace is the image of the signed average P.
Question
Let P be the antisymmetrizing projector on the n-fold tensor power of C^d, defined as the average over S_n of the sign of a permutation times the corresponding factor permutation. Prove that if d is strictly less than n then P annihilates the entire space, and interpret this as the statement that the totally antisymmetric subspace of the tensor power is zero whenever n exceeds d.
Hint: mathematical route
The antisymmetrizer on the n-fold tensor power of C^d is identically zero when n exceeds d, since no wedge of n distinct basis vectors exists.
- The image of P is spanned by wedges of basis vectors.
- A repeated index gives a vanishing wedge because the swap fixes the tensor yet flips its sign.
- Nonzero wedges require n distinct labels from the d-element alphabet.
- For n greater than d pigeonhole forbids distinct labels, so the antisymmetric subspace is zero and P is zero.
Reference solution
The image of P is the totally antisymmetric subspace, consisting of tensors that pick up the sign of any permutation when their factors are permuted. A spanning set for this image is obtained by antisymmetrizing basis tensors; the antisymmetrization of a basis tensor is, up to a scalar, the wedge of the chosen basis vectors. If two of the chosen indices coincide, this wedge is zero, because the transposition exchanging the two equal factors both fixes the tensor and multiplies it by minus one, forcing it to vanish. A nonzero antisymmetrized basis tensor therefore requires all n indices to be distinct, i.e. a strictly increasing choice of n labels drawn from the d-element alphabet. When n is greater than d there is no such choice: any n labels from a d-element set must repeat by the pigeonhole principle. Hence every antisymmetrized basis tensor is zero, the spanning set is trivial, the antisymmetric subspace is the zero subspace, and P is the zero operator. Equivalently its rank is the number of n-element subsets of a d-element set, which is zero for n greater than d.
Assessment rubric
- Identifies the image of P as the totally antisymmetric subspace and gives its spanning set by antisymmetrized basis tensors (1 weight)
- Shows a repeated index makes the antisymmetrized tensor vanish via the fixing-but-sign-flipping transposition (1 weight)
- Observes a nonzero antisymmetrized tensor needs n distinct labels from a d-element set (1 weight)
- Concludes by pigeonhole that n greater than d forces every spanning tensor to zero, so P is zero and the dimension vanishes (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)
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: 988d68c3196025855f6fcc732987a8a85c7e45261f1947aa2f965418fb34f4b0
Item digest: 961a255fe1a9311fd2c896ffa61b8256cbd38f180ff5a734a2dfeb558b1ed39b
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.