Documentation

TauCeti.RepresentationTheory.SymmetricAlgebra.Permutation

Invariants of a permutation representation #

Let a group G act on a finite set σ, and so linearly on the permutation module K[σ] with basis the points of σ (Representation.ofMulAction). The polynomial functions on K[σ] form Sym(K[σ]*), the symmetric algebra on the dual, with the contragredient action. The coordinate functions xᵢ, the basis dual to the points, identify Sym(K[σ]*) with the polynomial ring K[xᵢ | i ∈ σ] (SymmetricAlgebra.equivMvPolynomial), and under this identification g acts by renaming each variable xᵢ to x_(g • i). So the invariant polynomials of G are the polynomials fixed by these renamings.

For the full symmetric group S_σ, the invariants are the symmetric polynomials. By the fundamental theorem of symmetric polynomials (MvPolynomial.esymmAlgEquiv), if σ has n elements then the invariant algebra Sym(K[σ]*)^(S_σ) is a polynomial algebra on the n elementary symmetric invariants e₁, …, eₙ, where eₖ is homogeneous of degree k. Thus the degrees of the basic invariants of the full permutation representation are 1, 2, …, n. The degree-one invariant e₁ = ∑ᵢ xᵢ is a genuine invariant linear form, not an artifact of conventions: it spans the invariant linear forms on K[σ]. When n is invertible in K, K[σ] is the direct sum of the fixed line spanned by ∑ᵢ i and the trace-zero hyperplane e₁ = 0, on which S_σ acts by its reflection representation. That representation omits the trivial summand and its basic invariants have degrees 2, …, n instead; see TauCeti.RepresentationTheory.SymmetricAlgebra.Standard.

No hypothesis on K beyond commutativity is needed: the fundamental theorem holds over every commutative ring, including in characteristic dividing n!, where the group order is not invertible. The cases n = 0 and n = 1 are included: the invariant algebra is then K or K[x].

Main results #

References #

source
theorem Representation.ofMulAction_dual_dualBasis (K : Type u_1) [CommRing K] {G : Type u_2} {σ : Type u_3} [Group G] [MulAction G σ] [Finite σ] [DecidableEq σ] (g : G) (i : σ) :
((ofMulAction K G σ).dual g) ((MonoidAlgebra.basis σ K).dualBasis i) = (MonoidAlgebra.basis σ K).dualBasis (g • i)

The contragredient of a permutation representation permutes the coordinate functions: g sends the coordinate xᵢ to x_(g • i).

source
theorem Representation.equivMvPolynomial_symmetricAlgebra_ofMulAction_dual (K : Type u_1) [CommRing K] {G : Type u_2} {σ : Type u_3} [Group G] [MulAction G σ] [Finite σ] [DecidableEq σ] (g : G) (p : SymmetricAlgebra K (Module.Dual K (MonoidAlgebra K σ))) :
(SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) (((ofMulAction K G σ).dual.symmetricAlgebra g) p) = (MvPolynomial.rename fun (x : σ) => g • x) ((SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) p)

In the coordinates of a permutation representation, g acts on polynomial functions by renaming each variable xᵢ to x_(g • i).

source
theorem Representation.mem_symmetricAlgebraInvariants_ofMulAction_dual_iff (K : Type u_1) [CommRing K] {G : Type u_2} {σ : Type u_3} [Group G] [MulAction G σ] [Finite σ] [DecidableEq σ] (p : SymmetricAlgebra K (Module.Dual K (MonoidAlgebra K σ))) :
p ∈ (ofMulAction K G σ).dual.symmetricAlgebraInvariants ↔ ∀ (g : G), (MvPolynomial.rename fun (x : σ) => g • x) ((SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) p) = (SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) p

A polynomial function on a permutation representation is invariant exactly when its polynomial in the coordinates is fixed by the renamings xᵢ ↦ x_(g • i).

source
theorem Representation.mem_symmetricAlgebraInvariants_ofMulAction_perm_dual_iff (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Finite σ] (p : SymmetricAlgebra K (Module.Dual K (MonoidAlgebra K σ))) :
p ∈ (ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants ↔ ((SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) p).IsSymmetric

A polynomial function on the full permutation representation of S_σ is invariant exactly when its polynomial in the coordinates is symmetric.

source
theorem Representation.map_symmetricAlgebraInvariants_ofMulAction_perm_dual (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Finite σ] :
Subalgebra.map (↑(SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis)) (ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants = MvPolynomial.symmetricSubalgebra σ K

The invariants of the full permutation representation are the symmetric polynomials: the coordinates of K[σ] carry the invariant algebra of S_σ onto MvPolynomial.symmetricSubalgebra.

source
noncomputable def Representation.symmetricAlgebraInvariantsPermEquiv (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Finite σ] :
↥(ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants ≃ₐ[K] ↥(MvPolynomial.symmetricSubalgebra σ K)

The invariant algebra of the full permutation representation of S_σ is isomorphic to the algebra of symmetric polynomials in the coordinates.

Instances For
    source
    @[simp]
    theorem Representation.coe_symmetricAlgebraInvariantsPermEquiv_apply (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Finite σ] (p : ↥(ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants) :
    ↑((symmetricAlgebraInvariantsPermEquiv K σ) p) = (SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis) ↑p

    The isomorphism with the symmetric polynomials takes an invariant to its polynomial in the coordinates.

    source
    @[simp]
    theorem Representation.coe_symmetricAlgebraInvariantsPermEquiv_symm_apply (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Finite σ] (q : ↥(MvPolynomial.symmetricSubalgebra σ K)) :
    ↑((symmetricAlgebraInvariantsPermEquiv K σ).symm q) = (SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis).symm ↑q

    The inverse isomorphism reads a symmetric polynomial in the coordinates as a polynomial function.

    source
    noncomputable def Representation.esymmSymmetricAlgebraInvariantsEquiv (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Fintype σ] {n : ℕ} (hn : Fintype.card σ = n) :
    MvPolynomial (Fin n) K ≃ₐ[K] ↥(ofMulAction K (Equiv.Perm σ) σ).dual.symmetricAlgebraInvariants

    The invariants of the full permutation representation of S_σ form a polynomial algebra on the elementary symmetric invariants. If σ has n elements, the variable Xᵢ is sent to the elementary symmetric invariant e_(i + 1) in the coordinates, which is homogeneous of degree i + 1 (esymmSymmetricAlgebraInvariantsEquiv_X_mem_homogeneousSubmodule). So the basic invariants have degrees 1, …, n.

    Instances For
      source
      theorem Representation.coe_esymmSymmetricAlgebraInvariantsEquiv_X (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Fintype σ] {n : ℕ} (hn : Fintype.card σ = n) (i : Fin n) :
      ↑((esymmSymmetricAlgebraInvariantsEquiv K σ hn) (MvPolynomial.X i)) = (SymmetricAlgebra.equivMvPolynomial (MonoidAlgebra.basis σ K).dualBasis).symm (MvPolynomial.esymm σ K (↑i + 1))

      The generator Xᵢ is sent to the elementary symmetric polynomial of degree i + 1 in the coordinates.

      source
      @[simp]
      theorem Representation.coe_esymmSymmetricAlgebraInvariantsEquiv_X_eq_sum (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Fintype σ] {n : ℕ} (hn : Fintype.card σ = n) (i : Fin n) :
      ↑((esymmSymmetricAlgebraInvariantsEquiv K σ hn) (MvPolynomial.X i)) = ∑ t ∈ Finset.powersetCard (↑i + 1) Finset.univ, ∏ j ∈ t, (SymmetricAlgebra.ι K (Module.Dual K (MonoidAlgebra K σ))) ((MonoidAlgebra.basis σ K).dualBasis j)

      The generator Xᵢ is sent to ∑ ∏_(j ∈ t) xⱼ, the sum over the subsets t of σ with i + 1 elements of the products of their coordinates.

      source
      theorem Representation.coe_esymmSymmetricAlgebraInvariantsEquiv_X_zero (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Fintype σ] {n : ℕ} (hn : Fintype.card σ = n + 1) :
      ↑((esymmSymmetricAlgebraInvariantsEquiv K σ hn) (MvPolynomial.X 0)) = (SymmetricAlgebra.ι K (MonoidAlgebra K σ →ₗ[K] K)) (MonoidAlgebra.basis σ K).sumCoords

      The elementary symmetric invariant of degree one is the coefficient sum e₁ = ∑ᵢ xᵢ, which spans the invariant linear forms. When Fintype.card σ is invertible in K, so that K[σ] splits off the trivial summand spanned by ∑ᵢ i, it spans the dual of that summand.

      source
      theorem Representation.esymmSymmetricAlgebraInvariantsEquiv_X_mem_homogeneousSubmodule (K : Type u_1) [CommRing K] (σ : Type u_2) [DecidableEq σ] [Fintype σ] {n : ℕ} (hn : Fintype.card σ = n) (i : Fin n) :
      ↑((esymmSymmetricAlgebraInvariantsEquiv K σ hn) (MvPolynomial.X i)) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K (MonoidAlgebra K σ)) (↑i + 1)

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

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

      The degrees of the full permutation representation of S_σ are 1, …, n. If σ has n elements, then every system of basic invariants of Sym(K[σ]*)^(S_σ), 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 {1, …, n}.