The symmetric tensors are spanned by the pure powers

The symmetric group of ι acts on the tensor power ⨂[R] (_ : ι), M by permuting the factors. This file identifies the invariants of that action, once (#ι)! is invertible in R: they are exactly the span of the pure powers ⨂ₜ i, x, the tensors with the same vector in every slot.

The engine is the polarization identity PiTensorProduct.sum_neg_one_pow_card_smul_tprod_sum_compl, which writes the full symmetrization of a pure tensor as an alternating sum of pure powers and needs no invertibility. Dividing by (#ι)! then turns the symmetrization into a projection onto the invariants; that step is not special to permutations of tensor factors, and is taken here from Representation.range_norm_eq_invariants, which says that the group sum of any finite-group representation has the invariants as its range once the group order is invertible.

This is the spanning half of the double centralizer in Schur-Weyl duality. There ι is finite and V is a finite free module, so that the canonical map (End V)^{⊗ι} → End (V^{⊗ι}) is an isomorphism; the results below need neither hypothesis on M. Under that identification the endomorphisms commuting with the factor permutations are the invariants of the permutation action on (End V)^{⊗ι}, and this file says they are spanned by the pure powers f^{⊗ι} — the diagonal operators through which the general linear group acts.

Main results

• PiTensorProduct.invariants_reindexRepresentation: the invariants of the permutation action on the tensor power are the span of the pure powers, when (#ι)! is invertible.
• PiTensorProduct.range_sum_reindexRepresentation: the symmetrization operator has that same span as its range.
• SymmetricPower.range_toTensorPower_eq_span: consequently the symmetric power sits inside the tensor power as the span of the pure powers.
• TauCeti.invariants_permTensorAction and TauCeti.range_permTensorActionAlgHom_sum_single: the statement specialized to the S_d-action on (Rⁿ)^{⊗d}, the setting of Schur-Weyl duality, in its invariant-subspace and its group-algebra-image forms.

References

• Schur--Weyl roadmap, Layer 8, “The double centralizer (image-level)”: the centralizer of the symmetric-group image in End((ℂᵈ)^{⊗n}) is the image of ℂ[GLₔ], whose spanning half is the identification proved here.
• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6, and Appendix B.1 for the polarization argument.

theorem PiTensorProduct.tprod_const_mem_invariants {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] (x : M) : ((tprod R) fun (x_1 : ι) => x) ∈ (reindexRepresentation R M ι).invariants

A pure power ⨂ₜ i, x is fixed by every permutation of the tensor factors.

theorem PiTensorProduct.sum_reindexRepresentation_mem_span {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (y : PiTensorProduct R fun (x : ι) => M) : ∑ σ : Equiv.Perm ι, ((reindexRepresentation R M ι) σ) y ∈ Submodule.span R (Set.range fun (x : M) => (tprod R) fun (x_1 : ι) => x)

Symmetrizing any tensor lands in the span of the pure powers.

theorem PiTensorProduct.range_sum_reindexRepresentation {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (h : IsUnit ↑(Fintype.card ι).factorial) : (∑ σ : Equiv.Perm ι, (reindexRepresentation R M ι) σ).range = Submodule.span R (Set.range fun (x : M) => (tprod R) fun (x_1 : ι) => x)

The symmetrization operator has the symmetric tensors as its range. The range of ∑_σ σ is the span of the pure powers; the operator scales an invariant tensor by (#ι)!, so it is the projection onto that span only up to that factor.

@[simp]

theorem PiTensorProduct.invariants_reindexRepresentation {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommGroup M] [Module R M] [Fintype ι] (h : IsUnit ↑(Fintype.card ι).factorial) : (reindexRepresentation R M ι).invariants = Submodule.span R (Set.range fun (x : M) => (tprod R) fun (x_1 : ι) => x)

The symmetric tensors are the span of the pure powers. When (#ι)! is invertible in R, the invariants of the permutation action on ⨂[R] (_ : ι), M are spanned by the pure powers ⨂ₜ i, x.

theorem SymmetricPower.range_toTensorPower_eq_span {R : Type u} {M : Type v} {ι : Type u} [CommRing R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (h : IsUnit ↑(Fintype.card ι).factorial) : (toTensorPower R ι M).range = Submodule.span R (Set.range fun (x : M) => (PiTensorProduct.tprod R) fun (x_1 : ι) => x)

The symmetric power sits inside the tensor power as the span of the pure powers. The symmetrization SymmetricPower.toTensorPower has as its image the span of the tensors ⨂ₜ i, x.

Together with SymmetricPower.toTensorPower_injective this presents Sym[R] ι M concretely: it is the subspace of ⨂[R] (_ : ι), M generated by the pure powers. The index type is confined to the universe of R because SymmetricPower is.

@[simp]

theorem TauCeti.invariants_permTensorAction {R : Type u} {n d : ℕ} [CommRing R] (h : IsUnit ↑d.factorial) : (permTensorAction R n d).invariants = Submodule.span R (Set.range fun (x : Fin n → R) => (PiTensorProduct.tprod R) fun (x_1 : Fin d) => x)

The symmetric tensors in (Rⁿ)^{⊗d}. The invariants of the S_d-action permuting the tensor factors are spanned by the pure powers ⨂ₜ i, x; this is the spanning half of the Schur-Weyl double centralizer, read on the tensor power itself.

theorem TauCeti.range_permTensorActionAlgHom_sum_single {R : Type u} {n d : ℕ} [CommRing R] (h : IsUnit ↑d.factorial) : LinearMap.range ((permTensorActionAlgHom R n d) (∑ σ : Equiv.Perm (Fin d), MonoidAlgebra.single σ 1)) = Submodule.span R (Set.range fun (x : Fin n → R) => (PiTensorProduct.tprod R) fun (x_1 : Fin d) => x)

The symmetrizer of R[S_d] cuts out the same subspace. The image of the group-algebra element ∑_σ σ acting on (Rⁿ)^{⊗d} is the span of the pure powers, hence the invariants: it is the projection onto them, up to the factor d!. This is the Young symmetrizer of a one-row shape, read at the level of the image subalgebra of R[S_d] in which Schur-Weyl duality is stated.