Schur-Weyl duality: the symmetric-group image and the diagonal span are mutual commutants

The symmetric group S_d acts on (kⁿ)^{⊗d} by permuting the tensor factors, the diagonal operators f^{⊗d} act by applying one endomorphism of kⁿ in every factor, and the two actions commute (PiTensorProduct.commute_reindexRepresentation_map). Schur-Weyl duality says that inside End_k ((kⁿ)^{⊗d}) the two spans are exactly each other's commutants.

One half is already available: TauCeti.mem_span_range_map_const_iff_forall_commute_permTensorAction says that the commutant of the symmetric-group action is the span of the diagonal operators, and it needs only that d ! is invertible. This file records that half as an identity of centralizers (TauCeti.coe_centralizer_range_permTensorActionAlgHom_eq_span_range_map_const) and proves the other half, which needs semisimplicity: over a field in which d ! is nonzero, an endomorphism commuting with every diagonal operator already lies in the image of the group algebra k[S_d].

The argument

The image A of k[S_d] in End_k ((kⁿ)^{⊗d}) is a quotient of k[S_d], which is semisimple by Maschke's theorem, so the double centralizer theorem AlgHom.centralizer_centralizer_range applies and gives A'' = A. The commutant A' is the span of the diagonal operators by the half already available, so A is the commutant of that span.

The distinction between k[S_d] and its image is not cosmetic: the algebra map k[S_d] → End_k ((kⁿ)^{⊗d}) is injective only when d ≤ n (TauCeti.permTensorActionAlgHom_injective_iff), so the commutant of the diagonal operators is the image of k[S_d] and not k[S_d] itself. The statements below are accordingly about AlgHom.range.

Relation to the general-linear image

Every statement below takes the span of the diagonal operators f^{⊗d} over all f : kⁿ →ₗ[k] kⁿ, matching the half already proved. The general linear group acts through the subfamily of g^{⊗d} with g invertible. The downstream module TauCeti/RepresentationTheory/Symmetric/TensorAction/GeneralLinear.lean proves that these already span everything (TauCeti.toSubmodule_range_tensorPowerRep_asAlgebraHom_eq_span_range_map_const) and deduces the image-level mutual commutants, including TauCeti.centralizer_range_tensorPowerRep_asAlgebraHom_eq_range_permTensorActionAlgHom. The results in this file are the span-level input to that identification.

Main results

• TauCeti.coe_centralizer_range_permTensorActionAlgHom_eq_span_range_map_const: the commutant of the symmetric-group image is the span of the diagonal operators.
• TauCeti.centralizer_span_range_map_const_eq_range_permTensorActionAlgHom: the commutant of the diagonal operators is the symmetric-group image, the half that needs semisimplicity.
• TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute: the same statement as a membership criterion, x acting as an element of k[S_d] exactly when it commutes with every diagonal operator.

References

• Schur--Weyl roadmap, Layer 8, "The double centralizer (image-level)", of which this file proves the form with all diagonal operators in place of the image of k[GLₙ].
• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6 and Appendix B.1.
• C. Procesi, Lie Groups: An Approach through Invariants and Representations, Chapter 9.

theorem TauCeti.coe_centralizer_range_permTensorActionAlgHom_eq_span_range_map_const {R : Type u_1} {n d : ℕ} [CommRing R] (h : IsUnit ↑d.factorial) : ↑(Subalgebra.centralizer R ↑(permTensorActionAlgHom R n d).range) = ↑(Submodule.span R (Set.range fun (f : (Fin n → R) →ₗ[R] Fin n → R) => PiTensorProduct.map fun (x : Fin d) => f))

The commutant of the symmetric-group image is the span of the diagonal operators. This is TauCeti.mem_span_range_map_const_iff_forall_commute_permTensorAction read as an identity of centralizers rather than as a membership criterion: passing from the permutations to the group algebra they span does not change the commutant.

@[simp]

theorem TauCeti.centralizer_span_range_map_const_eq_range_permTensorActionAlgHom {k : Type u_1} {n d : ℕ} [Field k] [NeZero ↑d.factorial] : Subalgebra.centralizer k ↑(Submodule.span k (Set.range fun (f : (Fin n → k) →ₗ[k] Fin n → k) => PiTensorProduct.map fun (x : Fin d) => f)) = (permTensorActionAlgHom k n d).range

Schur-Weyl duality. Over a field in which d ! is nonzero, the commutant of the diagonal operators f^{⊗d} on (kⁿ)^{⊗d}, taken over all endomorphisms f of kⁿ, is exactly the image of the group algebra k[S_d] acting by permuting the tensor factors.

Together with TauCeti.coe_centralizer_range_permTensorActionAlgHom_eq_span_range_map_const, which computes the commutant in the other direction, this says that the symmetric-group image and the span of the diagonal operators are each other's commutants. The general linear group acts through the invertible g^{⊗d}. The downstream theorem TauCeti.toSubmodule_range_tensorPowerRep_asAlgebraHom_eq_span_range_map_const proves that these span the same subalgebra, and TauCeti.centralizer_range_tensorPowerRep_asAlgebraHom_eq_range_permTensorActionAlgHom gives the resulting commutant of the image of k[GLₙ].

theorem TauCeti.mem_range_permTensorActionAlgHom_iff_forall_commute {k : Type u_1} {n d : ℕ} [Field k] [NeZero ↑d.factorial] (x : Module.End k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) : x ∈ (permTensorActionAlgHom k n d).range ↔ ∀ (f : (Fin n → k) →ₗ[k] Fin n → k), Commute x (PiTensorProduct.map fun (x : Fin d) => f)

Schur-Weyl duality, as a membership criterion. An endomorphism of (kⁿ)^{⊗d} is the action of an element of the group algebra k[S_d] exactly when it commutes with every diagonal operator f^{⊗d}.