The h--e convolution and the Toeplitz inverse

The complete homogeneous symmetric polynomials h_n and the elementary symmetric polynomials e_n are related by the generating-function identity

(∑ₙ hₙ tⁿ) · (∑ₙ (-1)ⁿ eₙ tⁿ) = 1,

whose coefficient form is the convolution

∑_{r + s = m} h_r · (-1)ˢ e_s = δ_{m0}.

This is the Toeplitz-inverse identity behind the dual (transpose) Jacobi--Trudi formula: the matrix (h_{j - i}) and the matrix ((-1)^{j - i} e_{j - i}) are inverse to each other, so the s_μ minor of the first is complementary to the s_{μᵀ} minor of the second. Both matrices are upper unitriangular, hence have determinant 1, so the Schur-complement inversion is exact.

Determinantal formulas index h and e by integers, with h_m = e_m = 0 for m < 0; TauCeti.hsymmInt and TauCeti.esymmInt are these integer-indexed polynomials.

Main results

• TauCeti.mk_hsymm_mul_mk_neg_one_pow_mul_esymm_eq_one: the generating functions of h and signed e are inverse.
• TauCeti.sum_antidiagonal_hsymm_mul_neg_one_pow_mul_esymm: the convolution ∑_{r + s = m} h_r · (-1)ˢ e_s = δ_{m0}.
• TauCeti.sum_Icc_hsymmInt_mul_neg_one_pow_mul_esymmInt: its integer-indexed form, summed over [i, j].
• TauCeti.hsymmToeplitz, TauCeti.esymmToeplitz: the Toeplitz matrices (h_{j - i}) and ((-1)^{j - i} e_{j - i}).
• TauCeti.hsymmToeplitz_mul_esymmToeplitz: they are inverse to each other.
• TauCeti.det_hsymmToeplitz, TauCeti.det_esymmToeplitz: both matrices are upper unitriangular, so both have determinant 1.
• TauCeti.esymmToeplitz_apply_eq_neg_one_pow_mul: the sign of an entry of the signed e Toeplitz matrix splits as a row factor times a column factor.
• TauCeti.det_submatrix_esymmToeplitz: consequently a minor of the signed e Toeplitz matrix is a product of signs times the corresponding minor of TauCeti.esymmInt.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, (2.6'), (2.9), and (3.5).
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, §7.6.

theorem TauCeti.mk_hsymm_mul_mk_neg_one_pow_mul_esymm_eq_one {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] : ((PowerSeries.mk fun (n : ℕ) => MvPolynomial.hsymm σ R n) * PowerSeries.mk fun (n : ℕ) => (-1) ^ n * MvPolynomial.esymm σ R n) = 1

The h--e generating functions are inverse: (∑ₙ hₙ tⁿ) · (∑ₙ (-1)ⁿ eₙ tⁿ) = 1.

theorem TauCeti.sum_antidiagonal_hsymm_mul_neg_one_pow_mul_esymm {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] (m : ℕ) : ∑ p ∈ Finset.antidiagonal m, MvPolynomial.hsymm σ R p.1 * ((-1) ^ p.2 * MvPolynomial.esymm σ R p.2) = if m = 0 then 1 else 0

The h--e convolution: ∑_{r + s = m} hᵣ · (-1)ˢ eₛ = δ_{m0}, the coefficient form of TauCeti.mk_hsymm_mul_mk_neg_one_pow_mul_esymm_eq_one.

theorem TauCeti.sum_range_hsymm_mul_neg_one_pow_mul_esymm {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] (m : ℕ) : ∑ r ∈ Finset.range (m + 1), MvPolynomial.hsymm σ R r * ((-1) ^ (m - r) * MvPolynomial.esymm σ R (m - r)) = if m = 0 then 1 else 0

The h--e convolution summed over range (m + 1) rather than over an antidiagonal.

theorem TauCeti.sum_Icc_hsymmInt_mul_neg_one_pow_mul_esymmInt {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] {i j : ℕ} : ∑ k ∈ Finset.Icc i j, hsymmInt σ R (↑k - ↑i) * ((-1) ^ (↑j - ↑k).toNat * esymmInt σ R (↑j - ↑k)) = if i = j then 1 else 0

The integer-indexed h--e convolution: ∑_{k = i}^{j} h_{k - i} · (-1)^{j - k} e_{j - k} = δ_{ij}, the sum being empty for j < i.

theorem TauCeti.hsymmInt_sub_mul_neg_one_pow_mul_esymmInt_sub_eq_zero {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] {i j k : ℕ} (hk : k < i ∨ j < k) : hsymmInt σ R (↑k - ↑i) * ((-1) ^ (↑j - ↑k).toNat * esymmInt σ R (↑j - ↑k)) = 0

The h--e summand vanishes when k lies outside the interval [i, j]: either k < i, so h_{k - i} = 0, or j < k, so e_{j - k} = 0.

noncomputable def TauCeti.hsymmToeplitz (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (n : ℕ) : Matrix (Fin n) (Fin n) (MvPolynomial σ R)

The Toeplitz matrix of complete homogeneous symmetric polynomials (h_{j - i})_{0 ≤ i, j < n}, with negative indices read as 0.

@[simp]

theorem TauCeti.hsymmToeplitz_apply (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (n : ℕ) (i j : Fin n) : hsymmToeplitz σ R n i j = hsymmInt σ R (↑↑j - ↑↑i)

noncomputable def TauCeti.esymmToeplitz (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (n : ℕ) : Matrix (Fin n) (Fin n) (MvPolynomial σ R)

The signed Toeplitz matrix of elementary symmetric polynomials ((-1)^{j - i} e_{j - i})_{0 ≤ i, j < n}, with negative indices read as 0.

@[simp]

theorem TauCeti.esymmToeplitz_apply (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (n : ℕ) (i j : Fin n) : esymmToeplitz σ R n i j = (-1) ^ (↑↑j - ↑↑i).toNat * esymmInt σ R (↑↑j - ↑↑i)

theorem TauCeti.hsymmToeplitz_mul_esymmToeplitz_apply (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] (n : ℕ) (i j : Fin n) : (hsymmToeplitz σ R n * esymmToeplitz σ R n) i j = if i = j then 1 else 0

The entry of hsymmToeplitz * esymmToeplitz at (i, j) is the convolution of h and the signed e over r + s = j - i, which is δ_{ij}.

theorem TauCeti.hsymmToeplitz_mul_esymmToeplitz (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] (n : ℕ) : hsymmToeplitz σ R n * esymmToeplitz σ R n = 1

The Toeplitz matrices of h and signed e are inverse: (h_{j - i}) · ((-1)^{j - i} e_{j - i}) = 1. This is the matrix form of the h--e convolution TauCeti.sum_Icc_hsymmInt_mul_neg_one_pow_mul_esymmInt, and the input to Jacobi's complementary-minor identity in the dual (transpose) Jacobi--Trudi formula.

@[simp]

theorem TauCeti.det_hsymmToeplitz (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommRing R] (n : ℕ) : (hsymmToeplitz σ R n).det = 1

The Toeplitz matrix (h_{j - i}) is upper unitriangular, so its determinant is 1.

@[simp]

theorem TauCeti.det_esymmToeplitz (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (n : ℕ) : (esymmToeplitz σ R n).det = 1

The signed Toeplitz matrix ((-1)^{j - i} e_{j - i}) is upper unitriangular, so its determinant is 1.

theorem TauCeti.esymmToeplitz_apply_eq_neg_one_pow_mul (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (N : ℕ) (i j : Fin N) : esymmToeplitz σ R N i j = (-1) ^ ↑i * ((-1) ^ ↑j * esymmInt σ R (↑↑j - ↑↑i))

The sign carried by an entry of the signed elementary Toeplitz matrix splits as a factor depending only on the row and a factor depending only on the column. Below the diagonal the entry vanishes, so the two sides agree there as well.

theorem TauCeti.det_submatrix_esymmToeplitz (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (N : ℕ) (f g : ι → Fin N) : ((esymmToeplitz σ R N).submatrix f g).det = (∏ i : ι, (-1) ^ ↑(f i)) * (Matrix.of fun (i j : ι) => esymmInt σ R (↑↑(g j) - ↑↑(f i))).det * ∏ j : ι, (-1) ^ ↑(g j)

A minor of the signed elementary Toeplitz matrix is a product of signs, one per row and one per column, times the corresponding minor of the integer-indexed elementary symmetric polynomials.