The Schur polynomial of a one-column shape

A Young diagram with at most one column has one cell in each of its rows, and a semistandard tableau of that shape is exactly a strictly increasing list of letters, one per row: the entries of a column increase strictly downwards, and there is no row condition to satisfy. So a bounded tableau of a one-column shape is nothing but the set of the letters it uses, and its weight is the indicator of that set. Summing over the tableaux therefore sums a squarefree monomial over every set of letters of the right size, which is MvPolynomial.esymm:

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

For partitions this reads s_{(1ⁿ)} = e_n, TauCeti.schurPoly_ones, the shape (1ⁿ) being the TauCeti.Nat.Partition.ones at the bottom of the dominance order. It is the 1 × 1 instance of the dual Jacobi--Trudi identity, whose general form expresses s_μ as a determinant of elementary symmetric polynomials, and the character-level shadow of 𝕊^{(1ⁿ)}(V) = ⋀ⁿ V.

The identification runs through TauCeti.BoundedSSYT.colFinsetEquiv, the bijection between the bounded tableaux of a one-column shape and the sets of letters of size the number of rows. Both directions are explicit: a tableau is sent to the set TauCeti.BoundedSSYT.colFinset of the entries of its column, and a set is sent back to the tableau TauCeti.BoundedSSYT.ofColFinset that lists it in increasing order, which is Finset.orderEmbOfFin.

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

Main definitions

• TauCeti.BoundedSSYT.colEntry: the letter a bounded tableau puts in a given row of its first column.
• TauCeti.BoundedSSYT.colFinset: the set of letters used by the first column of a bounded tableau.
• TauCeti.BoundedSSYT.ofColFinset: the one-column tableau listing a given set of letters in increasing order.
• TauCeti.BoundedSSYT.colFinsetEquiv: the bijection between the bounded tableaux of a one-column shape and the sets of letters of size the number of rows.

Main results

• TauCeti.BoundedSSYT.weight_eq_sum_single: the weight of a one-column tableau is the indicator of the set of letters it uses.
• TauCeti.diagramSchurPoly_eq_esymm_of_rowLen_le_one: the Schur polynomial of a one-column shape is an elementary symmetric polynomial.
• TauCeti.schurPoly_ones: s_{(1ⁿ)} = e_n.

References

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

The first column of a bounded tableau

def TauCeti.BoundedSSYT.colEntry {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) (i : Fin (μ.colLen 0)) : Fin N

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

Equations

• T.colEntry i = ⟨↑T (↑i) 0, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.colEntry_val {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) (i : Fin (μ.colLen 0)) : ↑(T.colEntry i) = ↑T (↑i) 0

theorem TauCeti.BoundedSSYT.colEntry_strictMono {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : StrictMono T.colEntry

The first column of a bounded tableau increases strictly, entries increasing strictly down every column of a semistandard tableau.

def TauCeti.BoundedSSYT.colFinset {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : Finset (Fin N)

The set of letters the first column of a bounded tableau uses.

Equations

• T.colFinset = Finset.image T.colEntry Finset.univ

@[simp]

theorem TauCeti.BoundedSSYT.mem_colFinset {N : ℕ} {μ : YoungDiagram} {T : BoundedSSYT N μ} {x : Fin N} : x ∈ T.colFinset ↔ ∃ (i : Fin (μ.colLen 0)), T.colEntry i = x

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

@[simp]

theorem TauCeti.BoundedSSYT.card_colFinset {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : T.colFinset.card = μ.colLen 0

The first column of a bounded tableau uses one letter per row, its entries being distinct.

theorem TauCeti.BoundedSSYT.orderEmbOfFin_colFinset {N : ℕ} {μ : YoungDiagram} (T : BoundedSSYT N μ) : ⇑(T.colFinset.orderEmbOfFin ⋯) = T.colEntry

The first column of a bounded tableau lists its letters in increasing order: it is the monotone enumeration Finset.orderEmbOfFin of the set of letters it uses.

The weight of a one-column tableau

theorem TauCeti.BoundedSSYT.weight_eq_sum_single {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (T : BoundedSSYT N μ) : T.weight = ∑ x ∈ T.colFinset, Finsupp.single x 1

The weight of a one-column tableau is the indicator of the set of letters it uses: every letter it uses is used exactly once, one column having at most one cell per row.

Recovering a one-column tableau from its letters

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

The one-column tableau listing a given set 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.ofColFinset h s hs = ⟨TauCeti.BoundedSSYT.colTableau✝ h s hs, ⋯⟩

theorem TauCeti.BoundedSSYT.ofColFinset_apply {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (s : Finset (Fin N)) (hs : s.card = μ.colLen 0) (i j : ℕ) : ↑(ofColFinset h s hs) i j = if hij : i < μ.colLen 0 ∧ j = 0 then ↑((s.orderEmbOfFin hs) ⟨i, ⋯⟩) else 0

@[simp]

theorem TauCeti.BoundedSSYT.colEntry_ofColFinset {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (s : Finset (Fin N)) (hs : s.card = μ.colLen 0) (i : Fin (μ.colLen 0)) : (ofColFinset h s hs).colEntry i = (s.orderEmbOfFin hs) i

@[simp]

theorem TauCeti.BoundedSSYT.colFinset_ofColFinset {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (s : Finset (Fin N)) (hs : s.card = μ.colLen 0) : (ofColFinset h s hs).colFinset = s

@[simp]

theorem TauCeti.BoundedSSYT.ofColFinset_colFinset {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (T : BoundedSSYT N μ) : ofColFinset h T.colFinset ⋯ = T

def TauCeti.BoundedSSYT.colFinsetEquiv {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) : BoundedSSYT N μ ≃ { s : Finset (Fin N) // s.card = μ.colLen 0 }

The bounded tableaux of a one-column shape are the sets of letters of the right size: a tableau is the set of the letters of its column, and a set of letters is listed down the column in increasing order.

Equations

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

@[simp]

theorem TauCeti.BoundedSSYT.colFinsetEquiv_apply_coe {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (T : BoundedSSYT N μ) : ↑((colFinsetEquiv h) T) = T.colFinset

@[simp]

theorem TauCeti.BoundedSSYT.colFinsetEquiv_symm_apply {N : ℕ} {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) (s : { s : Finset (Fin N) // s.card = μ.colLen 0 }) : (colFinsetEquiv h).symm s = ofColFinset h ↑s ⋯

The inverse of colFinsetEquiv lists a set of letters down the column in increasing order.

The Schur polynomial of a one-column shape

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

The Schur polynomial of a one-column shape is an elementary symmetric polynomial: the tableaux of that shape are the sets of letters of size the number of rows, each contributing the squarefree monomial on the letters it uses.

@[simp]

theorem TauCeti.schurPoly_ones {R : Type u_1} [CommSemiring R] {σ : Type u_2} [Fintype σ] (n : ℕ) : schurPoly σ R (Nat.Partition.ones n) = MvPolynomial.esymm σ R n

The Schur polynomial of the one-column partition (1ⁿ) is the n-th elementary symmetric polynomial, s_{(1ⁿ)} = e_n.