The power sums generate the symmetric polynomials over a ℚ-algebra

Let σ be a finite alphabet and R a commutative ℚ-algebra, for instance ℚ itself or ℂ. Newton's identities MvPolynomial.mul_esymm_eq_sum,

k eₖ = (-1) ^ (k + 1) ∑_{a + b = k, a < k} (-1) ^ a e_a p_b,

are triangular: they express k eₖ through p₁, …, pₖ and the lower e_a. Once the integers are invertible they therefore write every elementary symmetric polynomial eₖ as a polynomial in the power sums p₁, …, pₖ, and the fundamental theorem of symmetric polynomials (MvPolynomial.esymmAlgHom_surjective) turns this into generation: the power sums p₁, …, pₙ generate the symmetric polynomials as an R-algebra whenever the alphabet has at most n letters. Over ℤ this fails already for two letters, where e₂ = (p₁² - p₂) / 2.

Graded by degree, generation says that the power-sum products p_μ = ∏ᵢ p_{μᵢ} of the partitions μ of n span the symmetric polynomials of degree n. When the alphabet has at least n letters there are exactly as many of them as there are monomial symmetric polynomials of degree n, and a spanning family of that size in a free module over a commutative ring is a basis (linearIndependent_of_top_le_span_of_card_eq_finrank). This is the power-sum basis, in which the Frobenius characteristic (1 / n!) ∑_π f(π) p_{ρ(π)} of a class function f of Sₙ is expanded; by spanning, two linear maps out of the symmetric polynomials of degree n agree as soon as they agree on every p_μ.

Main definitions

• TauCeti.psumPartBasis: for an alphabet with at least n letters, the power-sum products of the partitions of n as a basis of the symmetric polynomials of degree n.

Main results

• TauCeti.esymm_mem_adjoin_psum: eₖ lies in the subalgebra generated by p₁, …, pₖ.
• TauCeti.adjoin_psum_Icc_eq_symmetricSubalgebra: the power sums p₁, …, pₙ generate the symmetric polynomials in at most n variables.
• TauCeti.adjoin_range_psum_eq_symmetricSubalgebra: the power sums generate the symmetric polynomials.
• TauCeti.span_psumPart_eq_symmetricHomogeneousSubmodule: the power-sum products of the partitions of n span the symmetric polynomials of degree n.
• TauCeti.linearIndependent_psumPart: in at least n variables they are linearly independent.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 2: Newton's formulas, and the power sums as generators and the p_λ as a basis of the symmetric functions over ℚ.

Generation as an algebra

theorem TauCeti.esymm_mem_adjoin_psum (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] (k : ℕ) : MvPolynomial.esymm σ R k ∈ Algebra.adjoin R (MvPolynomial.psum σ R '' Set.Icc 1 k)

Newton's identities express eₖ through the power sums: over a ℚ-algebra the elementary symmetric polynomial eₖ is a polynomial in the power sums p₁, …, pₖ.

theorem TauCeti.adjoin_psum_Icc_eq_symmetricSubalgebra (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : Fintype.card σ ≤ n) : Algebra.adjoin R (MvPolynomial.psum σ R '' Set.Icc 1 n) = MvPolynomial.symmetricSubalgebra σ R

The power sums generate the symmetric polynomials: over a ℚ-algebra, the power sums p₁, …, pₙ generate the symmetric polynomials in an alphabet of at most n letters as an algebra.

theorem TauCeti.adjoin_range_psum_eq_symmetricSubalgebra (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] : Algebra.adjoin R (Set.range (MvPolynomial.psum σ R)) = MvPolynomial.symmetricSubalgebra σ R

Over a ℚ-algebra, the power sums generate the symmetric polynomials as an algebra.

The power-sum products in a fixed degree

theorem TauCeti.span_psumPart_eq_symmetricHomogeneousSubmodule (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] (n : ℕ) : Submodule.span R (Set.range (MvPolynomial.psumPart σ R)) = symmetricHomogeneousSubmodule σ R n

The power-sum products span the symmetric polynomials of degree n: over a ℚ-algebra, the products p_μ = ∏ᵢ p_{μᵢ} over the partitions μ of n span the symmetric polynomials that are homogeneous of degree n.

noncomputable def TauCeti.psumPartBasis (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : n ≤ Fintype.card σ) : Module.Basis n.Partition R ↥(symmetricHomogeneousSubmodule σ R n)

The power-sum basis: over a ℚ-algebra and in an alphabet of at least n letters, the power-sum products p_μ of the partitions μ of n form a basis of the symmetric polynomials of degree n.

@[simp]

theorem TauCeti.coe_psumPartBasis (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : n ≤ Fintype.card σ) (μ : n.Partition) : ↑((psumPartBasis σ R hn) μ) = MvPolynomial.psumPart σ R μ

The vectors of the power-sum basis are the power-sum products.

theorem TauCeti.linearIndependent_psumPart (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] [Algebra ℚ R] {n : ℕ} (hn : n ≤ Fintype.card σ) : LinearIndependent R (MvPolynomial.psumPart σ R)

The power-sum products are linearly independent: over a ℚ-algebra and in an alphabet of at least n letters, the products p_μ over the partitions μ of n are linearly independent.