Invariants of the reflection representation of the symmetric group

Let σ be a finite set with n + 1 elements, and let K[σ] be the permutation representation of the symmetric group S_σ. Its reflection representation is the standard representation TauCeti.standardRepresentation on the trace-zero hyperplane V₀ ⊆ K[σ] of vectors whose coefficients sum to zero. This file computes the invariant polynomial functions on V₀, that is the invariants of Sym(V₀*) under the contragredient action.

Polynomial functions on V₀ are restrictions of polynomial functions on K[σ]: restriction of linear forms K[σ]* → V₀* induces a map of symmetric algebras whose kernel, over every commutative ring, is the ideal generated by the invariant linear form e₁ = ∑ᵢ xᵢ, the coefficient sum (TauCeti.ker_map_dualRestrict_augmentation). When n + 1 is invertible in K, K[σ] is the direct sum of V₀ and the invariant line spanned by ∑ᵢ i, so this restriction has an equivariant section, and every invariant on V₀ is the restriction of an invariant on K[σ] (TauCeti.map_symmetricAlgebraInvariants_dualRestrict_augmentation). The invariants on K[σ] form a polynomial algebra on the elementary symmetric invariants e₁, …, e_(n+1) (Representation.esymmSymmetricAlgebraInvariantsEquiv); restriction kills e₁, and the restrictions of e₂, …, e_(n+1) are algebraically independent over any commutative ring. So whenever n + 1 is invertible in K, the invariant algebra Sym(V₀*)^(S_σ) is a polynomial algebra on n homogeneous invariants of degrees 2, …, n + 1 (TauCeti.esymmStandardInvariantsEquiv).

This is the exact difference from the full permutation representation, whose basic invariants have degrees 1, 2, …, n + 1: the degree-one invariant e₁ spans the dual of the trivial summand of K[σ] = K ⊕ V₀ and is lost on restriction to V₀, while the other basic invariants restrict to basic invariants. For n = 0 the trace-zero hyperplane is zero and the invariant algebra is K.

The hypothesis that n + 1 is invertible cannot be dropped from the description of the invariant algebra, which uses it only to lift invariants from V₀ to K[σ]: if K has characteristic 2 and σ has two elements, then V₀ is the invariant line spanned by x - y, and its invariant polynomial functions form a polynomial algebra on a generator of degree one.

Main results

• TauCeti.ker_map_dualRestrict_augmentation: polynomial functions on V₀ are polynomial functions on K[σ] modulo e₁.
• TauCeti.map_symmetricAlgebraInvariants_dualRestrict_augmentation: the invariants on V₀ are the restrictions of the invariants on K[σ].
• TauCeti.esymmStandardInvariantsEquiv: the invariant algebra of the reflection representation of S_σ is a polynomial algebra on the restrictions of e₂, …, e_(n+1), with TauCeti.coe_esymmStandardInvariantsEquiv_X and TauCeti.coe_esymmStandardInvariantsEquiv_X_eq_sum computing the generators and TauCeti.esymmStandardInvariantsEquiv_X_mem_homogeneousSubmodule giving their degrees 2, …, n + 1.
• TauCeti.map_univ_eq_of_bijective_aeval_standardRepresentation_dual: every system of basic invariants of the reflection representation has the multiset of degrees {2, …, n + 1}.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Chapter 3.

theorem TauCeti.ker_map_dualRestrict_augmentation (K : Type u_1) [CommRing K] (σ : Type u_2) : RingHom.ker (SymmetricAlgebra.map K (augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule.dualRestrict) = Ideal.span {(SymmetricAlgebra.ι K (MonoidAlgebra K σ →ₗ[K] K)) (MonoidAlgebra.basis σ K).sumCoords}

Polynomial functions on the trace-zero hyperplane V₀ ⊆ K[σ] are the polynomial functions on K[σ] modulo the coefficient sum e₁ = ∑ᵢ xᵢ: the kernel of restriction Sym(K[σ]*) → Sym(V₀*) is the ideal generated by e₁. This holds over every commutative ring.

theorem TauCeti.map_symmetricAlgebraInvariants_dualRestrict_augmentation (K : Type u_1) [CommRing K] (σ : Type u_2) [Fintype σ] (h : IsUnit ↑(Fintype.card σ)) : Subalgebra.map (SymmetricAlgebra.map K (augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule.dualRestrict) (Representation.ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants = (standardRepresentation K σ).dual.symmetricAlgebraInvariants

The invariant polynomial functions on the trace-zero hyperplane V₀ ⊆ K[σ] are the restrictions of the invariant polynomial functions on K[σ], when the cardinality of σ is invertible, so that V₀ is an invariant direct summand of K[σ].

noncomputable def TauCeti.esymmStandardInvariantsEquiv (K : Type u_1) [CommRing K] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (h : IsUnit ↑(Fintype.card σ)) (hn : Fintype.card σ = n + 1) : MvPolynomial (Fin n) K ≃ₐ[K] ↥(standardRepresentation K σ).dual.symmetricAlgebraInvariants

The invariants of the reflection representation of S_σ form a polynomial algebra. Let σ have n + 1 elements, with n + 1 invertible in K. The invariant polynomial functions on the trace-zero hyperplane V₀ ⊆ K[σ] form a polynomial algebra on n generators: the variable Xᵢ is sent to the restriction to V₀ of the elementary symmetric invariant e_(i + 2) (coe_esymmStandardInvariantsEquiv_X), which is homogeneous of degree i + 2 (esymmStandardInvariantsEquiv_X_mem_homogeneousSubmodule). So the basic invariants have degrees 2, …, n + 1.

theorem TauCeti.coe_esymmStandardInvariantsEquiv_X (K : Type u_1) [CommRing K] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (h : IsUnit ↑(Fintype.card σ)) (hn : Fintype.card σ = n + 1) (i : Fin n) : ↑((esymmStandardInvariantsEquiv K h hn) (MvPolynomial.X i)) = (SymmetricAlgebra.map K (augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule.dualRestrict) ↑((Representation.esymmSymmetricAlgebraInvariantsEquiv K σ hn) (MvPolynomial.X i.succ))

The generator Xᵢ is sent to the restriction to the trace-zero hyperplane of the elementary symmetric invariant of degree i + 2.

@[simp]

theorem TauCeti.coe_esymmStandardInvariantsEquiv_X_eq_sum (K : Type u_1) [CommRing K] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (h : IsUnit ↑(Fintype.card σ)) (hn : Fintype.card σ = n + 1) (i : Fin n) : ↑((esymmStandardInvariantsEquiv K h hn) (MvPolynomial.X i)) = ∑ t ∈ Finset.powersetCard (↑i + 2) Finset.univ, ∏ j ∈ t, (SymmetricAlgebra.ι K (Module.Dual K ↥(augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule)) ((augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule.dualRestrict ((MonoidAlgebra.basis σ K).dualBasis j))

The generator Xᵢ is sent to ∑ ∏_(j ∈ t) xⱼ|V₀, the sum over the subsets t of σ with i + 2 elements of the products of the restrictions of their coordinates to the trace-zero hyperplane V₀.

theorem TauCeti.esymmStandardInvariantsEquiv_X_mem_homogeneousSubmodule (K : Type u_1) [CommRing K] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {n : ℕ} (h : IsUnit ↑(Fintype.card σ)) (hn : Fintype.card σ = n + 1) (i : Fin n) : ↑((esymmStandardInvariantsEquiv K h hn) (MvPolynomial.X i)) ∈ SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K ↥(augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule) (↑i + 2)

The basic invariants of the reflection representation of S_σ have degrees 2, …, n + 1: the generator Xᵢ is sent to a homogeneous invariant of degree i + 2.

theorem TauCeti.map_univ_eq_of_bijective_aeval_standardRepresentation_dual (K : Type u_1) [CommRing K] {σ : Type u_2} [Fintype σ] {n : ℕ} [Nontrivial K] (h : IsUnit ↑(Fintype.card σ)) (hn : Fintype.card σ = n + 1) {ι : Type u_3} [Fintype ι] {f : ι → ↥(standardRepresentation K σ).dual.symmetricAlgebraInvariants} {d : ι → ℕ} (hf : ∀ (i : ι), ↑(f i) ∈ SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K ↥(augmentationSubrepresentation K (Equiv.Perm σ) σ).toSubmodule) (d i)) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : Multiset.map d Finset.univ.val = Multiset.map (fun (x : ℕ) => x + 2) (Multiset.range n)

The degrees of the reflection representation of S_σ are 2, …, n + 1. Let σ have n + 1 elements, with n + 1 invertible in K. Then every system of basic invariants of the reflection representation, that is, every family of homogeneous invariants of degrees d i on which the invariant algebra is a polynomial algebra, has the multiset of degrees {2, …, n + 1}.