Evaluating the complete homogeneous symmetric polynomial

The complete homogeneous symmetric polynomial h_d in variables indexed by a finite type σ is the sum of all monomials of degree d, one for each unordered d-tuple of indices. Evaluating it at a family f : σ → R therefore sums, over those unordered tuples, the product of the values f takes on the tuple: TauCeti.eval_hsymm.

In two variables the unordered d-tuples are the d + 1 splittings counted by TauCeti.symFinTwoEquiv, and the evaluation reads h_d(x, y) = ∑_{i ≤ d} xⁱ y^{d-i}: TauCeti.eval_hsymm_fin_two.

Reading the unordered tuples as their multiplicity functions instead writes h_d as the sum of the monomials of degree d, indexed by Finset.piAntidiag: TauCeti.hsymm_eq_sum_piAntidiag. Summed over all degrees, this is the generating function ∑ₙ hₙ tⁿ = ∏ᵢ ∑ₙ xᵢⁿ tⁿ, the product over the variables of the geometric series (1 - xᵢ t)⁻¹: TauCeti.mk_hsymm_eq_prod_mk_pow, and TauCeti.mk_aeval_hsymm_eq_prod_mk_pow at an arbitrary family of values. On the alphabet σ × τ, evaluated at products fᵢ gⱼ, the factors with a fixed first index multiply to ∑ₘ fᵢᵐ hₘ(g) tᵐ, so hₙ(fᵢ gⱼ) is the sum of ∏ᵢ fᵢ^{lᵢ} h_{lᵢ}(g) over the exponent vectors l on σ of total degree n: TauCeti.aeval_hsymm_prod_eq_sum_finsuppAntidiag. This is the first step of the Cauchy identity for Schur polynomials.

Determinantal formulas such as Jacobi--Trudi index h by integers, h_m being 0 for m < 0; reading a negative index as 0 through a truncated subtraction of natural numbers would silently give the wrong formula. TauCeti.hsymmInt is this integer-indexed complete homogeneous symmetric polynomial.

Main results

• TauCeti.eval_hsymm evaluates the complete homogeneous symmetric polynomial as a sum over the unordered d-tuples of indices.
• TauCeti.eval_hsymm_fin_two reads that off in two variables: h_d(x, y) = ∑_{i ≤ d} xⁱ y^{d-i}.
• TauCeti.hsymm_eq_sum_piAntidiag writes h_d as the sum of the monomials of degree d.
• TauCeti.mk_hsymm_eq_prod_mk_pow: the generating function of the h_d, and TauCeti.mk_aeval_hsymm_eq_prod_mk_pow, the same evaluated at an arbitrary family.
• TauCeti.aeval_hsymm_prod_eq_sum_finsuppAntidiag: hₙ(fᵢ gⱼ) = ∑_l ∏ᵢ fᵢ^{lᵢ} h_{lᵢ}(g).
• TauCeti.hsymmPart_mem_symmetricHomogeneousSubmodule: a product h_ν of complete homogeneous symmetric polynomials is symmetric and homogeneous of degree n for a partition ν of n.
• TauCeti.hsymmInt: the complete homogeneous symmetric polynomial h_m of an integer degree m, which is 0 for m < 0.

theorem TauCeti.eval_hsymm {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] (f : σ → R) (d : ℕ) : (MvPolynomial.eval f) (MvPolynomial.hsymm σ R d) = ∑ s : Sym σ d, (Multiset.map f ↑s).prod

The complete homogeneous symmetric polynomial evaluated: h_d(f) is the sum, over the unordered d-tuples of indices, of the product of the values f takes on the tuple.

theorem TauCeti.eval_hsymm_fin_two {R : Type u_1} [CommSemiring R] (f : Fin 2 → R) (d : ℕ) : (MvPolynomial.eval f) (MvPolynomial.hsymm (Fin 2) R d) = ∑ i ∈ Finset.range (d + 1), f 0 ^ i * f 1 ^ (d - i)

The complete homogeneous symmetric polynomial in two variables: h_d(x, y) is the sum of all d + 1 monomials xⁱ y^{d-i} of degree d.

theorem TauCeti.hsymm_eq_sum_piAntidiag {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (d : ℕ) : MvPolynomial.hsymm σ R d = ∑ γ ∈ Finset.univ.piAntidiag d, ∏ i : σ, MvPolynomial.X i ^ γ i

The monomial expansion of the complete homogeneous symmetric polynomial: h_d is the sum of the monomials ∏ᵢ X_i ^ γ_i over the exponent vectors γ of total degree d. This is the multiplicity-function form of MvPolynomial.hsymm, whose summands are indexed by the unordered d-tuples of variables.

theorem TauCeti.mk_hsymm_eq_prod_mk_pow {σ : Type u_1} [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] : (PowerSeries.mk fun (n : ℕ) => MvPolynomial.hsymm σ R n) = ∏ i : σ, PowerSeries.mk fun (n : ℕ) => MvPolynomial.X i ^ n

The generating function of the complete homogeneous symmetric polynomials: ∑ₙ hₙ tⁿ = ∏ᵢ ∑ₙ xᵢⁿ tⁿ, as power series over MvPolynomial σ R. Each factor is the geometric series (1 - xᵢ t)⁻¹, so the coefficient of tⁿ collects one monomial of degree n for every exponent vector.

theorem TauCeti.mk_aeval_hsymm_eq_prod_mk_pow {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype σ] [DecidableEq σ] [CommSemiring R] [CommSemiring S] [Algebra R S] (ψ : σ → S) : (PowerSeries.mk fun (n : ℕ) => (MvPolynomial.aeval ψ) (MvPolynomial.hsymm σ R n)) = ∏ i : σ, PowerSeries.mk fun (n : ℕ) => ψ i ^ n

The generating function of the complete homogeneous symmetric polynomials, evaluated: ∑ₙ hₙ(ψ) tⁿ = ∏ᵢ ∑ₙ ψᵢⁿ tⁿ for a family ψ in a commutative R-algebra S, as power series over S. This is TauCeti.mk_hsymm_eq_prod_mk_pow with the variables evaluated at ψ.

theorem TauCeti.aeval_hsymm_prod_eq_sum_finsuppAntidiag {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype σ] [DecidableEq σ] [Fintype τ] [DecidableEq τ] [CommSemiring R] [CommSemiring S] [Algebra R S] (f : σ → S) (g : τ → S) (n : ℕ) : (MvPolynomial.aeval fun (p : σ × τ) => f p.1 * g p.2) (MvPolynomial.hsymm (σ × τ) R n) = ∑ l ∈ Finset.univ.finsuppAntidiag n, ∏ i : σ, f i ^ l i * (MvPolynomial.aeval g) (MvPolynomial.hsymm τ R (l i))

hₙ of the products fᵢ gⱼ, grouped by the first index: substituting fᵢ gⱼ for the variable indexed by (i, j) in hₙ on the alphabet σ × τ gives ∑_l ∏ᵢ fᵢ^{lᵢ} h_{lᵢ}(g), the sum running over the exponent vectors l on σ of total degree n. In generating-function form, the product of the geometric series (1 - fᵢ gⱼ t)⁻¹ over all pairs is computed one i at a time, the factors with a fixed i multiplying to ∑ₘ fᵢᵐ hₘ(g) tᵐ.

theorem TauCeti.hsymmPart_mem_symmetricHomogeneousSubmodule {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommSemiring R] {n : ℕ} (ν : n.Partition) : MvPolynomial.hsymmPart σ R ν ∈ symmetricHomogeneousSubmodule σ R n

A product of complete homogeneous symmetric polynomials is symmetric and homogeneous: for a partition ν of n, h_ν = ∏ᵢ h_{νᵢ} lies in TauCeti.symmetricHomogeneousSubmodule σ R n, each factor h_{νᵢ} being symmetric and homogeneous of degree νᵢ.

noncomputable def TauCeti.hsymmInt (σ : Type u_1) [Fintype σ] [DecidableEq σ] (R : Type u_2) [CommSemiring R] (m : ℤ) : MvPolynomial σ R

The complete homogeneous symmetric polynomial of integer degree m: h_m for m ≥ 0 and 0 for m < 0. This is the indexing determinantal formulas such as Jacobi--Trudi use.

@[simp]

theorem TauCeti.hsymmInt_of_nonneg {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {m : ℤ} (hm : 0 ≤ m) : hsymmInt σ R m = MvPolynomial.hsymm σ R m.toNat

In a nonnegative degree, TauCeti.hsymmInt is MvPolynomial.hsymm.

@[simp]

theorem TauCeti.hsymmInt_of_neg {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {m : ℤ} (hm : m < 0) : hsymmInt σ R m = 0

In a negative degree, TauCeti.hsymmInt vanishes.

theorem TauCeti.hsymmInt_natCast {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] (n : ℕ) : hsymmInt σ R ↑n = MvPolynomial.hsymm σ R n

In a natural-number degree, TauCeti.hsymmInt is MvPolynomial.hsymm.

theorem TauCeti.hsymmInt_zero {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] : hsymmInt σ R 0 = 1

h_0 = 1.

@[simp]

theorem TauCeti.map_hsymmInt {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommSemiring S] (m : ℤ) (f : R →+* S) : (MvPolynomial.map f) (hsymmInt σ R m) = hsymmInt σ S m

Changing the coefficients along a ring homomorphism preserves TauCeti.hsymmInt.

@[simp]

theorem TauCeti.rename_hsymmInt {σ : Type u_1} [Fintype σ] [DecidableEq σ] {R : Type u_2} [CommSemiring R] {τ : Type u_3} [Fintype τ] [DecidableEq τ] (m : ℤ) (e : σ ≃ τ) : (MvPolynomial.rename ⇑e) (hsymmInt σ R m) = hsymmInt τ R m

Renaming the variables along a bijection preserves TauCeti.hsymmInt.