The ω-involution on symmetric functions #
The ω-involution is an algebra automorphism of the ring of symmetric functions that swaps the elementary and complete homogeneous symmetric polynomials:
- ω(e_n) = h_n
- ω(h_n) = e_n
- ω(s_λ) = s_{λᵗ}
This file defines the ω-involution and proves its key properties.
Main definitions #
SymmetricFunctions.hsymmAlgHom: The algebra homomorphism fromMvPolynomial (Fin n) Rto the symmetric subalgebra sendingX_itoh_{i+1}.SymmetricFunctions.omegaInvolution: The ω-involution on symmetric polynomials.
Main results #
SymmetricFunctions.omegaInvolution_esymm_succ: ω(e_{k+1}) = h_{k+1} for k < nSymmetricFunctions.omegaInvolution_hsymm_succ: ω(h_{k+1}) = e_{k+1} for k < nSymmetricFunctions.omegaInvolution_involutive: ω ∘ ω = id
Implementation notes #
The ω-involution is defined using the fundamental theorem of symmetric polynomials. The elementary symmetric polynomials generate the symmetric subalgebra, so we can define ω by specifying ω(e_k) = h_k and extending algebraically.
To prove that ω is an involution, we need to show that ω(h_k) = e_k. This requires proving that the h_k also generate the symmetric subalgebra (which they do, by the Newton-Girard relations and the fundamental theorem).
References #
- [Stanley, Enumerative Combinatorics, Vol. 2][Stanley-EC2], Section 7.8
- [Grinberg-Reiner, Hopf algebras in combinatorics][GriRei], Section 2.4
Why this is needed #
The ω-involution is essential for proving the second Jacobi-Trudi formula (jacobiTrudi_e in PieriJacobiTrudi.lean). The standard proof proceeds as follows:
- First Jacobi-Trudi: s_{λ/μ} = det(h_{λᵢ - μⱼ - i + j})
- Apply ω: ω(s_{λ/μ}) = det(ω(h_{...})) = det(e_{...})
- Since ω(s_{λ/μ}) = s_{λᵗ/μᵗ}: s_{λᵗ/μᵗ} = det(e_{λᵢ - μⱼ - i + j})
- Substitute λ → λᵗ: s_{λ/μ} = det(e_{(λᵗ)ᵢ - (μᵗ)ⱼ - i + j})
This file provides the infrastructure for steps 2 and 3.
Transfer lemmas for esymm and hsymm via rename #
These lemmas allow us to transfer results about symmetric polynomials from one
finite type to another via the rename operation.
Transfer lemma: esymm is preserved under rename by an equivalence.
Transfer lemma: hsymm is preserved under rename by an equivalence.
Newton-Girard identity for arbitrary finite type σ.
Transferred from newtonGirard_eh via rename.
Helper lemma: sum of subalgebra elements coerces to sum of their values.
The hsymm algebra homomorphism #
Similar to esymmAlgHom, we define an algebra homomorphism that sends
X_i to the (i+1)-th complete homogeneous symmetric polynomial.
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+1)$-th complete homogeneous symmetric polynomial.
This is analogous to MvPolynomial.esymmAlgHom which sends $x_i$ to $e_{i+1}$.
Equations
- SymmetricFunctions.hsymmAlgHom σ R n = MvPolynomial.aeval fun (i : Fin n) => ⟨MvPolynomial.hsymm σ R (↑i + 1), ⋯⟩
Instances For
The ω-involution #
The ω-involution is defined as the composition: ω = hsymmAlgHom ∘ esymmAlgEquiv.symm
This maps each e_k to h_k.
The ω-involution on symmetric polynomials.
This is an algebra endomorphism of the symmetric subalgebra that swaps elementary and complete homogeneous symmetric polynomials:
- ω(e_n) = h_n
- ω(h_n) = e_n
The definition uses the fundamental theorem of symmetric polynomials: since the e_k generate the symmetric subalgebra, we define ω by specifying ω(e_k) = h_k and extending algebraically.
Note: For this definition to work, we need Fintype.card σ = n.
Equations
- SymmetricFunctions.omegaInvolution hn = (SymmetricFunctions.hsymmAlgHom σ R n).comp ↑(MvPolynomial.esymmAlgEquiv σ R hn).symm
Instances For
The ω-involution maps e_k to h_k for 0 < k ≤ n.
The ω-involution maps 1 to 1.
The ω-involution preserves addition.
The ω-involution preserves multiplication.
The ω-involution commutes with scalar multiplication.
The ω-involution maps h_k to e_k #
To show that ω(h_k) = e_k, we need to establish that the h_k generate the symmetric
subalgebra. This is proved in the Definitions.lean file as hsymm_algebraicIndependent.
Given this, we can define the "dual" ω-involution that maps h_k to e_k, and show that it equals the original ω-involution composed with itself.
The symmetric Newton-Girard identity: ∑{j=0}^n (-1)^j h_j e{n-j} = 0 for n > 0.
This is the "symmetric" version of newtonGirard_eh (which gives ∑ (-1)^j e_j h_{n-j} = 0).
The proof follows from newtonGirard_eh by reindexing (j ↦ n-j) and using:
- Commutativity: h_j * e_{n-j} = e_{n-j} * h_j
- Sign identity: (-1)^{n-j} * (-1)^n = (-1)^j (since (n-j+n) mod 2 = j mod 2)
This identity is the key ingredient for proving omegaInvolution_hsymm_succ.
Recurrence for h_n from Newton-Girard: h_n = ∑{j=1}^n (-1)^{j+1} e_j h{n-j} for n > 0.
This follows from isolating the j=0 term in newtonGirard_eh_general:
∑{j=0}^n (-1)^j e_j h{n-j} = 0
⟹ e_0 h_n + ∑{j=1}^n (-1)^j e_j h{n-j} = 0 (since e_0 = 1)
⟹ h_n = -∑{j=1}^n (-1)^j e_j h{n-j} = ∑{j=1}^n (-1)^{j+1} e_j h{n-j}
Recurrence for e_n from symmetric Newton-Girard: e_n = ∑{j=1}^n (-1)^{j+1} h_j e{n-j} for n > 0.
This follows from isolating the j=0 term in newtonGirard_he:
∑{j=0}^n (-1)^j h_j e{n-j} = 0
⟹ h_0 e_n + ∑{j=1}^n (-1)^j h_j e{n-j} = 0 (since h_0 = 1)
⟹ e_n = -∑{j=1}^n (-1)^j h_j e{n-j} = ∑{j=1}^n (-1)^{j+1} h_j e{n-j}
The ω-involution maps h_k to e_k for 0 < k ≤ n.
Proof sketch: The h_k are algebraically independent and generate the symmetric subalgebra. Therefore, there exists a unique algebra homomorphism ω' that maps h_k to e_k. We show that ω' = ω by checking that ω(h_k) = e_k using the Newton-Girard relations.
The Newton-Girard relations give: k * e_k = ∑{i=1}^{k} (-1)^{i-1} e{k-i} * p_i k * h_k = ∑{i=1}^{k} h{k-i} * p_i
These can be used to express h_k in terms of e_k and p_k, and vice versa. Since ω(p_k) = (-1)^{k-1} p_k (which follows from the definition), we get ω(h_k) = e_k.
The ω-involution is an involution: ω ∘ ω = id.
This follows from ω(e_k) = h_k and ω(h_k) = e_k, since the e_k generate the symmetric subalgebra.
The ω-involution is bijective.
The ω-involution as an algebra equivalence.
Equations
Instances For
Application to Jacobi-Trudi #
The ω-involution is used to prove the second Jacobi-Trudi formula from the first. The key insight is that applying ω to both sides of the first Jacobi-Trudi formula transforms h_k entries to e_k entries, while transforming s_{λ/μ} to s_{λᵗ/μᵗ}.
The ω-involution applied to a determinant of h-entries gives a determinant of e-entries.
This is a key step in the proof of the second Jacobi-Trudi formula: ω(det(h_{λᵢ - μⱼ - i + j})) = det(e_{λᵢ - μⱼ - i + j})
Note: This requires showing that ω commutes with taking determinants, which follows from ω being an algebra homomorphism.