Symmetric powers of the standard representation

This file specializes symmetric powers of representations to the standard representation of the general linear group. The resulting action applies a matrix to every factor of a pure symmetric tensor.

A diagonal matrix acts diagonally on the basis of Sym[k]^d (Fin n → k) given by the unordered d-tuples of standard basis vectors, with eigenvalue the product of the corresponding diagonal entries. Summing those eigenvalues, the character of the dth symmetric power at a diagonal matrix is the dth complete homogeneous symmetric polynomial in its diagonal entries, dual to the elementary symmetric polynomial the exterior power gives.

Main definitions

• TauCeti.symPowerRep is the symmetric-power representation of GL n k.
• TauCeti.symPowerFDRep is its bundled finite-dimensional form.

Main results

• TauCeti.char_symPowerRep_diagonal identifies the character on diagonal matrices with a complete homogeneous symmetric polynomial.

References

• Classical groups roadmap, Layer 1, “Symmetric and exterior power representations”.
• The standard-representation specialization is adapted from the formal template in TauCeti.RepresentationTheory.ClassicalGroups.ExteriorPower.

@[reducible, inline]

noncomputable abbrev TauCeti.symPowerRep (k : Type) (n d : ℕ) [CommRing k] : Representation k (GL (Fin n) k) (SymmetricPower k (Fin d) (Fin n → k))

The dth symmetric power of the standard representation of GL n k.

Equations

• TauCeti.symPowerRep k n d = (TauCeti.stdRep k n).symmetricPower d

@[reducible, inline]

noncomputable abbrev TauCeti.symPowerFDRep (k : Type) (n d : ℕ) [CommRing k] : FDRep k (GL (Fin n) k)

The symmetric power of the standard representation, bundled as an object of FDRep.

Equations

• TauCeti.symPowerFDRep k n d = FDRep.of (TauCeti.symPowerRep k n d)

@[simp]

theorem TauCeti.char_symPowerRep_diagonal (k : Type) (n d : ℕ) [Field k] (t : Fin n → kˣ) : (symPowerRep k n d).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (MvPolynomial.hsymm (Fin n) k d)

The character of the dth symmetric power on a diagonal matrix is the dth complete homogeneous symmetric polynomial in its diagonal entries.

@[simp]

theorem TauCeti.char_symPowerFDRep_diagonal (k : Type) (n d : ℕ) [Field k] (t : Fin n → kˣ) : (symPowerFDRep k n d).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (MvPolynomial.hsymm (Fin n) k d)

The character of the bundled dth symmetric power on a diagonal matrix is the dth complete homogeneous symmetric polynomial in its diagonal entries.