N-partitions and Monomial Symmetric Polynomials

This file formalizes N-partitions and monomial symmetric polynomials, following Section sec.sf.m of the source.

Main definitions

• NPartition N - a weakly decreasing N-tuple of nonnegative integers (Definition def.sf.Npar) — alias for canonical definition in NPartition.lean
• NPartition.size - the sum of entries of an N-partition (|λ|)
• NPartition.ofPartition - converts a partition of length ≤ N to an N-partition by padding with zeros (Proposition prop.sf.Npar-as-par) — re-exported from NPartition.lean
• NPartition.toPartition - converts an N-partition to a partition by removing zeros — re-exported from NPartition.lean
• NPartition.equivPartition - the equivalence (bijection) between partitions of length ≤ N and N-partitions (Proposition prop.sf.Npar-as-par)
• monomialExp - x^a for a ∈ ℕ^N (Definition def.sf.sort (a))
• sortTuple - sorts a tuple in weakly decreasing order (Definition def.sf.sort (b))
• monomialSymm - the monomial symmetric polynomial m_λ (Definition def.sf.m)
• symmHomogeneous - the submodule of homogeneous symmetric polynomials of degree n (Theorem thm.sf.m-basis (c))

Main results

• NPartition.bijection_partition - bijection between partitions of length ≤ N and N-partitions (Proposition prop.sf.Npar-as-par)
• elem_symm_eq_monomialSymm - e_n expressed via monomial symmetric polynomials (Proposition prop.sf.ehp-through-m (a))
• homog_symm_eq_sum_monomialSymm - h_n as sum of m_μ over |μ| = n (Proposition prop.sf.ehp-through-m (b))
• power_sum_eq_monomialSymm - p_n expressed via monomial symmetric polynomials (Proposition prop.sf.ehp-through-m (c))
• monomialSymm_linearIndependent - the family (m_μ) is linearly independent (Theorem thm.sf.m-basis (a), part 1)
• monomialSymm_spans - the family (m_μ) spans the symmetric polynomials (Theorem thm.sf.m-basis (a), part 2)
• symm_eq_sum_coeff_monomialSymm - expansion formula for symmetric polynomials (Theorem thm.sf.m-basis (b))
• monomialSymm_homogeneous_linearIndependent - the family (m_μ) with |μ| = n is linearly independent (Theorem thm.sf.m-basis (d), linear independence)
• monomialSymm_homogeneous_spans - the family (m_μ) with |μ| = n spans 𝒮_n (Theorem thm.sf.m-basis (d), spanning)
• monomialSymm_basis_homogeneous - the family (m_μ) with |μ| = n forms a basis of 𝒮_n (Theorem thm.sf.m-basis (d))
• sigma_coeff_permute - permutation transforms polynomial coefficients (Proposition prop.sf.sigma-pol-coeff)

References

• Source: AlgebraicCombinatorics/tex/SymmetricFunctions/MonomialSymmetric.tex

Implementation notes

We use Fin N → ℕ to represent N-tuples of nonnegative integers. The ordering on Fin N is the standard one, and "weakly decreasing" means ∀ i j, i ≤ j → μ j ≤ μ i (i.e., antitone with respect to the standard order on Fin N).

Mathlib already has MvPolynomial.msymm for monomial symmetric polynomials indexed by Nat.Partition. Our NPartition provides an alternative indexing that is more natural for the N-variable setting and corresponds directly to the textbook presentation.

N-partitions (Definition def.sf.Npar)

An N-partition is a weakly decreasing N-tuple of nonnegative integers.

This namespace uses the canonical NPartition definition from NPartition.lean (imported above). All basic lemmas (ext, size, zero, length, etc.) are inherited from the canonical definition via the abbrev below.

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricFunctions.NPartition (N : ℕ) : Type

Alias for the canonical NPartition type within this namespace. An N-partition is a weakly decreasing N-tuple of nonnegative integers. (Definition def.sf.Npar)

This is represented as a function Fin N → ℕ that is antitone (i.e., i ≤ j → parts j ≤ parts i).

All basic operations (size, length, zero, etc.) and lemmas are inherited from the canonical _root_.NPartition definition in NPartition.lean.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.NPartition N = NPartition N

Bijection with partitions of length ≤ N (Proposition prop.sf.Npar-as-par)

There is a bijection between partitions of length ≤ N and N-partitions.

The core definitions (ofPartition, toPartition, ofPartition_size, toPartition_card_le) are defined in NPartition.lean and re-exported here for convenience within this namespace.

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricFunctions.NPartition.ofPartition {N n : ℕ} (p : n.Partition) (hp : p.parts.card ≤ N) : NPartition N

Convert a partition (as a Nat.Partition) to an N-partition by padding with zeros. Re-export of _root_.NPartition.ofPartition.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.NPartition.ofPartition p hp = NPartition.ofPartition p hp

@[reducible, inline]

abbrev AlgebraicCombinatorics.SymmetricFunctions.NPartition.toPartition {N : ℕ} (mu : NPartition N) : (NPartition.size mu).Partition

Convert an N-partition to a partition by removing trailing zeros. Re-export of _root_.NPartition.toPartition.

Equations

• mu.toPartition = NPartition.toPartition mu

theorem AlgebraicCombinatorics.SymmetricFunctions.NPartition.ofPartition_size {N n : ℕ} (p : n.Partition) (hp : p.parts.card ≤ N) : NPartition.size (ofPartition p hp) = n

The size of ofPartition p equals n (the sum of the original partition). Re-export of _root_.NPartition.ofPartition_size.

theorem AlgebraicCombinatorics.SymmetricFunctions.NPartition.toPartition_card_le {N : ℕ} (mu : NPartition N) : mu.toPartition.parts.card ≤ N

The number of non-zero parts of an N-partition is at most N. Re-export of _root_.NPartition.toPartition_card_le.

theorem AlgebraicCombinatorics.SymmetricFunctions.NPartition.Nat.Partition.parts_cast {m n : ℕ} (h : m = n) (p : m.Partition) : (h ▸ p).parts = p.parts

Helper lemma: casting a partition preserves its parts.

noncomputable def AlgebraicCombinatorics.SymmetricFunctions.NPartition.equivPartition {N : ℕ} (n : ℕ) : { p : n.Partition // p.parts.card ≤ N } ≃ { mu : NPartition N // NPartition.size mu = n }

The equivalence between partitions of length ≤ N that sum to n and N-partitions of size n. (Proposition prop.sf.Npar-as-par)

This provides the bijection:

• Forward: pad partition with zeros to get N-partition
• Backward: remove trailing zeros from N-partition to get partition

Note: We state this as an Equiv which is the proper way to express a bijection in Mathlib.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.SymmetricFunctions.NPartition.ofPartition_injective {N : ℕ} (n : ℕ) : Function.Injective fun (x : { p : n.Partition // p.parts.card ≤ N }) => ofPartition ↑x ⋯

theorem AlgebraicCombinatorics.SymmetricFunctions.NPartition.bijection_partition {N : ℕ} (n : ℕ) : Function.Bijective fun (x : { p : n.Partition // p.parts.card ≤ N }) => (equivPartition n) x

The bijection between partitions of length ≤ N and N-partitions (Proposition prop.sf.Npar-as-par)

This is a corollary of equivPartition stating that the map is bijective.

Monomials and sorting (Definition def.sf.sort)

noncomputable def AlgebraicCombinatorics.SymmetricFunctions.monomialExp {R : Type u_1} [CommSemiring R] {N : ℕ} (a : Fin N → ℕ) : MvPolynomial (Fin N) R

The monomial x^a = x₁^{a₁} x₂^{a₂} ⋯ x_N^{a_N} for a tuple a ∈ ℕ^N. (Definition def.sf.sort (a))

Equations

• AlgebraicCombinatorics.SymmetricFunctions.monomialExp a = ∏ i : Fin N, MvPolynomial.X i ^ a i

def AlgebraicCombinatorics.SymmetricFunctions.sortTuple {N : ℕ} (a : Fin N → ℕ) : NPartition N

Sort a tuple in weakly decreasing order to get an N-partition. (Definition def.sf.sort (b))

Equations

• One or more equations did not get rendered due to their size.

API for monomialExp (Definition def.sf.sort (a))

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_eq_monomial {R : Type u_1} [CommSemiring R] {N : ℕ} (a : Fin N → ℕ) : monomialExp a = (MvPolynomial.monomial (Finsupp.equivFunOnFinite.symm a)) 1

monomialExp equals the Mathlib monomial with the given exponent.

@[simp]

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_coeff_self {R : Type u_1} [CommSemiring R] {N : ℕ} (a : Fin N → ℕ) : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm a) (monomialExp a) = 1

Coefficient of the monomial x^a in monomialExp a is 1.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_coeff_ne {R : Type u_1} [CommSemiring R] {N : ℕ} (a b : Fin N → ℕ) (h : a ≠ b) : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm b) (monomialExp a) = 0

Coefficient of a different monomial in monomialExp a is 0.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_totalDegree {R : Type u_1} [CommSemiring R] {N : ℕ} [Nontrivial R] (a : Fin N → ℕ) : (monomialExp a).totalDegree = ∑ i : Fin N, a i

The total degree of monomialExp a is the sum of entries of a (when nonzero).

@[simp]

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_zero {R : Type u_1} [CommSemiring R] {N : ℕ} : monomialExp 0 = 1

monomialExp 0 is 1.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialExp_add {R : Type u_1} [CommSemiring R] {N : ℕ} (a b : Fin N → ℕ) : monomialExp (a + b) = monomialExp a * monomialExp b

monomialExp is multiplicative in the exponent.

API for sortTuple (Definition def.sf.sort (b))

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_sorted_length {N : ℕ} (a : Fin N → ℕ) : ((Multiset.map a Finset.univ.val).sort fun (x1 x2 : ℕ) => x1 ≥ x2).length = N

The length of the sorted list equals N.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_parts_eq {N : ℕ} (a : Fin N → ℕ) (i : Fin N) : (sortTuple a).parts i = ((Multiset.map a Finset.univ.val).sort fun (x1 x2 : ℕ) => x1 ≥ x2).get ⟨↑i, ⋯⟩

Access to the sorted list entries for valid indices.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_sum_eq {N : ℕ} (a : Fin N → ℕ) : ∑ i : Fin N, (sortTuple a).parts i = ∑ i : Fin N, a i

The sum of entries is preserved by sorting.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_size {N : ℕ} (a : Fin N → ℕ) : NPartition.size (sortTuple a) = ∑ i : Fin N, a i

The size of sortTuple a equals the sum of entries of a.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_of_antitone {N : ℕ} (a : Fin N → ℕ) (ha : Antitone a) : (sortTuple a).parts = a

If a tuple is already antitone (weakly decreasing), sorting doesn't change it.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_of_NPartition {N : ℕ} (mu : NPartition N) : sortTuple mu.parts = mu

Sorting an NPartition's parts returns the same NPartition.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_idempotent {N : ℕ} (a : Fin N → ℕ) : sortTuple (sortTuple a).parts = sortTuple a

Sorting is idempotent: sorting an already sorted tuple gives the same tuple.

Addition of N-partitions

The Add (NPartition N) instance and related lemmas (add_size, add_comm, add_zero, zero_add, add_assoc) are provided by the canonical NPartition.lean file.

The canonical definition uses component-wise addition (without sorting), which is equivalent to sorting the sum for N-partitions since the sum of two antitone functions is antitone. This is witnessed by sortTuple_of_NPartition.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_eq_iff {N : ℕ} (a b : Fin N → ℕ) : sortTuple a = sortTuple b ↔ Multiset.map a Finset.univ.val = Multiset.map b Finset.univ.val

Two tuples have the same sort if and only if one is a permutation of the other. (Two tuples have the same multiset of values iff they sort to the same N-partition.)

Helper lemmas for symmetry proof

The following lemmas establish that sorting is invariant under permutation of the input, which is the key insight for proving that monomial symmetric polynomials are symmetric.

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTuple_comp_perm {N : ℕ} (a : Fin N → ℕ) (σ : Equiv.Perm (Fin N)) : sortTuple (a ∘ ⇑σ) = sortTuple a

Sorting is invariant under permutation of the input tuple. This is the key insight: sortTuple (a ∘ σ) = sortTuple a for any permutation σ, because sorting only depends on the multiset of values, not their order.

Monomial symmetric polynomials (Definition def.sf.m)

def AlgebraicCombinatorics.SymmetricFunctions.sortPreimage {N : ℕ} (mu : NPartition N) : Finset (Fin N → ℕ)

The set of tuples a ∈ ℕ^N with sort(a) = μ and entries bounded by μ.size. This is a finite set since entries are bounded.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicCombinatorics.SymmetricFunctions.monomialSymm {R : Type u_1} [CommSemiring R] {N : ℕ} (mu : NPartition N) : MvPolynomial (Fin N) R

The monomial symmetric polynomial m_μ corresponding to an N-partition μ. (Definition def.sf.m)

m_μ = ∑_{a ∈ ℕ^N : sort(a) = μ} x^a

This is the sum of all monomials whose exponent tuple sorts to μ.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.monomialSymm mu = ∑ a ∈ AlgebraicCombinatorics.SymmetricFunctions.sortPreimage mu, AlgebraicCombinatorics.SymmetricFunctions.monomialExp a

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_isSymmetric {R : Type u_1} [CommSemiring R] {N : ℕ} (mu : NPartition N) : (monomialSymm mu).IsSymmetric

The monomial symmetric polynomial is symmetric. (Follows from Definition def.sf.m)

The proof uses the fact that:

1. rename σ (monomialExp a) = monomialExp (a ∘ σ⁻¹)
2. sortTuple (a ∘ σ) = sortTuple a for any permutation σ
3. Therefore the sum over sortPreimage μ is invariant under rename σ

theorem AlgebraicCombinatorics.SymmetricFunctions.parts_mem_sortPreimage {N : ℕ} (mu : NPartition N) : mu.parts ∈ sortPreimage mu

The parts of an N-partition belong to its sortPreimage. This is because sorting an already sorted (antitone) tuple gives the same tuple.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_coeff_self {R : Type u_1} [CommSemiring R] {N : ℕ} (mu : NPartition N) : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm mu.parts) (monomialSymm mu) = 1

The coefficient of x^{μ.parts} in m_μ is 1. This is because μ.parts is the unique element of sortPreimage μ that equals μ.parts.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_coeff_ne {R : Type u_1} [CommSemiring R] {N : ℕ} (mu nu : NPartition N) (h : mu ≠ nu) : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm mu.parts) (monomialSymm nu) = 0

The coefficient of x^{μ.parts} in m_ν is 0 when μ ≠ ν. This is because the only monomial in m_ν with exponent sorting to ν must have exponent ν.parts (when looking at the sorted exponent), not μ.parts.

Elementary, homogeneous, and power sum via monomial symmetric polynomials

(Proposition prop.sf.ehp-through-m)

def AlgebraicCombinatorics.SymmetricFunctions.onesThenZeros {N : ℕ} (n : ℕ) (_hn : n ≤ N) : NPartition N

The N-partition (1, 1, ..., 1, 0, 0, ..., 0) with n ones and N-n zeros.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.onesThenZeros n _hn = { parts := fun (i : Fin N) => if ↑i < n then 1 else 0, antitone := ⋯ }

def AlgebraicCombinatorics.SymmetricFunctions.singletonPartition {N : ℕ} (n : ℕ) (_hN : 0 < N) : NPartition N

The N-partition (n, 0, 0, ..., 0) with n in the first position and zeros elsewhere.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.singletonPartition n _hN = { parts := fun (i : Fin N) => if ↑i = 0 then n else 0, antitone := ⋯ }

Helper lemmas for Proposition prop.sf.ehp-through-m

These lemmas express the elementary, complete homogeneous, and power sum symmetric polynomials in terms of products over all variables with appropriate exponents.

theorem AlgebraicCombinatorics.SymmetricFunctions.elem_symm_eq_monomialSymm {R : Type u_1} [CommSemiring R] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) (hn : n ≤ N) : MvPolynomial.esymm (Fin N) R n = monomialSymm (onesThenZeros n hn)

e_n = m_{(1,1,...,1,0,0,...,0)} where there are n ones. (Proposition prop.sf.ehp-through-m (a))

The proof uses the fact that esymm n is the sum over n-element subsets S of ∏_{i∈S} X_i, and each such product equals X^{χ_S} where χ_S is the indicator function of S. All indicator functions of n-element subsets sort to the same N-partition (1,...,1,0,...,0).

Label: prop.sf.ehp-through-m.a

def AlgebraicCombinatorics.SymmetricFunctions.NPartitionsOfSize {N : ℕ} (n : ℕ) : Finset (NPartition N)

The set of N-partitions of a given size, as a finite set. This is finite because each entry is bounded by the size.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.SymmetricFunctions.mem_NPartitionsOfSize {N : ℕ} (mu : NPartition N) (n : ℕ) : mu ∈ NPartitionsOfSize n ↔ NPartition.size mu = n

Membership characterization for NPartitionsOfSize: an N-partition is in NPartitionsOfSize n if and only if its size equals n.

instance AlgebraicCombinatorics.SymmetricFunctions.fintype_of_size {N : ℕ} (n : ℕ) : Fintype { μ : NPartition N // NPartition.size μ = n }

The set of N-partitions of size n is finite. This provides a Fintype instance for the subtype { μ : NPartition N // μ.size = n }.

This is needed for:

1. Counting arguments involving N-partitions of fixed size
2. Finite sums over N-partitions in the monomial symmetric polynomial basis theorems
3. The basis theorem thm.sf.m-basis which requires finiteness of N-partitions of each degree

Equations

• AlgebraicCombinatorics.SymmetricFunctions.fintype_of_size n = Fintype.ofFinset (AlgebraicCombinatorics.SymmetricFunctions.NPartitionsOfSize n) ⋯

theorem AlgebraicCombinatorics.SymmetricFunctions.finite_of_size {N : ℕ} (n : ℕ) : {μ : NPartition N | NPartition.size μ = n}.Finite

The set of N-partitions of size n is finite (set version). This is the Set.Finite version of fintype_of_size.

theorem AlgebraicCombinatorics.SymmetricFunctions.homog_symm_eq_sum_monomialSymm {R : Type u_1} [CommSemiring R] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) : MvPolynomial.hsymm (Fin N) R n = ∑ mu ∈ NPartitionsOfSize n, monomialSymm mu

h_n = ∑_{|μ| = n} m_μ where the sum is over N-partitions of size n. (Proposition prop.sf.ehp-through-m (b))

The proof uses the bijection between Sym (Fin N) n and tuples f : Fin N → ℕ with ∑ f = n, given by the count function. Each term (s.1.map X).prod = ∏ i, X i ^ (count i s) corresponds to a monomial X^f. Sorting partitions these tuples by their N-partition, so hsymm n = ∑_{|μ| = n} m_μ.

Label: prop.sf.ehp-through-m.b

theorem AlgebraicCombinatorics.SymmetricFunctions.power_sum_eq_monomialSymm {R : Type u_1} [CommSemiring R] {N : ℕ} [DecidableEq (Fin N)] (n : ℕ) (hn : n ≠ 0) (hN : 0 < N) : MvPolynomial.psum (Fin N) R n = monomialSymm (singletonPartition n hN)

p_n = m_{(n,0,0,...,0)} when N > 0 and n > 0. (Proposition prop.sf.ehp-through-m (c))

Important: This theorem requires n > 0. The case n = 0 is FALSE when N > 1:

• psum 0 = ∑ i, X i ^ 0 = N (the constant polynomial N)
• monomialSymm (singletonPartition 0 hN) = 1 (since the only tuple sorting to (0,...,0) is the zero tuple, and monomialExp (0,...,0) = 1)

The TeX source (MonomialSymmetric.tex, line 133) states "For each n ∈ ℕ, we have p_n = m_{(n,0,0,...,0)}" which is mathematically incorrect for n = 0 when N > 1.

The proof uses the fact that psum n = ∑ i, X i ^ n, and each term X i ^ n corresponds to the tuple (0,...,0,n,0,...,0) with n at position i. All N such tuples sort to the same N-partition (n, 0, 0, ..., 0).

When n > 0, the sortPreimage of (n, 0, ..., 0) consists exactly of the N single tuples (0,...,0,n,0,...,0), giving the bijection needed for the proof.

Label: prop.sf.ehp-through-m.c

theorem AlgebraicCombinatorics.SymmetricFunctions.psum_zero_eq_N {R : Type u_1} [CommSemiring R] {N : ℕ} : MvPolynomial.psum (Fin N) R 0 = ↑N

The n = 0 case: p_0 = N while m_{(0,...,0)} = 1.

This documents why power_sum_eq_monomialSymm requires n ≠ 0. When n = 0:

• psum 0 = ∑ i, X i ^ 0 = N (constant polynomial)
• monomialSymm (singletonPartition 0 hN) = 1 (single monomial x^0 = 1)

These are equal only when N = 1.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_zero_partition_eq_one {R : Type u_1} [CommSemiring R] {N : ℕ} (hN : 0 < N) : monomialSymm (singletonPartition 0 hN) = 1

Permutation action on polynomial coefficients (Proposition prop.sf.sigma-pol-coeff)

theorem AlgebraicCombinatorics.SymmetricFunctions.sigma_coeff_permute {R : Type u_1} [CommSemiring R] {N : ℕ} (sigma : Equiv.Perm (Fin N)) (f : MvPolynomial (Fin N) R) (a : Fin N → ℕ) : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm a) ((MvPolynomial.rename ⇑sigma) f) = MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm (a ∘ ⇑sigma)) f

The coefficient of a monomial in σ · f equals the coefficient of the permuted monomial in f. (Proposition prop.sf.sigma-pol-coeff)

[x₁^{a₁} x₂^{a₂} ⋯ x_N^{a_N}](σ · f) = [x₁^{a_{σ(1)}} x₂^{a_{σ(2)}} ⋯ x_N^{a_{σ(N)}}] f

Label: prop.sf.sigma-pol-coeff

Basis theorem for monomial symmetric polynomials (Theorem thm.sf.m-basis)

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_linearIndependent {R : Type u_1} [CommSemiring R] {N : ℕ} (S : Finset (NPartition N)) : LinearIndependent R fun (mu : ↥S) => monomialSymm ↑mu

The monomial symmetric polynomials are linearly independent. (Theorem thm.sf.m-basis (a), linear independence part)

Label: thm.sf.m-basis.a.indep

theorem AlgebraicCombinatorics.SymmetricFunctions.coeff_perm_eq_of_symmetric {R : Type u_1} [CommSemiring R] {N : ℕ} (f : MvPolynomial (Fin N) R) (hf : f.IsSymmetric) (d : Fin N →₀ ℕ) (σ : Equiv.Perm (Fin N)) : MvPolynomial.coeff (Finsupp.mapDomain (⇑σ) d) f = MvPolynomial.coeff d f

Key: coeff is constant on orbits for symmetric polynomials. If f is symmetric and σ is a permutation, then coeff (σ · d) f = coeff d f.

theorem AlgebraicCombinatorics.SymmetricFunctions.support_closed_under_perm {R : Type u_1} [CommSemiring R] {N : ℕ} (f : MvPolynomial (Fin N) R) (hf : f.IsSymmetric) (d : Fin N →₀ ℕ) (hd : d ∈ f.support) (σ : Equiv.Perm (Fin N)) : Finsupp.mapDomain (⇑σ) d ∈ f.support

For symmetric f, support is closed under permutation.

noncomputable def AlgebraicCombinatorics.SymmetricFunctions.sortTupleFinsupp {N : ℕ} (d : Fin N →₀ ℕ) : NPartition N

sortTupleFinsupp applied to a Finsupp.

Equations

• AlgebraicCombinatorics.SymmetricFunctions.sortTupleFinsupp d = AlgebraicCombinatorics.SymmetricFunctions.sortTuple (Finsupp.equivFunOnFinite d)

theorem AlgebraicCombinatorics.SymmetricFunctions.sortTupleFinsupp_perm {N : ℕ} (d : Fin N →₀ ℕ) (σ : Equiv.Perm (Fin N)) : sortTupleFinsupp (Finsupp.mapDomain (⇑σ) d) = sortTupleFinsupp d

sortTupleFinsupp is invariant under permutation.

theorem AlgebraicCombinatorics.SymmetricFunctions.coeff_eq_of_same_sort {R : Type u_1} [CommSemiring R] {N : ℕ} (f : MvPolynomial (Fin N) R) (hf : f.IsSymmetric) (d₁ d₂ : Fin N →₀ ℕ) (h : sortTupleFinsupp d₁ = sortTupleFinsupp d₂) : MvPolynomial.coeff d₁ f = MvPolynomial.coeff d₂ f

Coefficients are equal for exponents with the same sort (for symmetric polynomials). This follows from the fact that two tuples with the same sort differ by a permutation, and symmetric polynomials have permutation-invariant coefficients.

The proof requires the combinatorial fact that equal sorted multisets implies the existence of a permutation relating the two tuples.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_spans {R : Type u_1} [CommSemiring R] {N : ℕ} (f : MvPolynomial (Fin N) R) : f.IsSymmetric → f ∈ Submodule.span R (Set.range fun (mu : NPartition N) => monomialSymm mu)

The monomial symmetric polynomials span the symmetric polynomials. (Theorem thm.sf.m-basis (a), spanning part)

The proof proceeds by:

1. Writing f as a sum of monomials grouped by their sort
2. For symmetric f, all monomials with the same sort have the same coefficient
3. Factoring out the common coefficient from each group
4. Showing that the sum of monomials in each group equals monomialSymm μ

Label: thm.sf.m-basis.a.span

theorem AlgebraicCombinatorics.SymmetricFunctions.symm_eq_sum_coeff_monomialSymm {R : Type u_1} [CommSemiring R] {N : ℕ} (f : MvPolynomial (Fin N) R) (hf : f.IsSymmetric) (S : Finset (NPartition N)) (hS : ∀ (mu : NPartition N), NPartition.size mu ≤ f.totalDegree → mu ∈ S) : f = ∑ mu ∈ S, MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm mu.parts) f • monomialSymm mu

Any symmetric polynomial f can be written as f = ∑_μ ([x₁^{μ₁} x₂^{μ₂} ⋯ x_N^{μ_N}] f) m_μ (Theorem thm.sf.m-basis (b))

Label: thm.sf.m-basis.b

def AlgebraicCombinatorics.SymmetricFunctions.symmHomogeneous (N : ℕ) (R : Type u_2) [CommSemiring R] (n : ℕ) : Submodule R (MvPolynomial (Fin N) R)

The submodule of homogeneous symmetric polynomials of degree n. (Theorem thm.sf.m-basis (c))

𝒮_n = {homogeneous symmetric polynomials of degree n}

Label: thm.sf.m-basis.c

Equations

• AlgebraicCombinatorics.SymmetricFunctions.symmHomogeneous N R n = { carrier := {f : MvPolynomial (Fin N) R | f.IsSymmetric ∧ f.IsHomogeneous n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_isHomogeneous {R : Type u_1} [CommSemiring R] {N : ℕ} (mu : NPartition N) : (monomialSymm mu).IsHomogeneous (NPartition.size mu)

The monomial symmetric polynomial m_μ is homogeneous of degree |μ|.

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_homogeneous_spans {R : Type u_1} [CommSemiring R] {N : ℕ} (n : ℕ) (f : MvPolynomial (Fin N) R) : f ∈ symmHomogeneous N R n → f ∈ Submodule.span R (Set.range fun (mu : { nu : NPartition N // NPartition.size nu = n }) => monomialSymm ↑mu)

The monomial symmetric polynomials of size n span 𝒮_n. (Theorem thm.sf.m-basis (d), spanning part)

Label: thm.sf.m-basis.d.span

theorem AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_homogeneous_linearIndependent {R : Type u_1} [CommSemiring R] {N : ℕ} (n : ℕ) : LinearIndependent R fun (mu : { nu : NPartition N // NPartition.size nu = n }) => monomialSymm ↑mu

The monomial symmetric polynomials of size n are linearly independent. (Theorem thm.sf.m-basis (d), linear independence part)

This follows from the fact that no two m_μ share any monomials, and each m_μ contains at least one monomial.

Label: thm.sf.m-basis.d.indep

noncomputable def AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_basis_homogeneous {R : Type u_1} [CommSemiring R] {N : ℕ} (n : ℕ) : Module.Basis { nu : NPartition N // NPartition.size nu = n } R ↥(symmHomogeneous N R n)

The monomial symmetric polynomials of size n form a basis of 𝒮_n. (Theorem thm.sf.m-basis (d))

This combines linear independence (monomialSymm_homogeneous_linearIndependent) and spanning (monomialSymm_homogeneous_spans).

Label: thm.sf.m-basis.d

Equations

• AlgebraicCombinatorics.SymmetricFunctions.monomialSymm_basis_homogeneous n = Module.Basis.mk ⋯ ⋯