The Reynolds operator on a symmetric algebra

Let a finite group G act linearly on a module M over a commutative ring R in which #G is invertible. Averaging the induced action on the symmetric algebra, p ↦ #G⁻¹ • ∑ g, g • p, is the Reynolds operator Sym M → Sym(M)^G. It is a retraction of the inclusion of the invariant subalgebra, it preserves homogeneous degrees, and it is linear over the invariant subalgebra: it sends a * p to a times the image of p for every invariant a. It is generally not multiplicative; the inclusion of the invariants, not the Reynolds operator, is the algebra map.

The Reynolds operator is the averaging projection Representation.averageMap of the induced representation Representation.symmetricAlgebra; this file records the additional structure that the multiplication and the grading of Sym M give it. It is the basic tool of the nonmodular invariant theory of finite groups (Hilbert's finite generation argument, Molien's formula); its definition requires #G to be invertible in R.

Main definitions

• Representation.symmetricAlgebraReynolds: the Reynolds operator, as a linear map over the invariant subalgebra from Sym M onto the invariant subalgebra.

Main results

• Representation.coe_symmetricAlgebraReynolds_eq_sum: it is the normalized group sum.
• Representation.symmetricAlgebraReynolds_coe: it restricts to the identity on invariants.
• Representation.symmetricAlgebraReynolds_coe_mul: it is linear over the invariants.
• Representation.coe_symmetricAlgebraReynolds_mem_homogeneousSubmodule: it preserves homogeneous degrees.
• Representation.symmetricAlgebraReynolds_map: it is constant on orbits.
• Representation.coe_averageMap_symmetricAlgebraHomogeneous: on each homogeneous component it is the averaging projection of the representation on that component.

References

• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), Chapter 2.
• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 475–511.

noncomputable def Representation.symmetricAlgebraReynolds {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] : SymmetricAlgebra R M →ₗ[↥ρ.symmetricAlgebraInvariants] ↥ρ.symmetricAlgebraInvariants

The Reynolds operator p ↦ #G⁻¹ • ∑ g, g • p, from Sym M onto the invariant subalgebra. It is linear over the invariant subalgebra and restricts to the identity on it, but it is generally not multiplicative.

theorem Representation.coe_symmetricAlgebraReynolds {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (p : SymmetricAlgebra R M) : ↑(ρ.symmetricAlgebraReynolds p) = ρ.symmetricAlgebra.averageMap p

The Reynolds operator is the averaging projection of the induced representation.

theorem Representation.coe_symmetricAlgebraReynolds_eq_sum {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (p : SymmetricAlgebra R M) : ↑(ρ.symmetricAlgebraReynolds p) = ⅟↑(Fintype.card G) • ∑ g : G, (ρ.symmetricAlgebra g) p

The Reynolds operator is the normalized sum #G⁻¹ • ∑ g, g • p over the group.

@[simp]

theorem Representation.symmetricAlgebraReynolds_coe {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (a : ↥ρ.symmetricAlgebraInvariants) : ρ.symmetricAlgebraReynolds ↑a = a

The Reynolds operator restricts to the identity on the invariant subalgebra.

theorem Representation.symmetricAlgebraReynolds_surjective {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] : Function.Surjective ⇑ρ.symmetricAlgebraReynolds

The Reynolds operator maps onto the invariant subalgebra.

@[simp]

theorem Representation.symmetricAlgebraReynolds_coe_mul {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (a : ↥ρ.symmetricAlgebraInvariants) (p : SymmetricAlgebra R M) : ρ.symmetricAlgebraReynolds (↑a * p) = a * ρ.symmetricAlgebraReynolds p

The Reynolds operator is linear over the invariant subalgebra.

theorem Representation.coe_symmetricAlgebraReynolds_mem_homogeneousSubmodule {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) : ↑(ρ.symmetricAlgebraReynolds p) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

The Reynolds operator preserves homogeneous degrees.

@[simp]

theorem Representation.symmetricAlgebraReynolds_map {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (g : G) (p : SymmetricAlgebra R M) : ρ.symmetricAlgebraReynolds ((SymmetricAlgebra.map R (ρ g)) p) = ρ.symmetricAlgebraReynolds p

The Reynolds operator is constant on the orbits of the induced action.

theorem Representation.coe_averageMap_symmetricAlgebraHomogeneous {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Invertible ↑(Fintype.card G)] (n : ℕ) (p : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) : ↑((ρ.symmetricAlgebraHomogeneous n).averageMap p) = ↑(ρ.symmetricAlgebraReynolds ↑p)

On the degree-n component, the Reynolds operator is the averaging projection of the degree-n representation Representation.symmetricAlgebraHomogeneous.