The coinvariant algebra is the regular representation

Let a finite group G act faithfully 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. When S is flat over A, which holds for a group generated by pseudoreflections whose order is invertible in k, the coinvariant algebra has the character of the regular representation, and over a field of characteristic zero it is isomorphic to the regular representation k[G] as an ungraded representation. For M = V* with the contragredient action this is Chevalley's theorem on the coinvariant algebra of a finite reflection group.

The proof is a trace computation, with no passage to fraction fields and no normal basis theorem.

• Each g acts on S by an A-algebra automorphism. If g moves some y, then the ideal of S generated by g y - y is nonzero, so it contains a nonzero invariant a, as S is an integral domain integral over A. Cyclicity of the trace gives a * trace_A (g) = 0 (AlgHom.mul_trace_toLinearMap_eq_zero_of_mem_span), so g has trace zero over A. This uses neither flatness nor freeness, the trace being zero by definition for a non-free module.
• When S is flat over A it has an A-basis lifting a k-basis of C (Representation.exists_basis_quotient_mk_eq_of_flat). Every invariant is congruent to its constant term modulo A₊ · S, so the matrix of g on C is the matrix of g on S with its entries reduced to their constant terms, and the trace of g on C is the constant term of its trace over A.

So g ≠ 1 has trace zero on C, while 1 has trace dim C = |G| (Representation.finrank_quotient_symmetricAlgebraHilbertIdeal_of_flat). In characteristic zero both C and k[G] are semisimple by Maschke's theorem, and semisimple representations with the same character are equivalent (Representation.nonempty_equiv_of_character_eq_of_isSemisimpleRepresentation).

This is the ungraded statement only: the coinvariant algebra is graded, and its graded character, a finer invariant, is computed in TauCeti.RepresentationTheory.SymmetricAlgebra.Coinvariant.Character. The fake-degree polynomials extracted from it are not computed.

Main results

• Representation.trace_symmetricAlgebraOverInvariants_eq_zero: an element acting nontrivially has trace zero on Sym M over its invariants, when Sym M is a domain.
• Representation.trace_coinvariantAlgebra: when Sym M is flat over its invariants, the trace on the coinvariant algebra is the constant term of the trace over the invariants.
• Representation.character_coinvariantAlgebra: for a faithful action, the coinvariant algebra has the regular character.
• Representation.nonempty_equiv_coinvariantAlgebra_leftRegular: in characteristic zero, it is equivalent to the regular representation.
• character_coinvariantAlgebra_dual_of_pseudoreflectionSubgroup_eq_top and nonempty_equiv_coinvariantAlgebra_dual_leftRegular_of_pseudoreflectionSubgroup_eq_top, in the namespace Representation: the same for the polynomial functions on a representation of a finite group generated by pseudoreflections.

References

• C. Chevalley, Invariants of finite groups generated by reflections, Amer. J. Math. 77 (1955).
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4–6, Springer (2002), Chapter V, § 5.

theorem Representation.trace_symmetricAlgebraOverInvariants_eq_zero {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M] [Module R M] [IsDomain (SymmetricAlgebra R M)] (ρ : Representation R G M) {g : G} (hg : ρ g ≠ 1) : (LinearMap.trace (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M)) (ρ.symmetricAlgebraOverInvariants g) = 0

An element acting nontrivially has trace zero over the invariants. For a finite group acting on M with Sym M a domain, if ρ g ≠ 1 then g has trace zero as an endomorphism of Sym M over the invariant subalgebra Sym(M)^G. This is only informative when Sym M is free of finite rank over its invariants; otherwise the trace vanishes by definition.

theorem Representation.trace_coinvariantAlgebra {k : Type u_1} {G : Type u_2} {M : Type u_3} [Field k] [Group G] [Finite G] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (ρ : Representation k G M) [Module.Flat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra k M)] (g : G) : (LinearMap.trace k (SymmetricAlgebra k M ⧸ ρ.symmetricAlgebraHilbertIdeal)) (ρ.coinvariantAlgebra g) = SymmetricAlgebra.algebraMapInv ↑((LinearMap.trace (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra k M)) (ρ.symmetricAlgebraOverInvariants g))

The trace on the coinvariant algebra is the constant term of the trace over the invariants. If Sym M is flat over its invariants A, then for every g the trace of g on the coinvariant algebra Sym M ⧸ A₊ · Sym M is the constant term of the trace of g on Sym M over A.

theorem Representation.character_coinvariantAlgebra {k : Type u_1} {G : Type u_2} {M : Type u_3} [Field k] [Group G] [Finite G] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (ρ : Representation k G M) [DecidableEq G] [Module.Flat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra k M)] (hρ : Function.Injective ⇑ρ) (g : G) : ρ.coinvariantAlgebra.character g = if g = 1 then ↑(Nat.card G) else 0

The coinvariant algebra has the regular character. If a finite group G acts faithfully on a finite-dimensional space M and Sym M is flat over its invariants A, then on the coinvariant algebra Sym M ⧸ A₊ · Sym M the identity has trace |G| and every other element has trace zero.

theorem Representation.nonempty_equiv_coinvariantAlgebra_leftRegular {k : Type u_1} {G : Type u_2} {M : Type u_3} [Field k] [Group G] [Finite G] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (ρ : Representation k G M) [CharZero k] [Module.Flat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra k M)] (hρ : Function.Injective ⇑ρ) : Nonempty (ρ.coinvariantAlgebra.Equiv (leftRegular k G))

The coinvariant algebra is the regular representation. If a finite group G acts faithfully on a finite-dimensional space M over a field of characteristic zero, and Sym M is flat over its invariants A, then the coinvariant algebra Sym M ⧸ A₊ · Sym M, as an ungraded representation, is equivalent to the regular representation k[G].

theorem Representation.character_coinvariantAlgebra_dual_of_pseudoreflectionSubgroup_eq_top {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (ρ : Representation K G V) [Fintype G] [DecidableEq G] [Invertible ↑(Fintype.card G)] (hG : ρ.pseudoreflectionSubgroup = ⊤) (hρ : Function.Injective ⇑ρ) (g : G) : ρ.dual.coinvariantAlgebra.character g = if g = 1 then ↑(Nat.card G) else 0

The coinvariant algebra of a pseudoreflection group has the regular character. If a finite group G, whose order is invertible in the field K, acts faithfully on a finite-dimensional vector space V and is generated by pseudoreflections, then on the coinvariant algebra of the polynomial functions Sym(V*) the identity has trace |G| and every other element has trace zero.

theorem Representation.nonempty_equiv_coinvariantAlgebra_dual_leftRegular_of_pseudoreflectionSubgroup_eq_top {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (ρ : Representation K G V) [Finite G] [CharZero K] (hG : ρ.pseudoreflectionSubgroup = ⊤) (hρ : Function.Injective ⇑ρ) : Nonempty (ρ.dual.coinvariantAlgebra.Equiv (leftRegular K G))

Chevalley's theorem: the coinvariant algebra of a reflection group is the regular representation. If a finite group G acts faithfully on a finite-dimensional vector space V over a field of characteristic zero and is generated by pseudoreflections, then the coinvariant algebra of the polynomial functions Sym(V*), as an ungraded representation, is equivalent to the regular representation K[G].