The Fundamental Theorem of Symmetric Polynomials

In a polynomial ring in n variables over a commutative ring, the subalgebra of symmetric polynomials is freely generated by the first n elementary symmetric polynomials (excluding the 0th, which is simply 1). This is expressed as an isomorphism MvPolynomial.esymmAlgEquiv between MvPolynomial (Fin n) R and the symmetric subalgebra of any polynomial ring MvPolynomial σ R with #σ = n. The forward map is called MvPolynomial.esymmAlgHom.

Proof strategy

We follow the alternative proof on the Wikipedia page https://en.wikipedia.org/wiki/Elementary_symmetric_polynomial#Alternative_proof It suffices to show esymmAlgHom is both injective and surjective.

Endow the Fintype σ with a linear order and endow the (monic) monomials in the polynomial ring MvPolynomial σ R with the lexicographic order on σ →₀ ℕ, which is a well order. Then any nonzero polynomial p : MvPolynomial σ R has a largest nonzero monomial (AddMonoidAlgebra.supDegree toLex p) and the corresponding coefficient is AddMonoidAlgebra.leadingCoeff toLex p. If p is symmetric, any permutation of a nonzero monomial in p must also be a nonzero monomial in p, so the largest nonzero monomial must be antitone as a function σ → ℕ (MvPolynomial.IsSymmetric.antitone_supDegree). We can then construct a monomial in MvPolynomial (Fin n) R whose image under esymmAlgHom has the same supDegree and leadingCoeff as p: MvPolynomial.supDegree_esymmAlgHomMonomial says that the supDegree of the image is given by Fin.accumulate, and Fin.accumulate_invAccumulate says that Fin.invAccumulate is inverse to Fin.accumulate for antitone monomials. If we subtract the image from p, we are left with a symmetric polynomial of lower supDegree, which we may assume to be in the image by induction, thanks to the well-orderedness of Lex (σ →₀ ℕ); the surjectivity of esymmAlgHom follows. For injectivity, just notice that the images of different monic monomials in MvPolynomial (Fin n) R have different supDegree (Fin.accumulate_injective), so if there is at least one nonzero monomial, the images cannot all cancel out (AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree).

We actually only define Fin.accumulate in the case σ := Fin m rather than an arbitrary Fintype with a linear order; we show that esymmAlgHom is in fact surjective whenever m ≤ n and injective whenever n ≤ m, and then transfer the results to any Fintype σ. See MvPolynomial.injective_esymmAlgHom and MvPolynomial.esymmAlgHom_surjective.

def Fin.accumulate (n m : ℕ) : (Fin n → ℕ) →+ Fin m → ℕ

The jth entry of accumulate n m t is the sum of t i over all i ≥ j.

Equations

• Fin.accumulate n m = { toFun := fun (t : Fin n → ℕ) (j : Fin m) => ∑ i : Fin n with ↑j ≤ ↑i, t i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Fin.accumulate_apply (n m : ℕ) (t : Fin n → ℕ) (j : Fin m) : (accumulate n m) t j = ∑ i : Fin n with ↑j ≤ ↑i, t i

def Fin.invAccumulate (n m : ℕ) (s : Fin m → ℕ) (i : Fin n) : ℕ

The ith entry of invAccumulate n m s is s i - s (i+1), where s j = 0 if j ≥ m.

Equations

• Fin.invAccumulate n m s i = (if hi : ↑i < m then s ⟨↑i, hi⟩ else 0) - if hi : ↑i + 1 < m then s ⟨↑i + 1, hi⟩ else 0

theorem Fin.accumulate_rec {i n m : ℕ} (hin : i < n) (him : i + 1 < m) (t : Fin n → ℕ) : (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (accumulate n m) t ⟨i + 1, him⟩

theorem Fin.accumulate_last {i n m : ℕ} (hin : i < n) (hmi : m = i + 1) (t : Fin n → ℕ) (ht : ∀ (j : Fin n), m ≤ ↑j → t j = 0) : (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩

theorem Fin.accumulate_injective {n m : ℕ} (hnm : n ≤ m) : Function.Injective ⇑(accumulate n m)

theorem Fin.accumulate_invAccumulate {n m : ℕ} (hmn : m ≤ n) {s : Fin m → ℕ} (hs : Antitone s) : (accumulate n m) (invAccumulate n m s) = s

noncomputable def MvPolynomial.esymmAlgHom (σ : Type u_1) (R : Type u_3) (n : ℕ) [CommSemiring R] [Fintype σ] : MvPolynomial (Fin n) R →ₐ[R] ↥(symmetricSubalgebra σ R)

The R-algebra homomorphism from $R[x_1,\dots,x_n]$ to the symmetric subalgebra of $R[\{x_i \mid i ∈ σ\}]$ sending $x_i$ to the $i$-th elementary symmetric polynomial.

Equations

• MvPolynomial.esymmAlgHom σ R n = MvPolynomial.aeval fun (i : Fin n) => ⟨MvPolynomial.esymm σ R (↑i + 1), ⋯⟩

theorem MvPolynomial.esymmAlgHom_apply {σ : Type u_1} {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] (p : MvPolynomial (Fin n) R) : ↑((esymmAlgHom σ R n) p) = (aeval fun (i : Fin n) => esymm σ R (↑i + 1)) p

theorem MvPolynomial.rename_esymmAlgHom {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] [Fintype τ] (e : σ ≃ τ) : (↑(renameSymmetricSubalgebra e)).comp (esymmAlgHom σ R n) = esymmAlgHom τ R n

noncomputable def MvPolynomial.esymmAlgHomMonomial (σ : Type u_1) {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] (t : Fin n →₀ ℕ) (r : R) : MvPolynomial σ R

The image of a monomial under esymmAlgHom.

Equations

• MvPolynomial.esymmAlgHomMonomial σ t r = ↑((MvPolynomial.esymmAlgHom σ R n) ((MvPolynomial.monomial t) r))

theorem MvPolynomial.isSymmetric_esymmAlgHomMonomial {σ : Type u_1} {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] (t : Fin n →₀ ℕ) (r : R) : (esymmAlgHomMonomial σ t r).IsSymmetric

theorem MvPolynomial.esymmAlgHomMonomial_single {σ : Type u_1} {R : Type u_3} {n k : ℕ} [CommSemiring R] [Fintype σ] {i : Fin n} {r : R} : esymmAlgHomMonomial σ (fun₀ | i => k) r = C r * esymm σ R (↑i + 1) ^ k

theorem MvPolynomial.esymmAlgHomMonomial_single_one {σ : Type u_1} {R : Type u_3} {n k : ℕ} [CommSemiring R] [Fintype σ] {i : Fin n} : esymmAlgHomMonomial σ (fun₀ | i => k) 1 = esymm σ R (↑i + 1) ^ k

theorem MvPolynomial.esymmAlgHomMonomial_add {σ : Type u_1} {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] {r : R} {t s : Fin n →₀ ℕ} : esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1

theorem MvPolynomial.esymmAlgHom_zero {σ : Type u_1} {R : Type u_3} {n : ℕ} [CommSemiring R] [Fintype σ] {r : R} : esymmAlgHomMonomial σ 0 r = C r

theorem MvPolynomial.supDegree_esymm {R : Type u_3} {n m : ℕ} [CommSemiring R] {i : Fin n} [Nontrivial R] (him : ↑i < m) : ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) (esymm (Fin m) R (↑i + 1)))) = (Fin.accumulate n m) ⇑fun₀ | i => 1

theorem MvPolynomial.monic_esymm {R : Type u_3} {m : ℕ} [CommSemiring R] {i : ℕ} (him : i ≤ m) : AddMonoidAlgebra.Monic (⇑toLex) (esymm (Fin m) R i)

theorem MvPolynomial.leadingCoeff_esymmAlgHomMonomial {R : Type u_3} {n m : ℕ} [CommSemiring R] {r : R} (t : Fin n →₀ ℕ) (hnm : n ≤ m) : AddMonoidAlgebra.leadingCoeff (⇑toLex) (esymmAlgHomMonomial (Fin m) t r) = r

theorem MvPolynomial.supDegree_esymmAlgHomMonomial {R : Type u_3} {n m : ℕ} [CommSemiring R] {r : R} (hr : r ≠ 0) (t : Fin n →₀ ℕ) (hnm : n ≤ m) : ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) (esymmAlgHomMonomial (Fin m) t r))) = (Fin.accumulate n m) ⇑t

theorem MvPolynomial.IsSymmetric.antitone_supDegree {σ : Type u_1} {R : Type u_3} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.IsSymmetric) : Antitone ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p))

theorem MvPolynomial.esymmAlgHom_fin_injective (R : Type u_3) {n m : ℕ} [CommRing R] (h : n ≤ m) : Function.Injective ⇑(esymmAlgHom (Fin m) R n)

theorem MvPolynomial.esymmAlgHom_injective {σ : Type u_1} (R : Type u_3) {n : ℕ} [Fintype σ] [CommRing R] (hn : n ≤ Fintype.card σ) : Function.Injective ⇑(esymmAlgHom σ R n)

theorem MvPolynomial.esymmAlgHom_fin_bijective (R : Type u_3) [CommRing R] (n : ℕ) : Function.Bijective ⇑(esymmAlgHom (Fin n) R n)

theorem MvPolynomial.esymmAlgHom_fin_surjective (R : Type u_3) {n m : ℕ} [CommRing R] (h : m ≤ n) : Function.Surjective ⇑(esymmAlgHom (Fin m) R n)

theorem MvPolynomial.esymmAlgHom_surjective {σ : Type u_1} (R : Type u_3) {n : ℕ} [Fintype σ] [CommRing R] (hn : Fintype.card σ ≤ n) : Function.Surjective ⇑(esymmAlgHom σ R n)

noncomputable def MvPolynomial.esymmAlgEquiv {σ : Type u_1} (R : Type u_3) {n : ℕ} [Fintype σ] [CommRing R] (hn : Fintype.card σ = n) : MvPolynomial (Fin n) R ≃ₐ[R] ↥(symmetricSubalgebra σ R)

If the cardinality of σ is n, then esymmAlgHom σ R n is an isomorphism.

Equations

• MvPolynomial.esymmAlgEquiv R hn = AlgEquiv.ofBijective (MvPolynomial.esymmAlgHom σ R n) ⋯

@[simp]

theorem MvPolynomial.esymmAlgEquiv_apply {σ : Type u_1} (R : Type u_3) {n : ℕ} [Fintype σ] [CommRing R] (hn : Fintype.card σ = n) (a : MvPolynomial (Fin n) R) : (esymmAlgEquiv R hn) a = (esymmAlgHom σ R n) a