The symmetric homogeneous polynomials of a fixed degree

The symmetric polynomials of Mathlib.RingTheory.MvPolynomial.Symmetric.Defs are graded by total degree, each graded piece being the intersection of MvPolynomial.symmetricSubalgebra with the homogeneous polynomials MvPolynomial.homogeneousSubmodule of that degree. This file names that intersection, TauCeti.symmetricHomogeneousSubmodule, and nothing else; it is the module the classical families of symmetric polynomials are bases of, one degree at a time: the monomial symmetric polynomials over any commutative semiring, and the Schur polynomials over a commutative ring.

Main definitions

• TauCeti.symmetricHomogeneousSubmodule σ R n: the polynomials in σ over R that are both symmetric and homogeneous of degree n.

Main results

• MvPolynomial.isHomogeneous_esymm: the elementary symmetric polynomial eₖ is homogeneous of degree k.

noncomputable def TauCeti.symmetricHomogeneousSubmodule (σ : Type u_1) (R : Type u_2) [CommSemiring R] (n : ℕ) : Submodule R (MvPolynomial σ R)

The symmetric polynomials of degree n: those polynomials in the alphabet σ over R that are both symmetric and homogeneous of degree n. The monomial symmetric polynomials of the partitions of n are a basis of this module over any commutative semiring; the Schur polynomials of those partitions are a basis of it over a commutative ring.

Equations

• TauCeti.symmetricHomogeneousSubmodule σ R n = Subalgebra.toSubmodule (MvPolynomial.symmetricSubalgebra σ R) ⊓ MvPolynomial.homogeneousSubmodule σ R n

@[simp]

theorem TauCeti.mem_symmetricHomogeneousSubmodule {σ : Type u_1} {R : Type u_2} [CommSemiring R] {n : ℕ} {p : MvPolynomial σ R} : p ∈ symmetricHomogeneousSubmodule σ R n ↔ p.IsSymmetric ∧ p.IsHomogeneous n

Membership in TauCeti.symmetricHomogeneousSubmodule is the conjunction of the two conditions defining it.

theorem MvPolynomial.isHomogeneous_esymm {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (k : ℕ) : (esymm σ R k).IsHomogeneous k

The elementary symmetric polynomial eₖ is homogeneous of degree k.