The Hall inner product

The Hall inner product is the symmetric bilinear form on the symmetric polynomials of degree n for which the Schur polynomials are orthonormal. Macdonald introduces it instead as the form for which the complete homogeneous products h_μ and the monomial symmetric polynomials m_ν are dual bases, ⟨h_μ, m_ν⟩ = δ_{μν}, and deduces the orthonormality of the Schur functions from the Cauchy identity. Here the logic runs the other way: the form is defined by the Schur basis, and the duality of h and m is a theorem. It follows from the two Kostka expansions h_ν = ∑_λ K_{λν} s_λ and s_λ = ∑_ν K_{λν} m_ν: pairing with h_ν reads off the coefficient of the sorted monomial x^ν (TauCeti.hallInner_hsymmPart_left).

The form lives on TauCeti.symmetricHomogeneousSubmodule σ R n for a finite alphabet σ and a commutative ring R, the module of which the Schur polynomials of the partitions of n with at most Fintype.card σ parts are a basis (TauCeti.schurPolyBasis). When σ has at least n letters this module is the degree-n part of the ring of symmetric functions, and the form is the classical one. With fewer letters the classical form does not descend to the quotient in which the Schur functions of the longer partitions vanish, those functions having norm 1; instead it is the restriction of the classical form to the span of the surviving Schur functions, transported to the symmetric polynomials in σ along the isomorphism carrying each surviving Schur function to its specialization.

The power-sum orthogonality ⟨p_ρ, p_ρ'⟩ = z_ρ δ_{ρρ'} and the isometry of the Frobenius characteristic need the character table of the symmetric group, and are proved in TauCeti/RepresentationTheory/Symmetric/FrobeniusCharacteristic.lean.

Main definitions

• TauCeti.hallInner: the Hall inner product on the symmetric polynomials of degree n.

Main results

• TauCeti.hallInner_schurPoly: the Schur polynomials are orthonormal.
• TauCeti.hallInner_apply: the form is the dot product of Schur coordinates.
• TauCeti.isSymm_hallInner and TauCeti.nondegenerate_hallInner: it is symmetric and nondegenerate.
• TauCeti.hallInner_hsymmPart_left: pairing with h_ν reads off the coefficient of x^ν.
• TauCeti.hallInner_hsymmPart_msymm: the h_μ and the m_ν are dual bases.

References

• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 4, (4.5)–(4.8).
• R. P. Stanley, Enumerative Combinatorics, Vol. 2, Section 7.9.

The Hall inner product

noncomputable def TauCeti.hallInner (σ : Type u_1) [Fintype σ] (R : Type u_2) [CommRing R] (n : ℕ) : LinearMap.BilinForm R ↥(symmetricHomogeneousSubmodule σ R n)

The Hall inner product on the symmetric polynomials of degree n in the alphabet σ: the bilinear form in which the Schur polynomials of the partitions of n with at most Fintype.card σ parts are orthonormal (TauCeti.hallInner_schurPoly). It is the dot product of the coordinates in the Schur basis (TauCeti.hallInner_apply), and the complete homogeneous products h_μ and the monomial symmetric polynomials m_ν are dual bases for it (TauCeti.hallInner_hsymmPart_msymm).

theorem TauCeti.hallInner_schurPolyBasis {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (μ ν : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ((hallInner σ R n) ((schurPolyBasis σ R n) μ)) ((schurPolyBasis σ R n) ν) = if μ = ν then 1 else 0

The Schur basis is orthonormal for the Hall inner product. It is not a simp lemma: TauCeti.hallInner_schurPolyBasis_right already reduces the left side to a Schur coordinate.

@[simp]

theorem TauCeti.hallInner_schurPolyBasis_right {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (p : ↥(symmetricHomogeneousSubmodule σ R n)) (μ : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) : ((hallInner σ R n) p) ((schurPolyBasis σ R n) μ) = ((schurPolyBasis σ R n).repr p) μ

Pairing with a Schur polynomial on the right reads off the Schur coordinate.

@[simp]

theorem TauCeti.hallInner_schurPolyBasis_left {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (μ : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }) (p : ↥(symmetricHomogeneousSubmodule σ R n)) : ((hallInner σ R n) ((schurPolyBasis σ R n) μ)) p = ((schurPolyBasis σ R n).repr p) μ

Pairing with a Schur polynomial on the left reads off the Schur coordinate.

theorem TauCeti.hallInner_apply {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (p q : ↥(symmetricHomogeneousSubmodule σ R n)) : ((hallInner σ R n) p) q = ∑ μ : { ν : n.Partition // ν.parts.card ≤ Fintype.card σ }, ((schurPolyBasis σ R n).repr p) μ * ((schurPolyBasis σ R n).repr q) μ

The Hall inner product is the dot product of Schur coordinates.

theorem TauCeti.hallInner_comm {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (p q : ↥(symmetricHomogeneousSubmodule σ R n)) : ((hallInner σ R n) p) q = ((hallInner σ R n) q) p

The Hall inner product is symmetric.

theorem TauCeti.isSymm_hallInner {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} : (hallInner σ R n).IsSymm

The Hall inner product is a symmetric bilinear form.

theorem TauCeti.nondegenerate_hallInner {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} : (hallInner σ R n).Nondegenerate

The Hall inner product is nondegenerate: a symmetric polynomial orthogonal to every Schur polynomial has all its Schur coordinates 0.

@[simp]

theorem TauCeti.hallInner_schurPoly {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} (l μ : n.Partition) (hμ : μ.parts.card ≤ Fintype.card σ) : ((hallInner σ R n) ⟨schurPoly σ R l, ⋯⟩) ⟨schurPoly σ R μ, ⋯⟩ = if l = μ then 1 else 0

The Schur polynomials are orthonormal for the Hall inner product, stated for partitions: ⟨s_λ, s_μ⟩ = δ_{λμ} whenever μ has at most Fintype.card σ parts. No bound on λ is needed: the Schur polynomial of a longer partition is 0, and that partition differs from μ.

The complete homogeneous and monomial bases are dual

@[simp]

theorem TauCeti.hallInner_hsymmPart_left {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} [DecidableEq σ] (ν : n.Partition) (hν : ν.parts.card ≤ Fintype.card σ) (p : ↥(symmetricHomogeneousSubmodule σ R n)) : ((hallInner σ R n) ⟨MvPolynomial.hsymmPart σ R ν, ⋯⟩) p = (↑p).coeff (partWeight σ ν)

Pairing with h_ν reads off the coefficient of x^ν: for a partition ν with at most Fintype.card σ parts, the Hall inner product of h_ν with a symmetric polynomial of degree n is its coefficient at the sorted monomial x^ν recording the parts of ν, which is its coordinate in the monomial basis (TauCeti.msymmBasis_repr_apply). On a Schur polynomial s_μ both sides are the Kostka number K_{μν}: the left by the expansion of h_ν in Schur polynomials, the right by the monomial expansion of s_μ.

theorem TauCeti.hallInner_hsymmPart_msymm {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommRing R] {n : ℕ} [DecidableEq σ] (μ ν : n.Partition) (hμ : μ.parts.card ≤ Fintype.card σ) : ((hallInner σ R n) ⟨MvPolynomial.hsymmPart σ R μ, ⋯⟩) ⟨MvPolynomial.msymm σ R ν, ⋯⟩ = if μ = ν then 1 else 0

The complete homogeneous products and the monomial symmetric polynomials are dual bases for the Hall inner product: ⟨h_μ, m_ν⟩ = δ_{μν} for partitions μ and ν of n, μ having at most Fintype.card σ parts. This is Macdonald's definition of the Hall inner product. No bound on ν is needed: the monomial symmetric polynomial of a longer partition is 0, and that partition differs from μ. It is not a simp lemma: TauCeti.hallInner_hsymmPart_left and TauCeti.coeff_msymm_partWeight already prove it.