The Schur polynomial of a one-row shape

A Young diagram with at most one row has one cell in each of its columns, and a semistandard tableau of that shape is exactly a weakly increasing list of letters, one per column: the entries of a row increase weakly rightwards, and there is no column condition to satisfy. So a bounded tableau of a one-row shape is nothing but the multiset of the letters it uses, and its weight is the multiplicity function of that multiset. Summing over the tableaux therefore sums the monomial ∏ᵢ xᵢ ^ (multiplicity of i) over every multiset of letters of the right size, which is MvPolynomial.hsymm:

TauCeti.diagramSchurPoly N R μ = MvPolynomial.hsymm (Fin N) R μ.card for μ.colLen 0 ≤ 1.

For partitions this reads s_{(n)} = h_n, TauCeti.schurPoly_indiscrete, the shape (n) being Mathlib's Nat.Partition.indiscrete at the top of the dominance order: a single row of n cells for n > 0, and the empty diagram for n = 0. It is the 1 × 1 instance of the Jacobi--Trudi identity, whose general form expresses s_μ as a determinant of complete homogeneous symmetric polynomials, and the character-level shadow of 𝕊^{(n)}(V) = Symⁿ V. It is dual to TauCeti.schurPoly_ones, the one-column identity s_{(1ⁿ)} = e_n.

The identification runs through TauCeti.BoundedSSYT.rowMultisetEquiv, the bijection between the bounded tableaux of a one-row shape and the multisets of letters of size the number of columns. Both directions are explicit: a tableau is sent to the multiset TauCeti.BoundedSSYT.rowMultiset of the entries of its row, and a multiset is sent back to the tableau TauCeti.BoundedSSYT.ofRowMultiset that lists it in increasing order, along the sorted word Multiset.sort produces.

Unlike the one-column case, where the letters of a tableau are pairwise distinct and form a Finset, a row may repeat a letter, so the enumeration Finset.orderEmbOfFin is unavailable and the sorted word is what carries the construction. Its two characterising properties, that it is weakly increasing and that it has the right multiset of letters, determine it (List.Perm.eq_of_pairwise'), which is how the round trip from a tableau back to itself is proved.

Stability is another corollary: setting the last of n + 1 variables to 0 sends h_d in n + 1 variables to h_d in n variables (TauCeti.aeval_snoc_zero_hsymm), because it does so for every Schur polynomial (TauCeti.aeval_snoc_zero_diagramSchurPoly). The same holds for the integer-indexed TauCeti.hsymmInt (TauCeti.aeval_snoc_zero_hsymmInt).

Symmetry is a corollary rather than an input: the one-row case falls out of TauCeti.schurPoly_indiscrete and the symmetry of the complete homogeneous symmetric polynomials, without the Bender--Knuth involution that TauCeti.schurPoly_isSymmetric needs in general.

Main definitions

• TauCeti.BoundedSSYT.rowEntry: the letter a bounded tableau puts in a given column of its first row.
• TauCeti.BoundedSSYT.rowMultiset: the multiset of letters used by the first row of a bounded tableau.
• TauCeti.BoundedSSYT.ofRowMultiset: the one-row tableau listing a given multiset of letters in increasing order.
• TauCeti.BoundedSSYT.rowMultisetEquiv: the bijection between the bounded tableaux of a one-row shape and the multisets of letters of size the number of columns.

Main results

• TauCeti.BoundedSSYT.weight_eq_toFinsupp: the weight of a one-row tableau is the multiplicity function of the multiset of letters it uses.
• TauCeti.diagramSchurPoly_eq_hsymm_of_colLen_le_one: the Schur polynomial of a one-row shape is a complete homogeneous symmetric polynomial.
• TauCeti.schurPoly_indiscrete: s_{(n)} = h_n.
• TauCeti.aeval_snoc_zero_hsymm, TauCeti.aeval_snoc_zero_hsymmInt: stability of the complete homogeneous symmetric polynomials under setting the last variable to 0.

References

• W. Fulton, Young Tableaux, Section 2.2.
• I. G. Macdonald, Symmetric Functions and Hall Polynomials, Chapter I, Section 3, where s_{(n)} = h_n sits beside s_{(1ⁿ)} = e_n as the first examples of a Schur function.
• Schur--Weyl roadmap, Layer 7.

The first row of a bounded tableau

def TauCeti.BoundedSSYT.rowEntry {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) (j : Fin (μ.rowLen 0)) : Fin N

The letter a bounded tableau puts in column j of its first row. The shape enters only through the length μ.rowLen 0 of its first row, so this reads the first row of any bounded tableau; for a one-row shape it reads the whole tableau.

Equations

• T.rowEntry j = ⟨↑T 0 ↑j, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.rowEntry_val {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) (j : Fin (μ.rowLen 0)) : ↑(T.rowEntry j) = ↑T 0 ↑j

theorem TauCeti.BoundedSSYT.rowEntry_monotone {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : Monotone T.rowEntry

The first row of a bounded tableau increases weakly, entries increasing weakly rightwards along every row of a semistandard tableau.

def TauCeti.BoundedSSYT.rowMultiset {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : Multiset (Fin N)

The multiset of letters the first row of a bounded tableau uses, with multiplicity.

Equations

• T.rowMultiset = Multiset.map T.rowEntry Finset.univ.val

@[simp]

theorem TauCeti.BoundedSSYT.mem_rowMultiset {N : ℕ} {μ : YoungDiagram} {T : BoundedSSYT N μ} {x : Fin N} : x ∈ T.rowMultiset ↔ ∃ (j : Fin (μ.rowLen 0)), T.rowEntry j = x

A letter is used by the first row of a bounded tableau exactly when some column carries it.

@[simp]

theorem TauCeti.BoundedSSYT.card_rowMultiset {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : T.rowMultiset.card = μ.rowLen 0

The first row of a bounded tableau uses one letter per column, counted with multiplicity.

The weight of a one-row tableau

theorem TauCeti.BoundedSSYT.weight_apply_eq_count {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (T : BoundedSSYT N μ) (y : Fin N) : T.weight y = Multiset.count y T.rowMultiset

The weight of a one-row tableau counts the letters of its row: a letter is used as often as it occurs in the row.

theorem TauCeti.BoundedSSYT.weight_eq_toFinsupp {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (T : BoundedSSYT N μ) : T.weight = Multiset.toFinsupp T.rowMultiset

The weight of a one-row tableau is the multiplicity function of the letters of its row.

Recovering a one-row tableau from its letters

def TauCeti.BoundedSSYT.ofRowMultiset {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (s : Multiset (Fin N)) (hs : s.card = μ.rowLen 0) : BoundedSSYT N μ

The one-row tableau listing a given multiset of letters in increasing order, as a bounded tableau: the letters it uses come from the alphabet because they are letters of the alphabet.

Equations

• TauCeti.BoundedSSYT.ofRowMultiset h s hs = ⟨TauCeti.BoundedSSYT.rowTableau✝ h s hs, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.rowMultiset_ofRowMultiset {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (s : Multiset (Fin N)) (hs : s.card = μ.rowLen 0) : (ofRowMultiset h s hs).rowMultiset = s

Listing a multiset of letters along a row uses exactly those letters: the multiset of letters of TauCeti.BoundedSSYT.ofRowMultiset h s hs is s again.

@[simp]

theorem TauCeti.BoundedSSYT.ofRowMultiset_rowMultiset {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (T : BoundedSSYT N μ) : ofRowMultiset h T.rowMultiset ⋯ = T

A one-row tableau is determined by the letters it uses: relisting the multiset of letters of the row of T in increasing order recovers T.

def TauCeti.BoundedSSYT.rowMultisetEquiv {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) : BoundedSSYT N μ ≃ Sym (Fin N) μ.card

The bounded tableaux of a one-row shape are the multisets of letters of the right size: a tableau is the multiset of the letters of its row, and a multiset of letters is listed along the row in increasing order.

Equations

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

@[simp]

theorem TauCeti.BoundedSSYT.rowMultisetEquiv_apply_coe {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (T : BoundedSSYT N μ) : ↑((rowMultisetEquiv h) T) = T.rowMultiset

@[simp]

theorem TauCeti.BoundedSSYT.rowMultisetEquiv_symm_apply {N : ℕ} {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) (s : Sym (Fin N) μ.card) : (rowMultisetEquiv h).symm s = ofRowMultiset h ↑s ⋯

The inverse of rowMultisetEquiv lists a multiset of letters along the row in increasing order.

The Schur polynomial of a one-row shape

theorem TauCeti.diagramSchurPoly_eq_hsymm_of_colLen_le_one {N : ℕ} {R : Type u_1} [CommSemiring R] {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) : diagramSchurPoly N R μ = MvPolynomial.hsymm (Fin N) R μ.card

The Schur polynomial of a one-row shape is a complete homogeneous symmetric polynomial: the tableaux of that shape are the multisets of letters of size the number of columns, each contributing the monomial on the letters it uses.

@[simp]

theorem TauCeti.schurPoly_indiscrete {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] [DecidableEq σ] (n : ℕ) : schurPoly σ R (Nat.Partition.indiscrete n) = MvPolynomial.hsymm σ R n

The Schur polynomial of the partition (n) is the n-th complete homogeneous symmetric polynomial, s_{(n)} = h_n. The diagram of (n) has at most one row: it is a single row of n cells for n > 0, and empty for n = 0.

Stability

theorem TauCeti.aeval_snoc_zero_hsymm {R : Type u_1} [CommSemiring R] (n d : ℕ) : (MvPolynomial.aeval (Fin.snoc MvPolynomial.X 0)) (MvPolynomial.hsymm (Fin (n + 1)) R d) = MvPolynomial.hsymm (Fin n) R d

Stability of the complete homogeneous symmetric polynomials: setting the last of n + 1 variables to 0 turns h_d in n + 1 variables into h_d in n variables.

Not a simp lemma, for the reason recorded at TauCeti.aeval_snoc_zero_diagramSchurPoly.

theorem TauCeti.aeval_snoc_zero_hsymmInt {R : Type u_1} [CommSemiring R] (n : ℕ) (m : ℤ) : (MvPolynomial.aeval (Fin.snoc MvPolynomial.X 0)) (hsymmInt (Fin (n + 1)) R m) = hsymmInt (Fin n) R m

Stability of the integer-indexed complete homogeneous symmetric polynomials: setting the last of n + 1 variables to 0 turns h_m in n + 1 variables into h_m in n variables, for every integer m.