Degrees of basic invariants

Let a group G act linearly on a module M, and so on the symmetric algebra S = Sym M, with invariant subalgebra A = Sym(M)^G. A system of basic invariants is a family of homogeneous invariants f i ∈ A ∩ Sym^{d i} M such that R[Xᵢ] → A, Xᵢ ↦ f i, is bijective: the f i are algebraically independent and generate A. Over a field, for a finite group generated by pseudoreflections whose order is invertible, such systems exist by the classical theorem of Chevalley and Shephard–Todd; for the symmetric group they are the elementary symmetric invariants (Representation.esymmSymmetricAlgebraInvariantsEquiv, TauCeti.esymmStandardInvariantsEquiv). Such systems are not unique, and this file proves that their numerical invariants are.

• Every basic invariant has positive degree, since the invariants of degree zero are the scalars.
• For a finite group acting on a finite-dimensional vector space M over a field, a system of basic invariants has exactly finrank M members: the invariant ring has the Krull dimension of Sym M, which is integral over it.
• The Hilbert series of the invariant algebra is ∑ₙ dim (A ∩ Symⁿ M) tⁿ = ∏ᵢ (1 - t ^ d i)⁻¹.
• Consequently the multiset of degrees d i does not depend on the system of basic invariants. These are the degrees of the group; for the reflection representation of the symmetric group S_{n+1}, with n + 1 invertible, they are 2, 3, …, n + 1 (TauCeti.map_univ_eq_of_bijective_aeval_standardRepresentation_dual).
• The degrees of a subgroup H are smaller than those of G: since Sym(M)^G ⊆ Sym(M)^H, for every n there are at most as many basic invariants of G of degree at most n as there are basic invariants of H of degree at most n.

These statements are specializations of the corresponding facts for graded polynomial algebras (TauCeti.RingTheory.GradedAlgebra.HilbertSeries) to the grading of the invariant subalgebra by the degrees of Sym M. Combined with Molien's formula (TauCeti.RepresentationTheory.SymmetricAlgebra.Molien), the Hilbert series formula expresses the average over G of det(1 - t g)⁻¹ through the degrees.

Main results

• Representation.ne_zero_of_injective_aeval_symmetricAlgebraInvariants: algebraically independent homogeneous invariants have positive degrees.
• Representation.card_eq_finrank_of_bijective_aeval_symmetricAlgebraInvariants: a polynomial generating system of the invariants of a finite group has finrank M members.
• mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule_mul_prod_one_sub_X_pow (in the namespace Representation): the Hilbert series of the invariants is ∏ᵢ (1 - t ^ d i)⁻¹.
• Representation.map_univ_eq_of_bijective_aeval_symmetricAlgebraInvariants: two systems of basic invariants have the same multiset of degrees.
• Representation.map_univ_eq_of_bijective_aeval_of_algEquiv_symmetricAlgebraInvariants: the same, with the second system given by an algebra isomorphism from a polynomial algebra.
• Representation.card_filter_le_le_card_filter_le_of_comp_subtype: a system of basic invariants of a subgroup has, in each degree range ≤ n, at least as many members as one of the group.

References

• C. Chevalley, Invariants of finite groups generated by reflections, Amer. J. Math. 77 (1955), 778–782.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Sections 3.5–3.7.
• R. Kane, Reflection Groups and Invariant Theory, Springer (2001), § 18.

theorem Representation.ne_zero_of_injective_aeval_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_3} {M : Type u_4} {ι : Type u_5} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {f : ι → ↥ρ.symmetricAlgebraInvariants} {d : ι → ℕ} [Nontrivial R] (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) (hinj : Function.Injective ⇑(MvPolynomial.aeval f)) (i : ι) : d i ≠ 0

Basic invariants have positive degrees. If invariants f i homogeneous of degrees d i are algebraically independent, then every d i is nonzero.

theorem Representation.mk_finrank_symmetricAlgebraInvariants_inf_homogeneousSubmodule_mul_prod_one_sub_X_pow {R : Type u_1} {G : Type u_3} {M : Type u_4} {ι : Type u_5} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {f : ι → ↥ρ.symmetricAlgebraInvariants} {d : ι → ℕ} [Nontrivial R] [Fintype ι] (S : Type u_7) [CommRing S] (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : (PowerSeries.mk fun (n : ℕ) => ↑(Module.finrank R ↥(Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n))) * ∏ i : ι, (1 - PowerSeries.X ^ d i) = 1

The Hilbert series of a polynomial invariant algebra. If the invariant subalgebra is a polynomial algebra on invariants f i homogeneous of degrees d i, then its Hilbert series ∑ₙ dim (Sym(M)^G ∩ Symⁿ M) tⁿ, with coefficients cast into any commutative ring S, is the inverse of ∏ᵢ (1 - t ^ d i).

theorem Representation.map_univ_eq_of_bijective_aeval_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_3} {M : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {f : ι → ↥ρ.symmetricAlgebraInvariants} {d : ι → ℕ} [Nontrivial R] [Fintype ι] [Fintype κ] {f' : κ → ↥ρ.symmetricAlgebraInvariants} {d' : κ → ℕ} (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) (hf' : ∀ (j : κ), ↑(f' j) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d' j)) (hbij' : Function.Bijective ⇑(MvPolynomial.aeval f')) : Multiset.map d Finset.univ.val = Multiset.map d' Finset.univ.val

The degrees of basic invariants are intrinsic. Two systems of basic invariants, that is, two families of homogeneous invariants on which the invariant subalgebra is a polynomial algebra, have the same multiset of degrees.

theorem Representation.map_univ_eq_of_bijective_aeval_of_algEquiv_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_3} {M : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {f : ι → ↥ρ.symmetricAlgebraInvariants} {d : ι → ℕ} [Nontrivial R] [Fintype ι] [Fintype κ] {d' : κ → ℕ} (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) (e : MvPolynomial κ R ≃ₐ[R] ↥ρ.symmetricAlgebraInvariants) (he : ∀ (j : κ), ↑(e (MvPolynomial.X j)) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d' j)) : Multiset.map d Finset.univ.val = Multiset.map d' Finset.univ.val

The degrees of basic invariants are intrinsic, comparing with a system of basic invariants given by an algebra isomorphism e : R[Xⱼ] ≃ₐ[R] Sym(M)^G that sends each Xⱼ to an invariant homogeneous of degree d' j.

theorem Representation.card_filter_le_le_card_filter_le_of_comp_subtype {R : Type u_1} {G : Type u_3} {M : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommRing R] [IsDomain R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype ι] [Fintype κ] {f : ι → ↥ρ.symmetricAlgebraInvariants} {d : ι → ℕ} {H : Subgroup G} (hf : ∀ (i : ι), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (d i)) (hinj : Function.Injective ⇑(MvPolynomial.aeval f)) {g : κ → ↥(symmetricAlgebraInvariants (MonoidHom.comp ρ H.subtype))} {e : κ → ℕ} (hg : ∀ (j : κ), ↑(g j) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (e j)) (hsurj : Function.Surjective ⇑(MvPolynomial.aeval g)) (n : ℕ) : {i : ι | d i ≤ n}.card ≤ {j : κ | e j ≤ n}.card

Degrees of the invariants of a subgroup. Let H be a subgroup of G. If invariants f i of G, homogeneous of degrees d i, are algebraically independent, and invariants g j of H, homogeneous of degrees e j, generate the invariants of H, then for every n there are at most as many f i of degree at most n as there are g j of degree at most n.

theorem Representation.card_eq_finrank_of_bijective_aeval_symmetricAlgebraInvariants {k : Type u_2} {G : Type u_3} {M : Type u_4} {ι : Type u_5} [Field k] [Group G] [Finite G] [AddCommGroup M] [Module k M] (ρ : Representation k G M) {f : ι → ↥ρ.symmetricAlgebraInvariants} (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : Nat.card ι = Module.finrank k M

The number of basic invariants. For a finite group acting on a vector space M, if the invariant subalgebra is a polynomial algebra on a family of invariants, then this family has finrank M members. (For infinite-dimensional M both sides are 0.)