Exercise PLAN-304

The permutation algebra and the algebra spanned by the common GL(V) action g^tensor(n) are mutual commutants. Pure-tensor commutation and interpolation from invertible shifts prove the GL claim without a unitary-only span substitution.

1. Every common endomorphism action X^tensor(n) commutes with factor permutations, so in particular the GL-generated B lies in A'.
2. The given A'=span{X^tensor(n)} reduces the reverse inclusion to arbitrary endomorphism powers, including singular X.
3. Outside finitely many complex shift values X+tI is invertible, so choose n+1 distinct such points with their tensor powers in the GL algebra B.
4. The operator-valued polynomial F(t)=(X+tI)^tensor(n) has degree at most n; Lagrange interpolation at those distinct points puts F(0)=X^tensor(n) in B.
5. Hence B=A'; A is the finite-group image unital star algebra, so A''=A and B'=A, with empty/zero tensor cases understood separately.

Use the question's exact algebra B=span_C{g^tensor(n):g in GL(V)}; 'diagonal action' here means the SAME g acts on every tensor factor, not that g is a diagonal matrix or necessarily a unitary. Write Q_pi for the factor-permutation action. For every endomorphism X, Q_pi X^tensor(n)=X^tensor(n) Q_pi: on a pure tensor both sides apply X to each factor and put the factors in the same permuted positions. Pure tensors span, so this is an operator equality for all X. In particular it holds for every invertible g, not merely unitary g. Hence every generator of B commutes with A, giving B subset A'.

For the reverse inclusion use the GIVEN description A'=span_C{X^tensor(n):X in End(V)}. Fix any such X, including a singular one. If d>0, det(X+tI) is a monic scalar polynomial of degree d, so only finitely many complex t make X+tI singular. Choose n+1 distinct complex numbers t_0,...,t_n outside that finite set. Every F(t_j)=(X+t_j I)^tensor(n) then belongs to B by its definition using GL(V). The operator-valued polynomial F(t) has degree AT MOST n: expand the n factors, collecting the finitely many terms with each power of t. Lagrange interpolation applies coefficientwise in this finite-dimensional operator space, and gives F(0)=sum_{j=0}^n ell_j(0)F(t_j), where ell_j(t)=product_{k!=j}(t-t_k)/(t_j-t_k). The denominators are nonzero because the sample points are distinct. B is a complex linear subspace, so F(0)=X^tensor(n) lies in B. Thus the span of all such powers, A', is contained in B. Together the inclusions prove B=A'.

Finally A is the finite-dimensional unital star algebra spanned by the permutation representation of the finite group S_n: products stay in the group image, the identity is present, and Q_pi^dagger=Q_(pi^-1). Thus the finite-dimensional double-commutant theorem applies to THIS algebra and gives A''=A; it is not asserted for arbitrary non-self-adjoint subalgebras. Since B=A', we obtain B'=A''=A, as requested.

For n=0 the tensor power is C, both algebras are the scalar algebra and F is constant; one interpolation sample suffices. If V=0 and n>0 the ambient tensor power and endomorphism algebra are zero and the conclusion is trivial; this avoids asserting an exact nonzero polynomial degree in a zero operator space. No d>=n premise is needed. The source Prop4.10/Eq4.15-4.16 proof is a GL(V) argument. The historical word 'unitary' in its first inclusion is insufficient wording for the defined B, but the pure-tensor computation above establishes the full GL inclusion directly. A separate unitary-only spanning theorem can be true, but it is NOT proved merely because X+tI is invertible: those interpolation samples need not be unitary. No such bridge is assumed or needed here. This is an algebraic mutual-commutant proof, not an efficient Schur-transform algorithm, fresh Lean result or source-publication approval.

1. Uses B=span{g^tensor(n):g in GL(V)} and proves factor-permutation commutation for every g (indeed every endomorphism), not only unitary generators. (1 weight)
2. Uses the explicitly given A' characterization to reduce the reverse inclusion to every endomorphism power, including singular X. (1 weight)
3. Uses det(X+tI) to choose n+1 distinct invertible shifts over C and places their powers in the GL-defined algebra B, without treating these shifts as necessarily unitary. (1 weight)
4. Treats F(t) as an operator-valued polynomial of degree at most n and applies valid Lagrange interpolation at distinct points to obtain X^tensor(n) in B. (1 weight)
5. Combines both inclusions and applies the finite-dimensional group-image/unital-star bicommutant theorem to A to get B'=A; preserves zero/empty boundaries and adds no unitary-only or d>=n premise. (1 weight)

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

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: 0a1210e64058fbc9844b798192122398397094a6ce67c6c6af5192f14476ae61

Item digest: 63d0ffabef4e6aad5e2c9a64947cf393005f177424421361257150e9326c07b2

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "8c71082c4fb736eefc753e15be5f10fee4e9608aa150fb873a1b2c6cec31a677", "predecessor_key": "qcb-core-plan-304-schur-weyl-mutual-commutant", "repair_record": "shared/repairs/plan-304-gl-action-clarification-repair.json", "repair_record_digest": "10c7a95815b55413a3f292826b15174f06ce558e4d3a47c26304f56f57c5adf2", "review_record": "reports/textbook-v1/repairs/plan-304-gl-action-clarification-repair-review.json", "review_digest": "88afa4390d9eff4c0d240f1965c6da67d9082c26e0790774f0d34a783132c5be" }