The induced action on a symmetric algebra and its invariant subalgebra

A representation ρ of a monoid G on a module M extends multiplicatively to the symmetric algebra Sym M: each ρ g induces the algebra endomorphism SymmetricAlgebra.map (ρ g). Taking M = V* with the contragredient representation Representation.dual gives the action of G on polynomial functions on V, the starting point of the invariant theory of finite linear groups.

The induced action preserves the grading of Sym M by homogeneous degree. Its fixed points form a subalgebra, the invariant subalgebra Sym(M)^G, which is homogeneous: every homogeneous component of an invariant is again invariant. Restricting the action to a homogeneous component Symⁿ M gives a representation whose invariants are the degree-n part of Sym(M)^G; these are the pieces whose dimensions form the Hilbert series of the invariant subalgebra. In degree one the invariants are exactly the invariant vectors of M. For a finite group G, Sym M is integral over its invariants: an element p is a root of the monic polynomial ∏ g, (X - g • p), whose coefficients are invariant (Algebra.IsInvariant.isIntegral).

Each ρ g fixes the invariant subalgebra pointwise, so it is linear over it; this gives the representation Representation.symmetricAlgebraOverInvariants of G on Sym M as a module over Sym(M)^G, whose invariants are Sym(M)^G itself.

Since the representation ρ is data that instance search cannot infer, the induced action is bundled as Representation.symmetricAlgebraMulSemiringAction for local use, rather than registered as an instance; this gives access to the MulSemiringAction API, in particular to Mathlib's invariant extensions Algebra.IsInvariant.

Main definitions

• Representation.symmetricAlgebra: the representation of G on Sym M induced by ρ.
• Representation.symmetricAlgebraMulSemiringAction: the same action, bundled as an action by semiring endomorphisms.
• Representation.symmetricAlgebraInvariants: the subalgebra of Sym M fixed by every ρ g.
• Representation.symmetricAlgebraOverInvariants: the induced action on Sym M, as a representation by linear maps over the invariant subalgebra.
• Representation.symmetricAlgebraHomogeneous: the representation of G on the degree-n homogeneous component Symⁿ M.

Main results

• Representation.symmetricAlgebra_mem_homogeneousSubmodule and Representation.decompose_symmetricAlgebra: the induced action preserves degrees and commutes with taking homogeneous components.
• Representation.isHomogeneous_symmetricAlgebraInvariants: the invariant subalgebra is a homogeneous subalgebra.
• Representation.toSubmodule_symmetricAlgebraInvariants: as a submodule, it is the module of invariants of the induced representation.
• Representation.ι_mem_symmetricAlgebraInvariants_iff: its degree-one part is M^G.
• Representation.map_symmetricAlgebraInvariants_of_leftInverse: an intertwining map with an intertwining right inverse carries the invariant subalgebra onto the invariant subalgebra.
• Representation.mem_invariants_symmetricAlgebraOverInvariants_iff: the invariants of the action over the invariant subalgebra are the invariant subalgebra.
• Representation.symmetricAlgebraHomogeneous_apply: on Symⁿ M, g acts by the map homogeneousSubmoduleMapₛₗ (ρ g) n induced on degree n.
• Representation.map_subtype_invariants_symmetricAlgebraHomogeneous and Representation.finrank_invariants_symmetricAlgebraHomogeneous: the invariants of Symⁿ M are the degree-n part of the invariant subalgebra.
• Representation.faithfulSMul_symmetricAlgebraMulSemiringAction_iff: the bundled action is faithful exactly when ρ is.
• Representation.symmetricAlgebraInvariants_eq_fixedPoints and Representation.isInvariant_symmetricAlgebraInvariants: it is the fixed subalgebra of the bundled action, and Sym M is an invariant extension of it in the sense of Algebra.IsInvariant.
• Representation.symmetricAlgebraInvariants_comp_subtype: the invariants of the restriction to a subgroup H are the fixed points of H under the bundled action of G.
• Representation.isIntegral_symmetricAlgebraInvariants: for a finite group, Sym M is integral over the invariant subalgebra.

References

• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), Chapters 1 and 2.
• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 475–511.
• The construction of Representation.symmetricAlgebra follows the template of Representation.symmetricPower in TauCeti.RepresentationTheory.SymmetricPower.

noncomputable def Representation.symmetricAlgebra {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Representation R G (SymmetricAlgebra R M)

The representation of G on the symmetric algebra Sym M induced by a representation ρ on M: the element g acts by the algebra endomorphism extending ρ g multiplicatively.

For the contragredient representation ρ.dual, this is the action on polynomial functions.

@[simp]

theorem Representation.symmetricAlgebra_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (p : SymmetricAlgebra R M) : (ρ.symmetricAlgebra g) p = (SymmetricAlgebra.map R (ρ g)) p

The induced action of g is the symmetric-algebra map induced by ρ g.

theorem Representation.symmetricAlgebra_comp_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {G' : Type u_4} [Monoid G'] (f : G' →* G) (g : G') : (symmetricAlgebra (MonoidHom.comp ρ f)) g = ρ.symmetricAlgebra (f g)

The action induced by a representation pulled back along f : G' →* G is the induced action of f g.

theorem Representation.symmetricAlgebra_ι {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (m : M) : (ρ.symmetricAlgebra g) ((SymmetricAlgebra.ι R M) m) = (SymmetricAlgebra.ι R M) ((ρ g) m)

The induced action applies ρ to a canonical generator.

This is intentionally not a simp lemma: symmetricAlgebra_apply followed by SymmetricAlgebra.map_apply_ι already performs this simplification.

theorem Representation.symmetricAlgebra_mem_homogeneousSubmodule {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) : (ρ.symmetricAlgebra g) p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

The induced action preserves every homogeneous degree.

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

The representation of G on the degree-n homogeneous component Symⁿ M of the symmetric algebra: the restriction of Representation.symmetricAlgebra to this subrepresentation.

@[simp]

theorem Representation.coe_symmetricAlgebraHomogeneous_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (n : ℕ) (g : G) (p : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) : ↑(((ρ.symmetricAlgebraHomogeneous n) g) p) = (ρ.symmetricAlgebra g) ↑p

The action on Symⁿ M is computed in the symmetric algebra by the induced action.

theorem Representation.symmetricAlgebraHomogeneous_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (n : ℕ) (g : G) : (ρ.symmetricAlgebraHomogeneous n) g = TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ (ρ g) n

The action of g on Symⁿ M is the map homogeneousSubmoduleMapₛₗ (ρ g) n induced by ρ g on degree n.

theorem Representation.decompose_symmetricAlgebra {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (p : SymmetricAlgebra R M) (n : ℕ) : ↑(((DirectSum.decompose (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) ((ρ.symmetricAlgebra g) p)) n) = (ρ.symmetricAlgebra g) ↑(((DirectSum.decompose (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) p) n)

The induced action commutes with taking homogeneous components.

@[reducible, inline]

noncomputable abbrev Representation.symmetricAlgebraMulSemiringAction {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : MulSemiringAction G (SymmetricAlgebra R M)

The action of G on Sym M induced by ρ, bundled as an action by semiring endomorphisms, for use with the API of MulSemiringAction (fixed points, orbit polynomials). It is not an instance, since ρ cannot be inferred.

theorem Representation.symmetricAlgebraMulSemiringAction_smul {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (p : SymmetricAlgebra R M) : g • p = (ρ.symmetricAlgebra g) p

The bundled action is the induced representation.

theorem Representation.smulCommClass_symmetricAlgebraMulSemiringAction {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : SMulCommClass G R (SymmetricAlgebra R M)

The bundled action commutes with scalar multiplication by R.

theorem Representation.faithfulSMul_symmetricAlgebraMulSemiringAction_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : FaithfulSMul G (SymmetricAlgebra R M) ↔ Function.Injective ⇑ρ

The action of G on Sym M induced by ρ is faithful exactly when ρ is: an element of G is determined by its action on the degree-one elements ι m.

theorem Representation.IsIntertwiningMap.symmetricAlgebraMap {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] {ρ : Representation R G M} {N : Type u_4} [AddCommMonoid N] [Module R N] {ρ' : Representation R G N} {f : M →ₗ[R] N} (hf : ρ.IsIntertwiningMap ρ' f) : ρ.symmetricAlgebra.IsIntertwiningMap ρ'.symmetricAlgebra (SymmetricAlgebra.map R f).toLinearMap

The symmetric-algebra map induced by an intertwining map intertwines the induced representations.

noncomputable def Representation.symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Subalgebra R (SymmetricAlgebra R M)

The invariant subalgebra Sym(M)^G: the elements of Sym M fixed by the induced action of every element of G, that is, the fixed subalgebra FixedPoints.subalgebra of the bundled action.

@[simp]

theorem Representation.mem_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (p : SymmetricAlgebra R M) : p ∈ ρ.symmetricAlgebraInvariants ↔ ∀ (g : G), (ρ.symmetricAlgebra g) p = p

An element of Sym M is invariant when every g fixes it.

theorem Representation.symmetricAlgebraInvariants_eq_fixedPoints {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : ρ.symmetricAlgebraInvariants = FixedPoints.subalgebra R (SymmetricAlgebra R M) G

The invariant subalgebra is the fixed subalgebra FixedPoints.subalgebra of the bundled action Representation.symmetricAlgebraMulSemiringAction; this holds by definition.

theorem Representation.isHomogeneous_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : DirectSum.SetLike.IsHomogeneous (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraInvariants

The invariant subalgebra is homogeneous: every homogeneous component of an invariant is invariant.

theorem Representation.ι_mem_symmetricAlgebraInvariants_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (m : M) : (SymmetricAlgebra.ι R M) m ∈ ρ.symmetricAlgebraInvariants ↔ ∀ (g : G), (ρ g) m = m

A degree-one element ι m is invariant exactly when m is a fixed vector of ρ.

theorem Representation.map_mem_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] {ρ : Representation R G M} {N : Type u_4} [AddCommMonoid N] [Module R N] {ρ' : Representation R G N} {f : M →ₗ[R] N} (hf : ρ.IsIntertwiningMap ρ' f) {p : SymmetricAlgebra R M} (hp : p ∈ ρ.symmetricAlgebraInvariants) : (SymmetricAlgebra.map R f) p ∈ ρ'.symmetricAlgebraInvariants

The symmetric-algebra map induced by an intertwining map sends invariants to invariants.

theorem Representation.map_symmetricAlgebraInvariants_of_leftInverse {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] {ρ : Representation R G M} {N : Type u_4} [AddCommMonoid N] [Module R N] {ρ' : Representation R G N} {f : M →ₗ[R] N} {s : N →ₗ[R] M} (hf : ρ.IsIntertwiningMap ρ' f) (hs : ρ'.IsIntertwiningMap ρ s) (hfs : Function.LeftInverse ⇑f ⇑s) : Subalgebra.map (SymmetricAlgebra.map R f) ρ.symmetricAlgebraInvariants = ρ'.symmetricAlgebraInvariants

Invariants of an equivariant retract. If f : M → N intertwines ρ with ρ' and has an intertwining right inverse, the induced map carries the invariant subalgebra of ρ onto that of ρ'. For instance, when N is an invariant direct summand of M, every invariant of Sym N is the image of an invariant of Sym M.

theorem Representation.symmetricAlgebraInvariants_comp_of_surjective {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {H : Type u_4} [Monoid H] (f : H →* G) (hf : Function.Surjective ⇑f) : symmetricAlgebraInvariants (MonoidHom.comp ρ f) = ρ.symmetricAlgebraInvariants

Pulling a representation back along a surjective homomorphism does not change its invariant subalgebra in the symmetric algebra. This equality preserves the ambient graded algebra.

noncomputable def Representation.symmetricAlgebraOverInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Representation (↥ρ.symmetricAlgebraInvariants) G (SymmetricAlgebra R M)

The action of G on Sym M induced by ρ, as a representation by linear maps over the invariant subalgebra Sym(M)^G: each ρ g fixes the invariants, so it is linear over them. Its underlying maps are those of Representation.symmetricAlgebra.

@[simp]

theorem Representation.symmetricAlgebraOverInvariants_apply {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (p : SymmetricAlgebra R M) : (ρ.symmetricAlgebraOverInvariants g) p = (ρ.symmetricAlgebra g) p

Over the invariant subalgebra, g acts on Sym M by Representation.symmetricAlgebra.

@[simp]

theorem Representation.ker_symmetricAlgebra {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) : MonoidHom.ker ρ.symmetricAlgebra = MonoidHom.ker ρ

Passing to the symmetric algebra preserves the kernel: an element acts trivially on the algebra exactly when it acts trivially on its degree-one generators.

theorem Representation.symmetricAlgebra_apply_of_mem_ker {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) {g : G} (hg : g ∈ MonoidHom.ker ρ) (p : SymmetricAlgebra R M) : (ρ.symmetricAlgebra g) p = p

The kernel of a representation acts trivially on its entire symmetric algebra.

theorem Representation.isInvariant_symmetricAlgebraInvariants {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) : Algebra.IsInvariant (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M) G

For a group, Sym M is an invariant extension of the invariant subalgebra under the bundled action, so Mathlib's Algebra.IsInvariant API applies to it. This is Mathlib's instance for FixedPoints.subalgebra, transported along symmetricAlgebraInvariants_eq_fixedPoints.

theorem Representation.symmetricAlgebraInvariants_comp_subtype {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) (H : Subgroup G) : symmetricAlgebraInvariants (MonoidHom.comp ρ H.subtype) = FixedPoints.subalgebra R (SymmetricAlgebra R M) ↥H

The invariants of the restriction of ρ to a subgroup H are the fixed points of H under the bundled action of G, so Mathlib's FixedPoints.subalgebra API applies to them.

@[simp]

theorem Representation.toSubmodule_symmetricAlgebraInvariants {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) : Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants = ρ.symmetricAlgebra.invariants

As a submodule, the invariant subalgebra is the module of invariants of the induced representation on Sym M.

theorem Representation.mem_invariants_symmetricAlgebraHomogeneous_iff {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) {n : ℕ} (p : ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) : p ∈ (ρ.symmetricAlgebraHomogeneous n).invariants ↔ ↑p ∈ ρ.symmetricAlgebraInvariants

An element of Symⁿ M is an invariant of the degree-n representation exactly when it lies in the invariant subalgebra.

theorem Representation.mem_invariants_symmetricAlgebraOverInvariants_iff {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) (p : SymmetricAlgebra R M) : p ∈ ρ.symmetricAlgebraOverInvariants.invariants ↔ p ∈ ρ.symmetricAlgebraInvariants

The invariants of the action over the invariant subalgebra are the invariant subalgebra.

theorem Representation.map_subtype_invariants_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) (n : ℕ) : Submodule.map (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n).subtype (ρ.symmetricAlgebraHomogeneous n).invariants = Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

The invariants of the degree-n representation are the degree-n part of the invariant subalgebra.

theorem Representation.finrank_invariants_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) (n : ℕ) : Module.finrank R ↥(ρ.symmetricAlgebraHomogeneous n).invariants = Module.finrank R ↥(Subalgebra.toSubmodule ρ.symmetricAlgebraInvariants ⊓ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)

The invariants of the degree-n representation have the dimension of the degree-n part of the invariant subalgebra.

instance Representation.isIntegral_symmetricAlgebraInvariants {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) [Finite G] : Algebra.IsIntegral (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M)

Integrality over the invariants. For a finite group, the symmetric algebra is integral over the invariant subalgebra: each p is a root of the monic orbit polynomial ∏ g, (X - g • p), whose coefficients are invariant.