Definitions and Examples of Symmetric Polynomials

This file formalizes the definitions and basic properties of symmetric polynomials, following Section "Definitions and examples of symmetric polynomials" (sec.sf.sp) of the source.

Main definitions

• We use Mathlib's MvPolynomial.IsSymmetric for the notion of symmetric polynomials.
• MvPolynomial.symmetricSubalgebra σ R is the ring of symmetric polynomials.
• MvPolynomial.esymm σ R n is the n-th elementary symmetric polynomial.
• MvPolynomial.hsymm σ R n is the n-th complete homogeneous symmetric polynomial.
• MvPolynomial.psum σ R n is the n-th power sum.

Main results

• The symmetric group acts on polynomials by permuting variables (Proposition prop.sf.SN-acts)
• The action is by K-algebra automorphisms (Proposition prop.sf.SN-acts-by-alg-auts)
• The set of symmetric polynomials forms a K-subalgebra (Theorem thm.sf.S-subalg)
• For n > N, the n-th elementary symmetric polynomial is zero (Proposition prop.sf.en=0)
• Newton-Girard formulas relating e_n, h_n, and p_n (Theorem thm.sf.NG)
• Fundamental Theorem of Symmetric Polynomials (Theorem thm.sf.ftsf)
• A polynomial is symmetric iff it is invariant under simple transpositions (Lemma lem.sf.simples-enough)

References

• Source: SymmetricFunctions/Definitions.tex, sec.sf.sp

Implementation notes

Mathlib already provides extensive support for symmetric polynomials via MvPolynomial.IsSymmetric and related definitions. This file connects the textbook presentation to Mathlib's API and provides additional lemmas following the source material.

The symmetric group action on polynomials is given by MvPolynomial.rename in Mathlib. For a permutation σ : Equiv.Perm (Fin N), the action σ · f is MvPolynomial.rename σ f.

Convention (Convention conv.sf.KN)

We fix a commutative ring K and a natural number N throughout. The polynomial ring P = K[x₁, x₂, ..., x_N] is MvPolynomial (Fin N) K in Mathlib.

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricPolynomials.P (K : Type u_2) [CommRing K] (N : ℕ) : Type u_2

The polynomial ring in N variables over K. This corresponds to 𝒫 in the source (Definition def.sf.PS (a)). Label: def.sf.PS

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.P K N = MvPolynomial (Fin N) K

The Symmetric Group Action (Definition def.sf.PS (b))

The symmetric group S_N acts on P by permuting variables: σ · f = f[x_{σ(1)}, x_{σ(2)}, ..., x_{σ(N)}]

In Mathlib, this is given by MvPolynomial.rename σ f where σ : Equiv.Perm (Fin N).

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.permAction {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f : P K N) : P K N

The action of a permutation on a polynomial by renaming variables. This is σ · f = f[x_{σ(1)}, ..., x_{σ(N)}] in the source. Label: def.sf.PS

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.permAction σ f = (MvPolynomial.rename ⇑σ) f

def AlgebraicCombinatorics.SymmetricPolynomials.«term_•ₚ_» : Lean.TrailingParserDescr

Notation: σ • f for the permutation action

Equations

• One or more equations did not get rendered due to their size.

Proposition prop.sf.SN-acts: The action is a well-defined group action

(a) id · f = f for every f ∈ P (b) (στ) · f = σ · (τ · f) for every σ, τ ∈ S_N and f ∈ P

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_id {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : permAction 1 f = f

The identity permutation acts trivially (Proposition prop.sf.SN-acts (a)). Label: prop.sf.SN-acts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_mul {K : Type u_1} [CommRing K] {N : ℕ} (σ τ : Equiv.Perm (Fin N)) (f : P K N) : permAction (σ * τ) f = permAction σ (permAction τ f)

Composition of permutation actions (Proposition prop.sf.SN-acts (b)). Label: prop.sf.SN-acts

noncomputable instance AlgebraicCombinatorics.SymmetricPolynomials.permMulAction {K : Type u_1} [CommRing K] {N : ℕ} : MulAction (Equiv.Perm (Fin N)) (P K N)

The symmetric group action on polynomials is a well-defined MulAction. This formalizes Proposition prop.sf.SN-acts in the standard Mathlib form:

• one_smul corresponds to part (a): id · f = f
• mul_smul corresponds to part (b): (στ) · f = σ · (τ · f) Label: prop.sf.SN-acts

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.permMulAction = { smul := AlgebraicCombinatorics.SymmetricPolynomials.permAction, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.smul_eq_permAction {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f : P K N) : σ • f = permAction σ f

The Mathlib smul action agrees with our permAction notation. Label: prop.sf.SN-acts

Definition of Symmetric Polynomials (Definition def.sf.PS (c)(d))

A polynomial f ∈ P is symmetric if σ · f = f for all σ ∈ S_N. The set S of all symmetric polynomials is symmetricSubalgebra (Fin N) K in Mathlib.

def AlgebraicCombinatorics.SymmetricPolynomials.IsSymm {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : Prop

A polynomial is symmetric if it is invariant under all permutations. This is Definition def.sf.PS (c) in the source. Label: def.sf.PS

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.IsSymm f = MvPolynomial.IsSymmetric f

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricPolynomials.S (K : Type u_2) [CommRing K] (N : ℕ) : Subalgebra K (P K N)

The ring of symmetric polynomials in N variables over K.

This is the K-subalgebra S of P consisting of all symmetric polynomials, i.e., polynomials f such that σ · f = f for all permutations σ ∈ S_N.

The terminology "ring of symmetric polynomials" comes from the fact that this subalgebra is closed under addition, multiplication, and scalar multiplication by elements of K (Theorem thm.sf.S-subalg).

Label: def.sf.ring-of-symm

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.S K N = MvPolynomial.symmetricSubalgebra (Fin N) K

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricPolynomials.ringOfSymmetricPolynomials (K : Type u_2) [CommRing K] (N : ℕ) : Subalgebra K (P K N)

Alternative name: the ring of symmetric polynomials. This is the standard terminology for the subalgebra S. Label: def.sf.ring-of-symm

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.ringOfSymmetricPolynomials K N = AlgebraicCombinatorics.SymmetricPolynomials.S K N

Additional API for Definition def.sf.PS

These lemmas provide useful characterizations of the definitions.

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_def {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : IsSymm f ↔ ∀ (σ : Equiv.Perm (Fin N)), (MvPolynomial.rename ⇑σ) f = f

The definition of IsSymm unfolds to: f is symmetric iff rename σ f = f for all σ. Label: def.sf.PS

theorem AlgebraicCombinatorics.SymmetricPolynomials.mem_S_iff {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : f ∈ S K N ↔ IsSymm f

Membership in S is equivalent to being symmetric. Label: def.sf.PS

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_eq_rename {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f : P K N) : permAction σ f = (MvPolynomial.rename ⇑σ) f

The permutation action definition: σ •ₚ f = rename σ f. Label: def.sf.PS

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_iff_permAction {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : IsSymm f ↔ ∀ (σ : Equiv.Perm (Fin N)), permAction σ f = f

A polynomial is symmetric iff the permutation action fixes it. Label: def.sf.PS

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_sum_X {K : Type u_1} [CommRing K] {N : ℕ} : IsSymm (∑ i : Fin N, MvPolynomial.X i)

Example: The sum ∑ xᵢ is symmetric (Example exa.sf.PS1 (a)). Label: exa.sf.PS1

noncomputable instance AlgebraicCombinatorics.SymmetricPolynomials.P_isCommRing' {K : Type u_1} [CommRing K] {N : ℕ} : CommRing (P K N)

The polynomial ring P K N is a commutative K-algebra. Label: def.sf.PS

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.P_isCommRing' = inferInstance

noncomputable instance AlgebraicCombinatorics.SymmetricPolynomials.P_isAlgebra' {K : Type u_1} [CommRing K] {N : ℕ} : Algebra K (P K N)

The polynomial ring P K N is a K-algebra. Label: def.sf.PS

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.P_isAlgebra' = inferInstance

Proposition prop.sf.SN-acts-by-alg-auts: The action is by K-algebra automorphisms

For each σ ∈ S_N, the map f ↦ σ · f is a K-algebra automorphism of P.

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_add {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f g : P K N) : permAction σ (f + g) = permAction σ f + permAction σ g

The permutation action preserves addition. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_mul' {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f g : P K N) : permAction σ (f * g) = permAction σ f * permAction σ g

The permutation action preserves multiplication. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_smul {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (c : K) (f : P K N) : permAction σ (c • f) = c • permAction σ f

The permutation action preserves scaling. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_inv {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f : P K N) : permAction σ⁻¹ (permAction σ f) = f

The permutation action is invertible with inverse σ⁻¹. Label: prop.sf.SN-acts-by-alg-auts

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) : P K N ≃ₐ[K] P K N

The K-algebra automorphism of P induced by a permutation σ. This is the main object of Proposition prop.sf.SN-acts-by-alg-auts: for each σ ∈ S_N, the map f ↦ σ · f is a K-algebra automorphism. Label: prop.sf.SN-acts-by-alg-auts

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism σ = MvPolynomial.renameEquiv K σ

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAction_eq_permAutomorphism {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (f : P K N) : permAction σ f = (permAutomorphism σ) f

The permutation action equals the automorphism applied to the polynomial. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_zero {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) : (permAutomorphism σ) 0 = 0

The permutation automorphism preserves zero. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_one {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) : (permAutomorphism σ) 1 = 1

The permutation automorphism preserves one. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_C {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) (c : K) : (permAutomorphism σ) (MvPolynomial.C c) = MvPolynomial.C c

The permutation automorphism preserves constants. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_id {K : Type u_1} [CommRing K] {N : ℕ} : permAutomorphism 1 = AlgEquiv.refl

The identity permutation gives the identity automorphism. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_mul_perm {K : Type u_1} [CommRing K] {N : ℕ} (σ τ : Equiv.Perm (Fin N)) : permAutomorphism (σ * τ) = permAutomorphism σ * permAutomorphism τ

Composition of permutation automorphisms: (σ * τ) acts as τ then σ. Note: In AlgEquiv, f * g = g.trans f (apply g first, then f). Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_symm {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) : (permAutomorphism σ).symm = permAutomorphism σ⁻¹

The inverse automorphism is given by the inverse permutation. Label: prop.sf.SN-acts-by-alg-auts

theorem AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphism_bijective {K : Type u_1} [CommRing K] {N : ℕ} (σ : Equiv.Perm (Fin N)) : Function.Bijective ⇑(permAutomorphism σ)

The permutation automorphism is bijective. Label: prop.sf.SN-acts-by-alg-auts

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.permAutomorphismHom {K : Type u_1} [CommRing K] {N : ℕ} : Equiv.Perm (Fin N) →* P K N ≃ₐ[K] P K N

The map from S_N to Aut_K(P) is a group homomorphism. This is the full content of Proposition prop.sf.SN-acts-by-alg-auts: S_N acts on P by K-algebra automorphisms. Label: prop.sf.SN-acts-by-alg-auts

Equations

• One or more equations did not get rendered due to their size.

Theorem thm.sf.S-subalg: S is a K-subalgebra of P

The set of symmetric polynomials is closed under addition, multiplication, and scaling, and contains 0 and 1.

From the source (AlgebraicCombinatorics/tex/SymmetricFunctions/Definitions.tex, Theorem thm.sf.S-subalg):

The subset S is a K-subalgebra of P.

A K-subalgebra of P must satisfy:

1. S contains 0 and 1
2. S is closed under addition
3. S is closed under multiplication
4. S is closed under scalar multiplication by elements of K

This section proves all these properties both in terms of IsSymm (the predicate) and ∈ S K N (membership in the subalgebra).

def AlgebraicCombinatorics.SymmetricPolynomials.S_subalgebra {K : Type u_1} [CommRing K] {N : ℕ} : Subalgebra K (P K N)

Theorem thm.sf.S-subalg: The symmetric polynomials form a K-subalgebra of P.

This is the main theorem stating that the set S of symmetric polynomials is a K-subalgebra of the polynomial ring P = K[x₁, x₂, ..., x_N].

A K-subalgebra satisfies:

• (a) S contains 0 and 1 (see S_zero_mem, S_one_mem)
• (b) S is closed under addition (see S_add_mem)
• (c) S is closed under multiplication (see S_mul_mem)
• (d) S is closed under scalar multiplication by K (see S_smul_mem)

The definition S K N := symmetricSubalgebra (Fin N) K directly provides the Subalgebra K (P K N) structure, which bundles all these properties.

Label: thm.sf.S-subalg

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.S_subalgebra = AlgebraicCombinatorics.SymmetricPolynomials.S K N

Part (a): S contains 0 and 1

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_zero_mem {K : Type u_1} [CommRing K] {N : ℕ} : 0 ∈ S K N

Zero is in S (Theorem thm.sf.S-subalg, part (a)). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_one_mem {K : Type u_1} [CommRing K] {N : ℕ} : 1 ∈ S K N

One is in S (Theorem thm.sf.S-subalg, part (a)). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_zero {K : Type u_1} [CommRing K] {N : ℕ} : IsSymm 0

Zero is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_one {K : Type u_1} [CommRing K] {N : ℕ} : IsSymm 1

One is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_C_mem {K : Type u_1} [CommRing K] {N : ℕ} (c : K) : MvPolynomial.C c ∈ S K N

Constants are in S (Theorem thm.sf.S-subalg, part (a) generalized). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_C {K : Type u_1} [CommRing K] {N : ℕ} (c : K) : IsSymm (MvPolynomial.C c)

Constants are symmetric. Label: thm.sf.S-subalg

Part (b): S is closed under addition

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_add_mem {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : f ∈ S K N) (hg : g ∈ S K N) : f + g ∈ S K N

S is closed under addition (Theorem thm.sf.S-subalg, part (b)). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_add {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : IsSymm f) (hg : IsSymm g) : IsSymm (f + g)

Sum of symmetric polynomials is symmetric. Label: thm.sf.S-subalg

Part (c): S is closed under multiplication

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_mul_mem {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : f ∈ S K N) (hg : g ∈ S K N) : f * g ∈ S K N

S is closed under multiplication (Theorem thm.sf.S-subalg, part (c)). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_mul {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : IsSymm f) (hg : IsSymm g) : IsSymm (f * g)

Product of symmetric polynomials is symmetric. Label: thm.sf.S-subalg

Part (d): S is closed under scalar multiplication

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_smul_mem {K : Type u_1} [CommRing K] {N : ℕ} (c : K) {f : P K N} (hf : f ∈ S K N) : c • f ∈ S K N

S is closed under scalar multiplication (Theorem thm.sf.S-subalg, part (d)). Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_smul {K : Type u_1} [CommRing K] {N : ℕ} (c : K) {f : P K N} (hf : IsSymm f) : IsSymm (c • f)

Scalar multiple of a symmetric polynomial is symmetric. Label: thm.sf.S-subalg

Additional closure properties (consequences of being a K-subalgebra)

These properties follow automatically from S being a K-subalgebra.

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_neg_mem {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : f ∈ S K N) : -f ∈ S K N

S is closed under negation. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_neg {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : IsSymm f) : IsSymm (-f)

Negation of a symmetric polynomial is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_sub_mem {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : f ∈ S K N) (hg : g ∈ S K N) : f - g ∈ S K N

S is closed under subtraction. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_sub {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : IsSymm f) (hg : IsSymm g) : IsSymm (f - g)

Difference of symmetric polynomials is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_pow_mem {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : f ∈ S K N) (n : ℕ) : f ^ n ∈ S K N

S is closed under powers. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_pow {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : IsSymm f) (n : ℕ) : IsSymm (f ^ n)

Power of a symmetric polynomial is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_sum_mem {K : Type u_1} [CommRing K] {N : ℕ} {ι : Type u_2} {s : Finset ι} {f : ι → P K N} (hf : ∀ i ∈ s, f i ∈ S K N) : ∑ i ∈ s, f i ∈ S K N

S is closed under finite sums. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_sum {K : Type u_1} [CommRing K] {N : ℕ} {ι : Type u_2} {s : Finset ι} {f : ι → P K N} (hf : ∀ i ∈ s, IsSymm (f i)) : IsSymm (∑ i ∈ s, f i)

Finite sum of symmetric polynomials is symmetric. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.S_prod_mem {K : Type u_1} [CommRing K] {N : ℕ} {ι : Type u_2} {s : Finset ι} {f : ι → P K N} (hf : ∀ i ∈ s, f i ∈ S K N) : ∏ i ∈ s, f i ∈ S K N

S is closed under finite products. Label: thm.sf.S-subalg

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_prod {K : Type u_1} [CommRing K] {N : ℕ} {ι : Type u_2} {s : Finset ι} {f : ι → P K N} (hf : ∀ i ∈ s, IsSymm (f i)) : IsSymm (∏ i ∈ s, f i)

Finite product of symmetric polynomials is symmetric. Label: thm.sf.S-subalg

Definition of Monomials (Definition def.sf.monomial)

(a) A monomial is x₁^{a₁} x₂^{a₂} ⋯ x_N^{a_N} with a_i ∈ ℕ (b) The degree of a monomial is a₁ + a₂ + ⋯ + a_N (c) A monomial is squarefree if all a_i ∈ {0, 1} (d) A monomial is primal if at most one a_i > 0

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricPolynomials.Monomial (N : ℕ) : Type

A monomial represented by its exponent vector. In the textbook, a monomial is x₁^{a₁} x₂^{a₂} ⋯ x_N^{a_N}. We represent it by the exponent vector (a₁, a₂, ..., a_N) ∈ ℕ^N. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.Monomial N = (Fin N →₀ ℕ)

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.toPoly {K : Type u_1} [CommRing K] {N : ℕ} (m : Monomial N) : P K N

Convert a monomial (exponent vector) to the corresponding polynomial x₁^{a₁} ⋯ x_N^{a_N}. Label: def.sf.monomial

Equations

• m.toPoly = (MvPolynomial.monomial m) 1

def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree {N : ℕ} (m : Monomial N) : ℕ

The degree of a monomial is the sum of its exponents. Label: def.sf.monomial

Equations

• m.degree = Finsupp.sum m fun (x : Fin N) (a : ℕ) => a

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_eq_support_sum {N : ℕ} (m : Monomial N) : m.degree = m.support.sum ⇑m

Alternative characterization: degree equals the support sum. Label: def.sf.monomial

def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.IsSquarefree {N : ℕ} (m : Monomial N) : Prop

A monomial is squarefree if all exponents are 0 or 1. Label: def.sf.monomial

Equations

• m.IsSquarefree = ∀ (i : Fin N), m i ≤ 1

def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.IsPrimal {N : ℕ} (m : Monomial N) : Prop

A monomial is primal if at most one exponent is positive. This means the monomial is either 1 or a power of a single variable. Label: def.sf.monomial

Equations

• m.IsPrimal = (m.support.card ≤ 1)

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_eq_totalDegree {K : Type u_1} [CommRing K] {N : ℕ} [Nontrivial K] (m : Monomial N) : m.degree = MvPolynomial.totalDegree m.toPoly

The degree of a monomial equals the total degree of its polynomial representation (when K is nontrivial). Label: def.sf.monomial

def AlgebraicCombinatorics.SymmetricPolynomials.monomialsOfDegree (N n : ℕ) : Set (Monomial N)

The set of all monomials of a given degree n. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.monomialsOfDegree N n = {m : AlgebraicCombinatorics.SymmetricPolynomials.Monomial N | m.degree = n}

def AlgebraicCombinatorics.SymmetricPolynomials.squarefreeMonomials (N n : ℕ) : Set (Monomial N)

The set of all squarefree monomials of a given degree n. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.squarefreeMonomials N n = {m : AlgebraicCombinatorics.SymmetricPolynomials.Monomial N | m.IsSquarefree ∧ m.degree = n}

def AlgebraicCombinatorics.SymmetricPolynomials.primalMonomials (N n : ℕ) : Set (Monomial N)

The set of all primal monomials of a given degree n. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.primalMonomials N n = {m : AlgebraicCombinatorics.SymmetricPolynomials.Monomial N | m.IsPrimal ∧ m.degree = n}

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.toPoly_zero {K : Type u_1} [CommRing K] {N : ℕ} : toPoly 0 = 1

The zero monomial (all exponents zero) represents 1. Label: def.sf.monomial

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_zero {N : ℕ} : degree 0 = 0

The degree of the zero monomial is 0. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isSquarefree_zero {N : ℕ} : IsSquarefree 0

The zero monomial is squarefree. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isPrimal_zero {N : ℕ} : IsPrimal 0

The zero monomial is primal. Label: def.sf.monomial

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.single {N : ℕ} (i : Fin N) : Monomial N

A single variable x_i corresponds to the monomial with exponent 1 at position i. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.Monomial.single i = fun₀ | i => 1

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.toPoly_single {K : Type u_1} [CommRing K] {N : ℕ} (i : Fin N) : (single i).toPoly = MvPolynomial.X i

The polynomial corresponding to Monomial.single i is X i. Label: def.sf.monomial

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_single {N : ℕ} (i : Fin N) : (single i).degree = 1

The degree of a single variable monomial is 1. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isSquarefree_single {N : ℕ} (i : Fin N) : (single i).IsSquarefree

A single variable monomial is squarefree. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isPrimal_single {N : ℕ} (i : Fin N) : (single i).IsPrimal

A single variable monomial is primal. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.toPoly_add {K : Type u_1} [CommRing K] {N : ℕ} (m₁ m₂ : Monomial N) : (m₁ + m₂).toPoly = m₁.toPoly * m₂.toPoly

Multiplication of monomials corresponds to addition of exponent vectors. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_add {N : ℕ} (m₁ m₂ : Monomial N) : (m₁ + m₂).degree = m₁.degree + m₂.degree

The degree of a product of monomials is the sum of degrees. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_le_of_isSquarefree {N : ℕ} (m : Monomial N) (hm : m.IsSquarefree) : m.degree ≤ N

A squarefree monomial has degree at most N. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.support_card_le_one_of_isPrimal {N : ℕ} (m : Monomial N) (hm : m.IsPrimal) : m.support.card ≤ 1

A primal monomial has support of size at most 1. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isPrimal_iff {N : ℕ} (m : Monomial N) : m.IsPrimal ↔ m = 0 ∨ ∃ (i : Fin N) (k : ℕ), (m = fun₀ | i => k) ∧ 0 < k

Characterization: a monomial is primal iff it's 0 or a power of a single variable. Label: def.sf.monomial

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.Monomial.ofFinset {N : ℕ} (s : Finset (Fin N)) : Monomial N

The monomial corresponding to a subset S ⊆ [N] is ∏_{i ∈ S} x_i. This is the squarefree monomial with support S. Label: def.sf.monomial

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.Monomial.ofFinset s = ∑ x ∈ s, fun₀ | x => 1

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.toPoly_ofFinset {K : Type u_1} [CommRing K] {N : ℕ} (s : Finset (Fin N)) : (ofFinset s).toPoly = ∏ i ∈ s, MvPolynomial.X i

The polynomial corresponding to Monomial.ofFinset s is ∏_{i ∈ s} X i. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.isSquarefree_ofFinset {N : ℕ} (s : Finset (Fin N)) : (ofFinset s).IsSquarefree

Monomial.ofFinset gives a squarefree monomial. Label: def.sf.monomial

@[simp]

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.degree_ofFinset {N : ℕ} (s : Finset (Fin N)) : (ofFinset s).degree = s.card

The degree of Monomial.ofFinset s is the cardinality of s. Label: def.sf.monomial

theorem AlgebraicCombinatorics.SymmetricPolynomials.Monomial.support_ofFinset {N : ℕ} (s : Finset (Fin N)) : (ofFinset s).support = s

The support of Monomial.ofFinset s equals s. Label: def.sf.monomial

Elementary Symmetric Polynomials (Definition def.sf.ehp (a))

e_n = sum of all squarefree monomials of degree n = ∑{i₁ < i₂ < ... < i_n} x{i₁} x_{i₂} ⋯ x_{i_n}

In Mathlib, this is MvPolynomial.esymm (Fin N) K n.

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.SymmetricPolynomials.e {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : P K N

The n-th elementary symmetric polynomial. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.e n = MvPolynomial.esymm (Fin N) K n

theorem AlgebraicCombinatorics.SymmetricPolynomials.e_isSymm {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : IsSymm (e n)

Elementary symmetric polynomials are symmetric. Label: def.sf.ehp

Complete Homogeneous Symmetric Polynomials (Definition def.sf.ehp (b))

h_n = sum of all monomials of degree n = ∑{i₁ ≤ i₂ ≤ ... ≤ i_n} x{i₁} x_{i₂} ⋯ x_{i_n}

In Mathlib, this is MvPolynomial.hsymm (Fin N) K n.

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.SymmetricPolynomials.h {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) : P K N

The n-th complete homogeneous symmetric polynomial. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.h n = MvPolynomial.hsymm (Fin N) K n

theorem AlgebraicCombinatorics.SymmetricPolynomials.h_isSymm {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) : IsSymm (h n)

Complete homogeneous symmetric polynomials are symmetric. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.h_zero {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] : h 0 = 1

h_0 = 1 (Example exa.sf.ehp.1 (e)). Label: exa.sf.ehp.1

theorem AlgebraicCombinatorics.SymmetricPolynomials.h_one {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] : h 1 = ∑ i : Fin N, MvPolynomial.X i

h_1 = ∑ x_i (Example exa.sf.ehp.1 (d)). Label: exa.sf.ehp.1

Power Sums (Definition def.sf.ehp (c))

p_n = x₁^n + x₂^n + ... + x_N^n (for n > 0) p_0 = 1 p_n = 0 (for n < 0)

In Mathlib, this is MvPolynomial.psum (Fin N) K n. Note: Mathlib's definition has p_0 = N (the number of variables), not 1.

@[reducible, inline]

noncomputable abbrev AlgebraicCombinatorics.SymmetricPolynomials.p {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : P K N

The n-th power sum symmetric polynomial. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.p n = MvPolynomial.psum (Fin N) K n

theorem AlgebraicCombinatorics.SymmetricPolynomials.p_isSymm {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : IsSymm (p n)

Power sums are symmetric. Label: def.sf.ehp

Basic Values (Example exa.sf.ehp.1)

(d) e_1 = h_1 = p_1 = x_1 + x_2 + ... + x_N (e) e_0 = h_0 = 1, p_0 = N (f) e_n = h_n = p_n = 0 for n < 0 (vacuously true for ℕ)

theorem AlgebraicCombinatorics.SymmetricPolynomials.e_zero {K : Type u_1} [CommRing K] {N : ℕ} : e 0 = 1

e_0 = 1 (Example exa.sf.ehp.1 (e)). Label: exa.sf.ehp.1

theorem AlgebraicCombinatorics.SymmetricPolynomials.p_zero {K : Type u_1} [CommRing K] {N : ℕ} : p 0 = ↑(Fintype.card (Fin N))

p_0 = N (number of variables). Note: The source defines p_0 = 1, but Mathlib defines p_0 = N. Label: exa.sf.ehp.1

theorem AlgebraicCombinatorics.SymmetricPolynomials.e_one {K : Type u_1} [CommRing K] {N : ℕ} : e 1 = ∑ i : Fin N, MvPolynomial.X i

e_1 = ∑ x_i (Example exa.sf.ehp.1 (d)). Label: exa.sf.ehp.1

theorem AlgebraicCombinatorics.SymmetricPolynomials.p_one {K : Type u_1} [CommRing K] {N : ℕ} : p 1 = ∑ i : Fin N, MvPolynomial.X i

p_1 = ∑ x_i (Example exa.sf.ehp.1 (d)). Label: exa.sf.ehp.1

Integer-indexed versions (Definition def.sf.ehp)

The source defines e_n, h_n, p_n for all integers n ∈ ℤ. For negative n, they are all 0. This section provides integer-indexed versions that match the textbook definitions exactly.

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.eZ {K : Type u_1} [CommRing K] {N : ℕ} (n : ℤ) : P K N

Integer-indexed elementary symmetric polynomial. For n ∈ ℤ: e_n = esymm n if n ≥ 0, e_n = 0 if n < 0. This matches Definition def.sf.ehp (a) in the source. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.eZ n = if 0 ≤ n then AlgebraicCombinatorics.SymmetricPolynomials.e n.toNat else 0

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.hZ {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℤ) : P K N

Integer-indexed complete homogeneous symmetric polynomial. For n ∈ ℤ: h_n = hsymm n if n ≥ 0, h_n = 0 if n < 0. This matches Definition def.sf.ehp (b) in the source. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.hZ n = if 0 ≤ n then AlgebraicCombinatorics.SymmetricPolynomials.h n.toNat else 0

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.pZ {K : Type u_1} [CommRing K] {N : ℕ} (n : ℤ) : P K N

Integer-indexed power sum (textbook convention). For n ∈ ℤ: p'_n = psum n if n > 0, p'_0 = 1, p'_n = 0 if n < 0. This matches Definition def.sf.ehp (c) in the source.

Note: Mathlib's psum has p_0 = N (number of variables), but the textbook defines p_0 = 1. We follow the textbook convention here. Label: def.sf.ehp

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.pZ n = if n > 0 then AlgebraicCombinatorics.SymmetricPolynomials.p n.toNat else if n = 0 then 1 else 0

theorem AlgebraicCombinatorics.SymmetricPolynomials.eZ_neg {K : Type u_1} [CommRing K] {N : ℕ} {n : ℤ} (hn : n < 0) : eZ n = 0

e_n = 0 for negative n (Definition def.sf.ehp (a)). Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.eZ_of_nonneg {K : Type u_1} [CommRing K] {N : ℕ} {n : ℤ} (hn : 0 ≤ n) : eZ n = e n.toNat

eZ agrees with e for non-negative integers. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.eZ_isSymmetric {K : Type u_1} [CommRing K] {N : ℕ} (n : ℤ) : MvPolynomial.IsSymmetric (eZ n)

eZ n is symmetric for all n ∈ ℤ. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.hZ_neg {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] {n : ℤ} (hn : n < 0) : hZ n = 0

h_n = 0 for negative n (Definition def.sf.ehp (b)). Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.hZ_of_nonneg {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] {n : ℤ} (hn : 0 ≤ n) : hZ n = h n.toNat

hZ agrees with h for non-negative integers. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.hZ_isSymmetric {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℤ) : MvPolynomial.IsSymmetric (hZ n)

hZ n is symmetric for all n ∈ ℤ. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.pZ_neg {K : Type u_1} [CommRing K] {N : ℕ} {n : ℤ} (hn : n < 0) : pZ n = 0

p'_n = 0 for negative n (Definition def.sf.ehp (c)). Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.pZ_zero {K : Type u_1} [CommRing K] {N : ℕ} : pZ 0 = 1

p'_0 = 1 (Definition def.sf.ehp (c)). Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.pZ_of_pos {K : Type u_1} [CommRing K] {N : ℕ} {n : ℤ} (hn : 0 < n) : pZ n = p n.toNat

pZ agrees with psum for positive integers. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.pZ_isSymmetric {K : Type u_1} [CommRing K] {N : ℕ} (n : ℤ) : MvPolynomial.IsSymmetric (pZ n)

pZ n is symmetric for all n ∈ ℤ. Label: def.sf.ehp

Alternative characterizations (Definition def.sf.ehp)

The defining formulas for e_n, h_n, p_n as sums over tuples.

theorem AlgebraicCombinatorics.SymmetricPolynomials.e_eq_sum_prod_subsets {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : e n = ∑ s ∈ Finset.powersetCard n Finset.univ, ∏ i ∈ s, MvPolynomial.X i

e_n is the sum over all n-element subsets of [N] of the product of variables. This is the defining formula in Definition def.sf.ehp (a): e_n = ∑{i₁ < i₂ < ... < i_n} x{i₁} x_{i₂} ⋯ x_{i_n} Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.h_eq_sum_prod_sym {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) : h n = ∑ s : Sym (Fin N) n, (Multiset.map MvPolynomial.X ↑s).prod

h_n is the sum over all symmetric n-tuples (multisets) of [N] of the product of variables. This is the defining formula in Definition def.sf.ehp (b): h_n = ∑{i₁ ≤ i₂ ≤ ... ≤ i_n} x{i₁} x_{i₂} ⋯ x_{i_n} Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.p_eq_sum_pow {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : p n = ∑ i : Fin N, MvPolynomial.X i ^ n

p_n is the sum of n-th powers of all variables. This is the defining formula in Definition def.sf.ehp (c): p_n = x₁^n + x₂^n + ... + x_N^n Label: def.sf.ehp

Proposition prop.sf.en=0: e_n = 0 for n > N

For n > N, there are no n distinct elements in [N], so e_n = 0.

theorem AlgebraicCombinatorics.SymmetricPolynomials.e_eq_zero_of_gt {K : Type u_1} [CommRing K] {N n : ℕ} (hn : N < n) : e n = 0

e_n = 0 for n > N (Proposition prop.sf.en=0). Label: prop.sf.en=0

Adding a Variable Recurrence

The elementary symmetric polynomial e_n(x₁,...,x_N,y) satisfies the recurrence: e_n(x₁,...,x_N,y) = e_n(x₁,...,x_N) + y * e_{n-1}(x₁,...,x_N)

This is fundamental for inductive proofs about symmetric polynomials.

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_succ_add_var' {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : MvPolynomial.esymm (Fin (N + 1)) K (n + 1) = (MvPolynomial.rename Fin.castSucc) (MvPolynomial.esymm (Fin N) K (n + 1)) + MvPolynomial.X (Fin.last N) * (MvPolynomial.rename Fin.castSucc) (MvPolynomial.esymm (Fin N) K n)

Adding a variable: e_{n+1}(x₁,...,x_N,y) = e_{n+1}(x₁,...,x_N) + y * e_n(x₁,...,x_N). This is the recurrence for computing elementary symmetric polynomials. Label: def.sf.ehp

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_succ_add_var {K : Type u_1} [CommRing K] {N : ℕ} (n : ℕ) : MvPolynomial.esymm (Fin (N + 1)) K n = (MvPolynomial.rename Fin.castSucc) (MvPolynomial.esymm (Fin N) K n) + if n = 0 then 0 else MvPolynomial.X (Fin.last N) * (MvPolynomial.rename Fin.castSucc) (MvPolynomial.esymm (Fin N) K (n - 1))

Adding a variable: e_n(x₁,...,x_N,y) = e_n(x₁,...,x_N) + y * e_{n-1}(x₁,...,x_N). This is the recurrence for computing elementary symmetric polynomials. For n = 0, the second term vanishes since e_{-1} = 0 by convention (but Nat subtraction gives e_0 instead, so we use a conditional). Label: def.sf.ehp

Newton-Girard Formulas (Theorem thm.sf.NG)

For any positive integer n: (eq.thm.sf.NG.eh) ∑{j=0}^n (-1)^j e_j h{n-j} = 0 (eq.thm.sf.NG.ep) ∑{j=1}^n (-1)^{j-1} e{n-j} p_j = n · e_n (eq.thm.sf.NG.hp) ∑{j=1}^n h{n-j} p_j = n · h_n

These are implemented in Mathlib as MvPolynomial.mul_esymm_eq_sum and related theorems.

theorem AlgebraicCombinatorics.SymmetricPolynomials.newtonGirard_esymm {K : Type u_1} [CommRing K] {N : ℕ} (k : ℕ) : ↑k * e k = (-1) ^ (k + 1) * ∑ a ∈ Finset.antidiagonal k with a.1 < k, (-1) ^ a.1 * e a.1 * p a.2

Newton-Girard formula: recurrence for elementary symmetric polynomials. k * e_k = (-1)^{k+1} * ∑{a ∈ antidiagonal k, a.1 < k} (-1)^{a.1} * e{a.1} * p_{a.2} (Theorem thm.sf.NG, equation eq.thm.sf.NG.ep). Label: thm.sf.NG

theorem AlgebraicCombinatorics.SymmetricPolynomials.newtonGirard_psum {K : Type u_1} [CommRing K] {N : ℕ} (k : ℕ) (hk : 0 < k) : p k = (-1) ^ (k + 1) * ↑k * e k - ∑ a ∈ Finset.antidiagonal k with a.1 ∈ Set.Ioo 0 k, (-1) ^ a.1 * e a.1 * p a.2

Newton-Girard formula: recurrence for power sums. p_k = (-1)^{k+1} * k * e_k - ∑{a ∈ antidiagonal k, 0 < a.1 < k} (-1)^{a.1} * e{a.1} * p_{a.2} (Theorem thm.sf.NG, equation eq.thm.sf.NG.ep). Label: thm.sf.NG

theorem AlgebraicCombinatorics.SymmetricPolynomials.geom_series_mul_one_sub {K : Type u_1} [CommRing K] {N : ℕ} (i : Fin N) : ((1 - PowerSeries.X * PowerSeries.C (MvPolynomial.X i)) * PowerSeries.mk fun (k : ℕ) => MvPolynomial.X i ^ k) = 1

Geometric series identity: (1 - t·x) * (∑_{k≥0} t^k x^k) = 1. This is the key lemma for the generating function proof of Newton-Girard.

theorem AlgebraicCombinatorics.SymmetricPolynomials.prod_geom_series_mul_prod_one_sub {K : Type u_1} [CommRing K] {N : ℕ} : ((∏ i : Fin N, (1 - PowerSeries.X * PowerSeries.C (MvPolynomial.X i))) * ∏ i : Fin N, PowerSeries.mk fun (k : ℕ) => MvPolynomial.X i ^ k) = 1

Product of geometric series equals 1 when multiplied by ∏(1 - t·x_i). This is the generating function identity E(t) * H(t) = 1.

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_genfunc {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] : ∏ i : Fin N, (1 - Polynomial.X * Polynomial.C (MvPolynomial.X i)) = ∑ n ∈ Finset.range (N + 1), (-1) ^ n * Polynomial.X ^ n * Polynomial.C (e n)

Generating function for elementary symmetric polynomials (Proposition prop.sf.e-h-FPS (a)). ∏{i=1}^N (1 - t·x_i) = ∑{n=0}^N (-1)^n t^n e_n This is placed here so it can be used in newtonGirard_eh. Label: prop.sf.e-h-FPS

theorem AlgebraicCombinatorics.SymmetricPolynomials.newtonGirard_eh {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) (hn : 0 < n) : ∑ j ∈ Finset.range (n + 1), (-1) ^ j * e j * h (n - j) = 0

Newton-Girard formula relating e and h: ∑{j=0}^n (-1)^j e_j h{n-j} = 0 for n > 0. (Theorem thm.sf.NG, equation eq.thm.sf.NG.eh).

The proof uses the generating function identity: E(t) * H(t) = 1, where E(t) = ∏_i (1 - t·x_i) and H(t) = ∑_n t^n h_n.

Since E(t) = ∑n (-1)^n t^n e_n, the coefficient of t^n in E(t) * H(t) is: ∑{j=0}^n (-1)^j e_j h_{n-j}

For n > 0, this coefficient must be 0 (since E(t) * H(t) = 1).

Label: thm.sf.NG

theorem AlgebraicCombinatorics.SymmetricPolynomials.sum_count_eq_card {N : ℕ} [DecidableEq (Fin N)] (m : ℕ) (s : Sym (Fin N) m) : ∑ i : Fin N, Multiset.count i ↑s = m

Key lemma: For any multiset s of size m, the sum of counts over all elements equals m. This is used in the proof of the Newton-Girard formula for h and p. Label: thm.sf.NG

Helper lemmas for the bijection in Newton-Girard hp formula

theorem AlgebraicCombinatorics.SymmetricPolynomials.newtonGirard_hp {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) (_hn : 0 < n) : ∑ j ∈ Finset.range n, h (n - 1 - j) * p (j + 1) = ↑n * h n

Newton-Girard formula relating h and p: ∑{j=1}^n h{n-j} p_j = n · h_n. (Theorem thm.sf.NG, equation eq.thm.sf.NG.hp).

Proof strategy: The proof is by a counting argument on monomials. Each monomial in h_n corresponds to a multiset s : Sym (Fin N) n.

On the LHS, each such monomial appears exactly n times: once for each way to decompose s = t + replicate (j+1) i where j ∈ {0, ..., n-1}, t : Sym (n-1-j), and i : Fin N.

The key bijection is:

• LHS: { (j, t, i) | j < n, t : Sym (n-1-j), i : Fin N }
• RHS: { (s, i, k) | s : Sym n, i : Fin N, k < count i s } where (j, t, i) ↦ (t.1 + replicate (j+1) i, i, j).

For each s : Sym n, the monomial (s.1.map X).prod appears:

• On LHS: #{(j, t, i) | t.1 + replicate (j+1) i = s.1} = ∑_i count(i,s) = n times
• On RHS: with coefficient ∑_i count(i,s) = n

Label: thm.sf.NG

Generating Function Identities (Proposition prop.sf.e-h-FPS)

These identities express the elementary and complete homogeneous symmetric polynomials as coefficients in certain generating functions.

(a) In P[t]: ∏{i=1}^N (1 - t·x_i) = ∑{n≥0} (-1)^n t^n e_n (b) In P[u,v]: ∏{i=1}^N (u - v·x_i) = ∑{n=0}^N (-1)^n u^{N-n} v^n e_n (c) In P[[t]]: ∏{i=1}^N 1/(1 - t·x_i) = ∑{n≥0} t^n h_n

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_genfunc_two_var {K : Type u_1} [CommRing K] {N : ℕ} : ∏ i : Fin N, (MvPolynomial.X 0 - MvPolynomial.X 1 * MvPolynomial.C (MvPolynomial.X i)) = ∑ n ∈ Finset.range (N + 1), (-1) ^ n * MvPolynomial.X 0 ^ (N - n) * MvPolynomial.X 1 ^ n * MvPolynomial.C (e n)

Generating function for elementary symmetric polynomials, two-variable version (Proposition prop.sf.e-h-FPS (b)). ∏{i=1}^N (u - v·x_i) = ∑{n=0}^N (-1)^n u^{N-n} v^n e_n Label: prop.sf.e-h-FPS

theorem AlgebraicCombinatorics.SymmetricPolynomials.hsymm_genfunc {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] : have E := ∏ i : Fin N, (1 - Polynomial.X * Polynomial.C (MvPolynomial.X i)); (PowerSeries.mk fun (n : ℕ) => h n) * ↑E = 1

Generating function for complete homogeneous symmetric polynomials (Proposition prop.sf.e-h-FPS (c)). In the ring of formal power series, ∏{i=1}^N 1/(1 - t·x_i) = ∑{n≥0} t^n h_n. We state this as: (∑ t^n h_n) * ∏(1 - t·x_i) = 1. Label: prop.sf.e-h-FPS

Fundamental Theorem of Symmetric Polynomials (Theorem thm.sf.ftsf)

(a) e_1, e_2, ..., e_N are algebraically independent and generate S. (b) h_1, h_2, ..., h_N are algebraically independent and generate S. (c) If K is a ℚ-algebra, then p_1, p_2, ..., p_N are algebraically independent and generate S.

These are implemented in Mathlib via MvPolynomial.esymmAlgEquiv.

Part (a): Elementary Symmetric Polynomials

The elementary symmetric polynomials e_1, e_2, ..., e_N are algebraically independent over K and generate the K-algebra S of symmetric polynomials. This means:

1. The only polynomial relation P(e_1, ..., e_N) = 0 is P = 0 (algebraic independence)
2. Every symmetric polynomial can be written uniquely as a polynomial in e_1, ..., e_N (generation)

Equivalently, the map K[y_1, ..., y_N] → S given by g ↦ g(e_1, ..., e_N) is a K-algebra isomorphism.

noncomputable def AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgEquiv' {K : Type u_1} [CommRing K] {N : ℕ} : MvPolynomial (Fin N) K ≃ₐ[K] ↥(S K N)

The elementary symmetric polynomials e_1, ..., e_N generate the symmetric subalgebra and the map g ↦ g[e_1, ..., e_N] is a K-algebra isomorphism. (Theorem thm.sf.ftsf (a)). Label: thm.sf.ftsf

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgEquiv' = MvPolynomial.esymmAlgEquiv (Fin N) K ⋯

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgHom_injective' {K : Type u_1} [CommRing K] {N : ℕ} : Function.Injective ⇑(MvPolynomial.esymmAlgHom (Fin N) K N)

The map sending g to g[e_1, ..., e_N] is injective. This is equivalent to saying the elementary symmetric polynomials are algebraically independent. Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgHom_surjective' {K : Type u_1} [CommRing K] {N : ℕ} : Function.Surjective ⇑(MvPolynomial.esymmAlgHom (Fin N) K N)

The map sending g to g[e_1, ..., e_N] is surjective. This is equivalent to saying the elementary symmetric polynomials generate S. Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgEquiv'_eq_esymmAlgHom {K : Type u_1} [CommRing K] {N : ℕ} (g : MvPolynomial (Fin N) K) : esymmAlgEquiv' g = (MvPolynomial.esymmAlgHom (Fin N) K N) g

The esymmAlgEquiv' equals esymmAlgHom as a function. Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymmAlgHom_eq_aeval {K : Type u_1} [CommRing K] {N : ℕ} (r : MvPolynomial (Fin N) K) : ↑((MvPolynomial.esymmAlgHom (Fin N) K N) r) = (MvPolynomial.aeval fun (i : Fin N) => MvPolynomial.esymm (Fin N) K (↑i + 1)) r

The key lemma: esymmAlgHom is aeval composed with the inclusion. Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_algebraicIndependent {K : Type u_1} [CommRing K] {N : ℕ} : AlgebraicIndependent K fun (i : Fin N) => MvPolynomial.esymm (Fin N) K (↑i + 1)

The elementary symmetric polynomials e_1, ..., e_N are algebraically independent. This means: if P(e_1, ..., e_N) = 0 for some polynomial P ∈ K[y_1, ..., y_N], then P = 0. (Theorem thm.sf.ftsf (a), algebraic independence part). Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.esymm_generates_symmetric {K : Type u_1} [CommRing K] {N : ℕ} (f : ↥(S K N)) : ∃! g : MvPolynomial (Fin N) K, (MvPolynomial.esymmAlgHom (Fin N) K N) g = f

Every symmetric polynomial can be uniquely written as a polynomial in e_1, ..., e_N. (Theorem thm.sf.ftsf (a), generation part). Label: thm.sf.ftsf

Part (b): Complete Homogeneous Symmetric Polynomials

The complete homogeneous symmetric polynomials h_1, h_2, ..., h_N are also algebraically independent and generate S. This is a consequence of the Newton-Girard relations which express each h_k as a polynomial in e_1, ..., e_k and vice versa.

theorem AlgebraicCombinatorics.SymmetricPolynomials.hsymm_algebraicIndependent {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] [IsDomain K] : AlgebraicIndependent K fun (i : Fin N) => MvPolynomial.hsymm (Fin N) K (↑i + 1)

The complete homogeneous symmetric polynomials h_1, ..., h_N are algebraically independent. (Theorem thm.sf.ftsf (b), algebraic independence part).

The proof uses the Newton-Girard relations to show that the map sending polynomials to their evaluation at h_1, ..., h_N factors through the symmetric subalgebra S, and this factored map is bijective.

Key steps:

1. The map aeval hsymm lands in S K N (since hsymm is symmetric)
2. Factor aeval hsymm as: MvPolynomial → S K N → P K N
3. The composition esymmAlgEquiv'.symm ∘ (factored map) : MvPolynomial → MvPolynomial is surjective (because X_i = esymmAlgEquiv'.symm (esymm (i+1)) and esymm is in the range by Newton-Girard)
4. A surjective algebra endomorphism of K[X_1, ..., X_n] is bijective
5. Therefore the factored map is bijective, hence aeval hsymm is injective

Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.hsymm_generates_symmetric {K : Type u_1} [CommRing K] {N : ℕ} [DecidableEq (Fin N)] [IsDomain K] (f : ↥(S K N)) : ∃! g : MvPolynomial (Fin N) K, (MvPolynomial.aeval fun (i : Fin N) => MvPolynomial.hsymm (Fin N) K (↑i + 1)) g = ↑f

Every symmetric polynomial can be uniquely written as a polynomial in h_1, ..., h_N. (Theorem thm.sf.ftsf (b), generation part). Label: thm.sf.ftsf

Part (c): Power Sums (over ℚ-algebras)

When K is a ℚ-algebra (e.g., K = ℚ, ℝ, ℂ, or any field of characteristic 0), the power sums p_1, p_2, ..., p_N are also algebraically independent and generate S.

Note: This fails in positive characteristic. For example, over 𝔽_p, we have p_p = x_1^p + ... + x_N^p = (x_1 + ... + x_N)^p = p_1^p by the Frobenius endomorphism.

Weight argument infrastructure for power sum algebraic independence

The key insight for proving the triangular structure of ψ(X_i) is a weight argument:

• Define weight(X_k) = k+1 for variables X_k in MvPolynomial (Fin N) K
• The map psumAeval' sends X_k to psum(k+1), which is homogeneous of degree k+1
• Therefore psumAeval' maps polynomials of weighted degree w to polynomials of total degree w
• Since esymm(i+1) has total degree i+1, any polynomial P with psumAeval'(P) = esymm(i+1) must have all monomials with weighted degree i+1
• This constrains which variables can appear in P with which exponents

theorem AlgebraicCombinatorics.SymmetricPolynomials.psum_algebraicIndependent {K : Type u_1} [CommRing K] {N : ℕ} [Algebra ℚ K] [IsDomain K] : AlgebraicIndependent K fun (i : Fin N) => MvPolynomial.psum (Fin N) K (↑i + 1)

The power sums p_1, ..., p_N are algebraically independent over a ℚ-algebra. (Theorem thm.sf.ftsf (c), algebraic independence part).

The proof follows the same strategy as for hsymm_algebraicIndependent:

1. The map aeval psum lands in S K N (since psum is symmetric)
2. Factor aeval psum as: MvPolynomial → S K N → P K N
3. The composition esymmAlgEquiv'.symm ∘ (factored map) : MvPolynomial → MvPolynomial is surjective (because X_i = esymmAlgEquiv'.symm (esymm (i+1)) and esymm is in the range by Newton's identities)
4. A surjective algebra endomorphism of K[X_1, ..., X_n] is bijective (transcendence degree argument)
5. Therefore the factored map is bijective, hence aeval psum is injective

Label: thm.sf.ftsf

theorem AlgebraicCombinatorics.SymmetricPolynomials.psum_generates_symmetric {K : Type u_1} [CommRing K] {N : ℕ} [Algebra ℚ K] [IsDomain K] (f : ↥(S K N)) : ∃! g : MvPolynomial (Fin N) K, (MvPolynomial.aeval fun (i : Fin N) => MvPolynomial.psum (Fin N) K (↑i + 1)) g = ↑f

Over a ℚ-algebra, every symmetric polynomial can be uniquely written as a polynomial in p_1, ..., p_N. (Theorem thm.sf.ftsf (c), generation part). Label: thm.sf.ftsf

Lemma lem.sf.simples-enough: Simple transpositions suffice

A polynomial f ∈ P is symmetric if and only if s_k · f = f for each k ∈ [N-1], where s_k is the simple transposition swapping k and k+1.

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricPolynomials.simpleTransposition {N : ℕ} (k : Fin (N - 1)) : Equiv.Perm (Fin N)

Simple transposition s_k swaps positions k and k+1.

This is an alias for the canonical definition AlgebraicCombinatorics.simpleTransposition from Permutations/Basics.lean. The canonical definition uses Fin (N - 1) to encode the constraint that k + 1 < N.

Label: lem.sf.simples-enough

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.simpleTransposition k = AlgebraicCombinatorics.simpleTransposition k

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_iff_simpleTranspositions {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : IsSymm f ↔ ∀ (k : Fin (N - 1)), permAction (simpleTransposition k) f = f

A polynomial is symmetric iff it is invariant under all simple transpositions. (Lemma lem.sf.simples-enough). Label: lem.sf.simples-enough

Example: Antisymmetric Polynomials

A polynomial f is antisymmetric if σ · f = (-1)^σ · f for all σ ∈ S_N. The square of an antisymmetric polynomial is symmetric.

def AlgebraicCombinatorics.SymmetricPolynomials.IsAntisymm {K : Type u_1} [CommRing K] {N : ℕ} (f : P K N) : Prop

A polynomial is antisymmetric if σ · f = sign(σ) · f for all permutations σ. Label: exa.sf.PS1

Equations

• AlgebraicCombinatorics.SymmetricPolynomials.IsAntisymm f = ∀ (σ : Equiv.Perm (Fin N)), (MvPolynomial.rename ⇑σ) f = Equiv.Perm.sign σ • f

Basic API lemmas for IsAntisymm

The following lemmas establish that antisymmetric polynomials form a K-submodule of P (but not a subalgebra, since the product of two antisymmetric polynomials is symmetric, not antisymmetric).

theorem AlgebraicCombinatorics.SymmetricPolynomials.isAntisymm_zero {K : Type u_1} [CommRing K] {N : ℕ} : IsAntisymm 0

The zero polynomial is antisymmetric. Label: exa.sf.PS1

theorem AlgebraicCombinatorics.SymmetricPolynomials.isAntisymm_neg {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : IsAntisymm f) : IsAntisymm (-f)

If f is antisymmetric, then -f is antisymmetric. Label: exa.sf.PS1

theorem AlgebraicCombinatorics.SymmetricPolynomials.isAntisymm_smul {K : Type u_1} [CommRing K] {N : ℕ} (c : K) {f : P K N} (hf : IsAntisymm f) : IsAntisymm (c • f)

If f is antisymmetric, then c • f is antisymmetric for any scalar c. Label: exa.sf.PS1

theorem AlgebraicCombinatorics.SymmetricPolynomials.isAntisymm_add {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : IsAntisymm f) (hg : IsAntisymm g) : IsAntisymm (f + g)

If f and g are antisymmetric, then f + g is antisymmetric. Label: exa.sf.PS1

theorem AlgebraicCombinatorics.SymmetricPolynomials.isAntisymm_sub {K : Type u_1} [CommRing K] {N : ℕ} {f g : P K N} (hf : IsAntisymm f) (hg : IsAntisymm g) : IsAntisymm (f - g)

If f and g are antisymmetric, then f - g is antisymmetric. Label: exa.sf.PS1

theorem AlgebraicCombinatorics.SymmetricPolynomials.isSymm_sq_of_isAntisymm {K : Type u_1} [CommRing K] {N : ℕ} {f : P K N} (hf : IsAntisymm f) : IsSymm (f ^ 2)

The square of an antisymmetric polynomial is symmetric. (Example exa.sf.PS1 (d)). Label: exa.sf.PS1