The elementary symmetric functions of a geometric progression

The Gaussian binomial coefficient [n k]_X (by the q-Pascal rule) and the identity e_k(1, X, …, X^{n−1}) = X^{k(k−1)/2} [n k]_X (Lemma 2.1 of «A segment of the character ring»): induction on n, splitting {1, X, …, X^n} = {1} ∪ X·{1, …, X^{n−1}} and using e_{k+1}(a, s) = e_{k+1}(s) + a e_k(s) and e_k(c·s) = c^k e_k(s).

Main definitions

• GaussBinom.gaussBinom: the Gaussian binomial coefficient in ℤ[X].

Main results

• GaussBinom.esymm_geometric: the identity above.
• GaussBinom.esymm_cons_succ, GaussBinom.esymm_map_mul: the two rules for Multiset.esymm.

References

• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847477, Lemma lem:gauss.

noncomputable def GaussBinom.gaussBinom : ℕ → ℕ → Polynomial ℤ

The Gaussian binomial coefficient [n k]_X, by the q-Pascal rule [n+1, k+1] = [n, k] + X^{k+1} [n, k+1].

Equations

• GaussBinom.gaussBinom x✝ 0 = 1
• GaussBinom.gaussBinom 0 n.succ = 0
• GaussBinom.gaussBinom n.succ k.succ = GaussBinom.gaussBinom n k + Polynomial.X ^ (k + 1) * GaussBinom.gaussBinom n (k + 1)

theorem GaussBinom.range_succ_map_pow (n : ℕ) : Multiset.map (fun (i : ℕ) => Polynomial.X ^ i) (Multiset.range (n + 1)) = 1 ::ₘ Multiset.map (fun (i : ℕ) => Polynomial.X * Polynomial.X ^ i) (Multiset.range n)

theorem GaussBinom.esymm_cons_succ (a : Polynomial ℤ) (s : Multiset (Polynomial ℤ)) (k : ℕ) : (a ::ₘ s).esymm (k + 1) = s.esymm (k + 1) + a * s.esymm k

theorem GaussBinom.esymm_map_mul (c : Polynomial ℤ) (s : Multiset (Polynomial ℤ)) (k : ℕ) : (Multiset.map (fun (x : Polynomial ℤ) => c * x) s).esymm k = c ^ k * s.esymm k

theorem GaussBinom.tri_succ (k : ℕ) : k + k * (k - 1) / 2 = (k + 1) * k / 2

theorem GaussBinom.esymm_range_zero (k : ℕ) : (Multiset.map (fun (i : ℕ) => Polynomial.X ^ i) (Multiset.range 0)).esymm k = Polynomial.X ^ (k * (k - 1) / 2) * gaussBinom 0 k

theorem GaussBinom.esymm_geometric (n k : ℕ) : (Multiset.map (fun (i : ℕ) => Polynomial.X ^ i) (Multiset.range n)).esymm k = Polynomial.X ^ (k * (k - 1) / 2) * gaussBinom n k

Lemma 2.1 of character-ring-segment: the k-th elementary symmetric function of 1, X, …, X^{n−1} is X^{k(k−1)/2} [n k]_X.