The graded character of the coinvariant algebra

Let a group G act linearly on a finite-dimensional vector space M over a field K, and so on the symmetric algebra S = Sym M, with invariant subalgebra A = Sym(M)^G and coinvariant algebra C = S ⧸ A₊ · S. The coinvariant algebra is graded by the images Cⱼ of the homogeneous components Symʲ M, and G acts on each of them (Representation.coinvariantAlgebraHomogeneous). Its graded character is the power series ∑ⱼ χ_{Cⱼ}(g) tʲ, recording the action of each element degree by degree.

If A is generated by homogeneous invariants f₁, …, fₙ of positive degrees d₁, …, dₙ which form a regular sequence in S, then for every g

∑ⱼ χ_{Cⱼ}(g) tʲ = (∑ⱼ χ_{Symʲ M}(g) tʲ) * ∏ᵢ (1 - t ^ dᵢ).

Each g acts on S by an algebra automorphism fixing the invariants fᵢ, so this is the equivariant regular-sequence formula TauCeti.GradedAlgebra.mk_trace_quotientPiece_of_isWeaklyRegular. When G is finite of order invertible in K, the graded trace formula on the symmetric algebra identifies ∑ⱼ χ_{Symʲ M}(g) tʲ with det(1 - t g | M)⁻¹, so that

∑ⱼ χ_{Cⱼ}(g) tʲ = ∏ᵢ (1 - t ^ dᵢ) / det(1 - t g | M).

For a finite group generated by pseudoreflections, of order invertible in K, acting on a finite-dimensional space V, any homogeneous basic invariants of the polynomial functions Sym(V*) form such a regular sequence, which gives the graded character of the coinvariant algebra of Sym(V*). At g = 1 this is the Hilbert series of the coinvariant algebra (TauCeti.RepresentationTheory.SymmetricAlgebra.Coinvariant.HilbertSeries). This graded character refines the ungraded statement that the coinvariant algebra has the regular character (TauCeti.RepresentationTheory.SymmetricAlgebra.RegularRepresentation); over a splitting field of characteristic zero, the orthogonality of characters recovers from it the fake-degree polynomials, the graded multiplicities of the irreducible representations, which are not computed here.

Main results

• Representation.coinvariantAlgebraHomogeneous: the representation on the degree-j piece of the coinvariant algebra.
• Representation.mk_character_coinvariantAlgebraHomogeneous: the graded character of the coinvariant algebra is the graded character of Sym M times ∏ᵢ (1 - t ^ dᵢ).
• Representation.mk_character_coinvariantAlgebraHomogeneous_mul_reverse_charpoly: for a finite group of invertible order, its product with det(1 - t g | M) is ∏ᵢ (1 - t ^ dᵢ).
• mk_character_coinvariantAlgebraHomogeneous_dual_of_pseudoreflectionSubgroup_eq_top, in the namespace Representation: the same for the polynomial functions on a representation of a finite group generated by pseudoreflections, with any homogeneous basic invariants.

References

• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 475–511, §§ 3–4.
• R. Kane, Reflection Groups and Invariant Theory, CMS Books in Mathematics, Springer (2001).

theorem Representation.coinvariantAlgebra_mem_quotientPiece {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) {n : ℕ} {x : SymmetricAlgebra R M ⧸ ρ.symmetricAlgebraHilbertIdeal} (hx : x ∈ TauCeti.GradedAlgebra.quotientPiece (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraHilbertIdeal n) : (ρ.coinvariantAlgebra g) x ∈ TauCeti.GradedAlgebra.quotientPiece (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraHilbertIdeal n

The action of G on the coinvariant algebra preserves the image of each homogeneous component Symⁿ M.

noncomputable def Representation.coinvariantAlgebraHomogeneous {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (n : ℕ) : Representation R G ↥(TauCeti.GradedAlgebra.quotientPiece (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraHilbertIdeal n)

The representation of G on the degree-n piece of the coinvariant algebra Sym M ⧸ A₊ · Sym M, the image of the homogeneous component Symⁿ M: the restriction of Representation.coinvariantAlgebra to this subrepresentation.

@[simp]

theorem Representation.coe_coinvariantAlgebraHomogeneous_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (n : ℕ) (g : G) (x : ↥(TauCeti.GradedAlgebra.quotientPiece (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraHilbertIdeal n)) : ↑(((ρ.coinvariantAlgebraHomogeneous n) g) x) = (ρ.coinvariantAlgebra g) ↑x

The action on the degree-n piece of the coinvariant algebra is computed in the coinvariant algebra.

theorem Representation.mk_character_coinvariantAlgebraHomogeneous {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] [Monoid G] (ρ : Representation K G M) {n : ℕ} (f : Fin n → ↥ρ.symmetricAlgebraInvariants) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hf : ∀ (i : Fin n), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K M (d i)) (hsurj : Function.Surjective ⇑(MvPolynomial.aeval f)) (hreg : RingTheory.Sequence.IsWeaklyRegular (SymmetricAlgebra K M) (List.ofFn fun (i : Fin n) => ↑(f i))) (g : G) : (PowerSeries.mk fun (j : ℕ) => (ρ.coinvariantAlgebraHomogeneous j).character g) = (PowerSeries.mk fun (j : ℕ) => (ρ.symmetricAlgebraHomogeneous j).character g) * ∏ i : Fin n, (1 - PowerSeries.X ^ d i)

The graded character of the coinvariant algebra. If the invariants are generated by homogeneous invariants f i of positive degrees d i forming a weakly regular sequence in Sym M, then for every g the graded character ∑ⱼ χ_{Cⱼ}(g) tʲ of the coinvariant algebra is the graded character of Sym M multiplied by ∏ᵢ (1 - t ^ d i). Surjectivity of evaluation suffices; algebraic independence is not required, and neither is any finiteness of G.

theorem Representation.mk_character_coinvariantAlgebraHomogeneous_mul_reverse_charpoly {K : Type u_1} {G : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (ρ : Representation K G M) {n : ℕ} (f : Fin n → ↥ρ.symmetricAlgebraInvariants) (d : Fin n → ℕ) (hd : ∀ (i : Fin n), 0 < d i) (hf : ∀ (i : Fin n), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K M (d i)) (hsurj : Function.Surjective ⇑(MvPolynomial.aeval f)) (hreg : RingTheory.Sequence.IsWeaklyRegular (SymmetricAlgebra K M) (List.ofFn fun (i : Fin n) => ↑(f i))) (g : G) : (PowerSeries.mk fun (j : ℕ) => (ρ.coinvariantAlgebraHomogeneous j).character g) * ↑(ρ g).charpoly.reverse = ∏ i : Fin n, (1 - PowerSeries.X ^ d i)

The graded character of the coinvariant algebra, determinant form. For a finite group whose order is invertible in K, if the invariants are generated by homogeneous invariants f i of positive degrees d i forming a weakly regular sequence in Sym M, then for every g (∑ⱼ χ_{Cⱼ}(g) tʲ) * det(1 - t g | M) = ∏ᵢ (1 - t ^ d i), where det(1 - t g | M) is the reverse of the characteristic polynomial of ρ g. No eigenvalue of ρ g need lie in K.

theorem Representation.mk_character_coinvariantAlgebraHomogeneous_dual_of_pseudoreflectionSubgroup_eq_top {K : Type u_1} {G : Type u_2} [Field K] {V : Type u_4} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (ρ : Representation K G V) (hG : ρ.pseudoreflectionSubgroup = ⊤) {n : ℕ} (f : Fin n → ↥ρ.dual.symmetricAlgebraInvariants) (d : Fin n → ℕ) (hf : ∀ (i : Fin n), ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) (d i)) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) (g : G) : (PowerSeries.mk fun (j : ℕ) => (ρ.dual.coinvariantAlgebraHomogeneous j).character g) * ↑(ρ.dual g).charpoly.reverse = ∏ i : Fin n, (1 - PowerSeries.X ^ d i)

The graded character of the coinvariant algebra of a pseudoreflection group. Let a finite group G, whose order is invertible in K, act on a finite-dimensional vector space V and be generated by pseudoreflections. For any homogeneous basic invariants f i of the polynomial functions Sym(V*), of degrees d i, and every g, the graded character of the coinvariant algebra of Sym(V*) satisfies (∑ⱼ χ_{Cⱼ}(g) tʲ) * det(1 - t g | V*) = ∏ᵢ (1 - t ^ d i), where det(1 - t g | V*) is the reverse of the characteristic polynomial of ρ.dual g. No faithfulness assumption is needed.