Tensor Symmetry
Exercise PLAN-301
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 and W are finite-dimensional complex vector spaces.
- End(V tensor W) is identified with End(V) tensor End(W); 1 denotes the identity on the indicated factor.
Question
Let V and W be finite-dimensional complex vector spaces and identify End(V tensor W) with End(V) tensor End(W). Consider the subalgebra A consisting of operators of the form a tensor 1 with a in End(V), where 1 is the identity on W. Prove that the commutant of A inside End(V tensor W), that is the set of all operators commuting with every element of A, is exactly the set of operators 1 tensor b with b in End(W).
Hint: mathematical route
The commutant of End(V) tensor 1 inside End(V tensor W) is exactly 1 tensor End(W), proved by a block-matrix argument.
- Operators 1 tensor b are block-scalar and commute with the block-diagonal a tensor 1.
- In a basis of W the commutation of T with every a tensor 1 forces each block to commute with every a.
- Only scalar multiples of the identity commute with all of End(V), so each block is a scalar times the identity.
- Collecting the scalar blocks shows T = 1 tensor c, proving the commutant is 1 tensor End(W).
Reference solution
Write n for the dimension of W and fix a basis of W, so every operator T on V tensor W becomes an n-by-n block matrix with blocks that are endomorphisms of V. In this basis a tensor 1 is block diagonal with the single block a repeated on the diagonal. First inclusion: any operator 1 tensor b has blocks that are scalar multiples of the identity on V, namely the entry of b times the identity, and these commute with the block-diagonal a tensor 1 because scalars commute with a; so every 1 tensor b lies in the commutant. Second inclusion: suppose a block operator T commutes with a tensor 1 for all a in End(V). Comparing blocks, the (i,j) block of (a tensor 1) T is a times the (i,j) block of T, while that of T (a tensor 1) is the (i,j) block of T times a, so block times a equals a times block for every a in End(V) and every pair i,j. An operator on V that commutes with all of End(V) must be a scalar multiple of the identity (apply the relation to rank-one operators, or use that the defining action of End(V) on V is irreducible). Hence each block equals a scalar times the identity on V, which means T = 1 tensor c where c in End(W) collects those scalars. Therefore the commutant equals the operators 1 tensor b, as claimed.
Assessment rubric
- States both inclusions must be shown and proves the easy direction that every 1 tensor b commutes with every a tensor 1 (1 weight)
- Introduces the block-matrix form in a basis of W and identifies a tensor 1 as block diagonal with repeated block a (1 weight)
- Derives from the commutation relation that each block commutes with every endomorphism of V (1 weight)
- Concludes each block is a scalar multiple of the identity because only scalars commute with all of End(V), giving T = 1 tensor c (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: db56cf5d64ff2d5c14d60f74805325e42cc3e3801ad70cb9fc7a670bca07c92e
Item digest: b584bed80a1e10178eb2030fccf506dbf434129c43df6e2d8bfdb6f12531583e
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.