The commutant of the permutation action on a tensor power

The symmetric group of ι acts on ⨂[R] (_ : ι), M by permuting the tensor factors, and every diagonal endomorphism f^{⊗ι} = PiTensorProduct.map (fun _ ↦ f) commutes with that action (PiTensorProduct.commute_reindexRepresentation_map). This file proves the converse when M is finite projective and (#ι)! is invertible in R: an endomorphism of the tensor power commuting with all the factor permutations is an R-linear combination of diagonal ones.

That is one half of the double centralizer of Schur-Weyl duality, at the level of image subalgebras: the commutant of the image of R[S_ι] in End (M^{⊗ι}) is the span of the diagonal operators, through which the general linear group acts.

The proof runs the computation on the other side of the comparison isomorphism PiTensorProduct.piTensorHomEquiv, which identifies End (M^{⊗ι}) with (End M)^{⊗ι}. Under that identification conjugation by a factor permutation on End (M^{⊗ι}) becomes the permutation action on (End M)^{⊗ι}, so a commuting endomorphism is an invariant tensor; and the invariants of a permutation action are the span of the pure powers (PiTensorProduct.invariants_reindexRepresentation), which are exactly the diagonal operators. Both hypotheses are used once: projectivity and finiteness make the comparison map an isomorphism, and the invertibility of (#ι)! is what averaging over the symmetric group needs.

Main results

• PiTensorProduct.piTensorHomEquiv_reindexRepresentation_mul: the comparison isomorphism intertwines the permutation action on (End M)^{⊗ι} with conjugation by the factor permutations on End (M^{⊗ι}).
• PiTensorProduct.mem_span_range_map_const_iff_forall_commute: the commutant of the permutation action is the span of the diagonal operators.
• TauCeti.mem_span_range_map_const_iff_forall_commute_permTensorAction: the same statement in the Schur-Weyl setting M = Rⁿ, ι = Fin d, where the invertibility hypothesis reads d !.

References

• Schur--Weyl roadmap, Layer 8, "The double centralizer (image-level)", whose first half asks for exactly the commutant of the symmetric-group image inside End (V^{⊗n}). The other half, that the commutant of the diagonal operators is the symmetric-group image, is not proved here.
• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6 and Appendix B.1.

theorem PiTensorProduct.piTensorHomEquiv_reindexRepresentation_tprod_mul {R : Type u} {M : Type v} {ι : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Finite ι] [Module.Projective R M] [Module.Finite R M] (σ : Equiv.Perm ι) (f : ι → M →ₗ[R] M) : (piTensorHomEquiv R (fun (x : ι) => M) fun (x : ι) => M) (((reindexRepresentation R (M →ₗ[R] M) ι) σ) ((tprod R) f)) * (reindexRepresentation R M ι) σ = (reindexRepresentation R M ι) σ * (piTensorHomEquiv R (fun (x : ι) => M) fun (x : ι) => M) ((tprod R) f)

The comparison isomorphism carries a permuted pure tensor to the conjugated map. This is the pure-tensor case of PiTensorProduct.piTensorHomEquiv_reindexRepresentation_mul, and is Mathlib's compatibility of PiTensorProduct.map with PiTensorProduct.reindex.

theorem PiTensorProduct.piTensorHomEquiv_reindexRepresentation_mul {R : Type u} {M : Type v} {ι : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [Finite ι] [Module.Projective R M] [Module.Finite R M] (σ : Equiv.Perm ι) (x : PiTensorProduct R fun (x : ι) => M →ₗ[R] M) : (piTensorHomEquiv R (fun (x : ι) => M) fun (x : ι) => M) (((reindexRepresentation R (M →ₗ[R] M) ι) σ) x) * (reindexRepresentation R M ι) σ = (reindexRepresentation R M ι) σ * (piTensorHomEquiv R (fun (x : ι) => M) fun (x : ι) => M) x

The comparison isomorphism intertwines the two actions. Permuting the factors of a tensor of endomorphisms is conjugating the corresponding endomorphism of the tensor power by the permutation of the factors.

theorem PiTensorProduct.mem_span_range_map_const_iff_forall_commute {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] [Module.Projective R M] [Module.Finite R M] (h : IsUnit ↑(Fintype.card ι).factorial) (T : (PiTensorProduct R fun (x : ι) => M) →ₗ[R] PiTensorProduct R fun (x : ι) => M) : T ∈ Submodule.span R (Set.range fun (f : M →ₗ[R] M) => map fun (x : ι) => f) ↔ ∀ (σ : Equiv.Perm ι), Commute T ((reindexRepresentation R M ι) σ)

The commutant of the permutation action on a tensor power is the span of the diagonal operators. For a finite projective module M and (#ι)! invertible in R, an endomorphism of ⨂[R] (_ : ι), M commutes with every permutation of the tensor factors exactly when it is an R-linear combination of the operators f^{⊗ι} applying one endomorphism f in every factor.

One direction is PiTensorProduct.commute_reindexRepresentation_map; the substance is the other, which says that the diagonal operators already exhaust the commutant.

theorem TauCeti.mem_span_range_map_const_iff_forall_commute_permTensorAction {R : Type u_1} {n d : ℕ} [CommRing R] (h : IsUnit ↑d.factorial) (T : (PiTensorProduct R fun (x : Fin d) => Fin n → R) →ₗ[R] PiTensorProduct R fun (x : Fin d) => Fin n → R) : T ∈ Submodule.span R (Set.range fun (f : (Fin n → R) →ₗ[R] Fin n → R) => PiTensorProduct.map fun (x : Fin d) => f) ↔ ∀ (σ : Equiv.Perm (Fin d)), Commute T ((permTensorAction R n d) σ)

The commutant of the symmetric group on (Rⁿ)^{⊗d}, the Schur-Weyl reading of PiTensorProduct.mem_span_range_map_const_iff_forall_commute: when d ! is invertible in R, the endomorphisms of (Rⁿ)^{⊗d} commuting with the permutations of the tensor factors are exactly the R-linear combinations of the diagonal operators f^{⊗d}, through which the general linear group acts.