Polynomial invariants of a faithful quotient

Removing a normal subgroup acting trivially does not change the invariant subalgebra of the symmetric algebra, including its grading. This applies both to a representation and to its contragredient action on polynomial functions. In particular, the faithful representation of G ⧸ ker ρ has exactly the original polynomial invariants. The kernel acts trivially even on the entire polynomial algebra, not just on its invariant subalgebra.

@[simp]

theorem Representation.symmetricAlgebraInvariants_ofQuotient {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : (ρ.ofQuotient S).symmetricAlgebraInvariants = ρ.symmetricAlgebraInvariants

Removing a trivially acting normal subgroup preserves the invariant subalgebra of Sym M, as a subalgebra of the same ambient graded algebra.

@[simp]

theorem Representation.symmetricAlgebraInvariants_dual_ofQuotient {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : (ρ.ofQuotient S).dual.symmetricAlgebraInvariants = ρ.dual.symmetricAlgebraInvariants

Removing a trivially acting normal subgroup preserves the polynomial invariant algebra Sym(M*)^G, with its original coefficient and dual-module structures and its grading.