Graded traces on a symmetric algebra

An endomorphism f of a module M acts on each homogeneous component Symⁿ M of the symmetric algebra, by the restriction of SymmetricAlgebra.map f. When f is diagonal in a finite basis, with eigenvalues aᵢ, the monomials in that basis are eigenvectors of the induced map, so its trace on Symⁿ M is the complete homogeneous symmetric polynomial hₙ(a). Collecting these traces into a power series gives the graded trace formula

∑ₙ tr(f | Symⁿ M) tⁿ = det(1 - t f)⁻¹,

stated as (∑ₙ tr(f | Symⁿ M) tⁿ) * det(1 - t f) = 1 in R⟦t⟧, with det(1 - t f) the reverse of the characteristic polynomial of f. Averaged over a finite group acting on M = V*, this is the term-by-term content of Molien's formula for the Hilbert series of the invariants of Sym(V*).

Main results

• Module.Basis.homogeneousSubmoduleMapₛₗ_symmetricAlgebraHomogeneous_of_apply: an endomorphism diagonal in a basis is diagonal in the induced monomial basis of Symⁿ M.
• Module.Basis.trace_homogeneousSubmoduleMapₛₗ_of_apply: its trace on Symⁿ M is the sum of the eigenvalue products over the degree-n multisets of basis indices.
• Module.Basis.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_apply: the graded trace formula.
• Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_iSup_eigenspace_eq_top: the graded trace formula for an endomorphism of a finite-dimensional vector space whose eigenspaces span, which therefore has an eigenbasis.
• Module.End.IsSemisimple.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly: the case of a semisimple endomorphism over an algebraically closed field.
• Module.End.trace_homogeneousSubmoduleMapₛₗ_baseChange: the trace on Symⁿ M commutes with scalar extension.
• Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_pow_eq_one: the graded trace formula for an endomorphism of finite order n, with n nonzero in the field, over an arbitrary field. Such an endomorphism is diagonalizable over an algebraic closure, and the formula descends because both of its factors commute with scalar extension.

References

• T. Molien, Über die Invarianten der linearen Substitutionsgruppen, Sitzungsber. Königl. Preuss. Akad. Wiss. (1897), 1152–1156.
• R. P. Stanley, Invariants of finite groups and their applications to combinatorics, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 475–511, Theorem 2.1.

theorem Module.Basis.homogeneousSubmoduleMapₛₗ_symmetricAlgebraHomogeneous_of_apply {R : Type u_1} {M : Type u_2} {κ : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (hf : ∀ (i : κ), f (b i) = a i • b i) (n : ℕ) (s : Sym κ n) : (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n) ((b.symmetricAlgebraHomogeneous n) s) = (Multiset.map a ↑s).prod • (b.symmetricAlgebraHomogeneous n) s

An endomorphism diagonal in a basis is diagonal in the monomial basis of Symⁿ M: the monomial indexed by s is an eigenvector of the induced map, with eigenvalue the product of the eigenvalues listed by s.

theorem Module.Basis.trace_homogeneousSubmoduleMapₛₗ_of_apply {R : Type u_1} {M : Type u_2} {κ : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype κ] [DecidableEq κ] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (hf : ∀ (i : κ), f (b i) = a i • b i) (n : ℕ) : (LinearMap.trace R ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n) = ∑ s : Sym κ n, (Multiset.map a ↑s).prod

The trace on Symⁿ M of an endomorphism diagonal in a finite basis is the sum, over the degree-n multisets of basis indices, of the product of the corresponding eigenvalues: the complete homogeneous symmetric polynomial hₙ evaluated at the eigenvalues.

theorem Module.Basis.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_apply {R : Type u_1} {M : Type u_2} {κ : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] (b : Basis κ R M) (f : M →ₗ[R] M) (a : κ → R) (hf : ∀ (i : κ), f (b i) = a i • b i) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace R ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n)) * ↑f.charpoly.reverse = 1

The graded trace formula. If f is diagonal in a finite basis, the generating function of its traces on the homogeneous components of the symmetric algebra is the inverse of det(1 - t f), the reverse of the characteristic polynomial of f: (∑ₙ tr(f | Symⁿ M) tⁿ) * det(1 - t f) = 1.

@[simp]

theorem Module.End.trace_homogeneousSubmoduleMapₛₗ_baseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (n : ℕ) (S : Type u_4) [CommRing S] [Algebra R S] : (LinearMap.trace S ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule S (TensorProduct R S M) n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ (LinearMap.baseChange S f) n) = (algebraMap R S) ((LinearMap.trace R ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n))

Graded traces commute with scalar extension: the trace of f ⊗ 1 on Symⁿ (S ⊗[R] M) is the image in S of the trace of f on Symⁿ M.

theorem Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_iSup_eigenspace_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (h : ⨆ (μ : K), f.eigenspace μ = ⊤) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K V n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n)) * ↑(LinearMap.charpoly f).reverse = 1

The graded trace formula for a diagonalizable endomorphism of a finite-dimensional vector space, one whose eigenspaces span: (∑ₙ tr(f | Symⁿ V) tⁿ) * det(1 - t f) = 1.

theorem Module.End.IsSemisimple.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [IsAlgClosed K] {f : End K V} (hf : f.IsSemisimple) : (PowerSeries.mk fun (n : ℕ) => (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K V n)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f n)) * ↑(LinearMap.charpoly f).reverse = 1

The graded trace formula for a semisimple endomorphism of a finite-dimensional vector space over an algebraically closed field: (∑ₙ tr(f | Symⁿ V) tⁿ) * det(1 - t f) = 1.

theorem Module.End.mk_trace_homogeneousSubmoduleMapₛₗ_mul_reverse_charpoly_of_pow_eq_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} {n : ℕ} (hn : ↑n ≠ 0) (hf : f ^ n = 1) : (PowerSeries.mk fun (m : ℕ) => (LinearMap.trace K ↥(TauCeti.SymmetricAlgebra.homogeneousSubmodule K V m)) (TauCeti.SymmetricAlgebra.homogeneousSubmoduleMapₛₗ f m)) * ↑(LinearMap.charpoly f).reverse = 1

The graded trace formula for an endomorphism of finite order of a finite-dimensional vector space over an arbitrary field: if f ^ n = 1 with n nonzero in K, then (∑ₘ tr(f | Symᵐ V) tᵐ) * det(1 - t f) = 1.

No eigenvalue of f need lie in K: over an algebraic closure f becomes diagonalizable, and both factors commute with scalar extension (Module.End.trace_homogeneousSubmoduleMapₛₗ_baseChange, LinearMap.charpoly_baseChange).