Gelfand-Tsetlin patterns are semistandard Young tableaux

A Gelfand-Tsetlin pattern whose top row is a shape μ records a chain of shapes

∅ = ν⁰ ⊆ ν¹ ⊆ ⋯ ⊆ νⁿ = μ,

row j being the row-length sequence of νʲ; consecutive shapes differ by a horizontal strip because consecutive rows interlace. Such a chain is the same thing as a semistandard Young tableau of shape μ with entries in {0, …, n - 1}: the cells carrying the entry j are exactly those of νʲ⁺¹ and not of νʲ. This file builds that bijection.

Both directions are counting maps, and both rest on the same principle: a downward closed predicate on ℕ cuts an initial segment out of Finset.range N, so membership in the segment is decided by comparison with its cardinality. Concretely, the tableau attached to a pattern P has

T i c = #{j < n | λᵢ,ⱼ₊₁ ≤ c},

the number of rows of P that do not yet reach past c: for a cell (i, c) of μ this is one less than the number of the first shape of the chain that contains it, so that the cells carrying the entry j are exactly those of νʲ⁺¹ and not of νʲ. The pattern attached to a tableau T has λᵢ,ⱼ the number of cells (i, c) of μ with T i c < j, that is, the length of row i of the shape filled by the entries below j. The interlacing inequalities and the semistandardness conditions are exchanged by these two formulas, and the two maps are mutually inverse.

Nonnegativity of the entries is not assumed on TauCeti.GTPattern, which admits the determinant-twisted patterns; it is a consequence of the top row being a shape, since every entry dominates a top-row entry (TauCeti.GTPattern.entry_nonneg). Only in this polynomial regime is there a tableau to speak of.

Main definitions

• TauCeti.GTPattern.tableauEntry and TauCeti.GTPattern.toTableau: the tableau entry T i c read off a pattern, and the semistandard Young tableau it assembles.
• SemistandardYoungTableau.patternEntry and SemistandardYoungTableau.toGTPattern: the pattern read off a tableau.
• TauCeti.gtPatternEquivSSYT: the bijection, between the patterns with n rows and top row the shape μ and the semistandard Young tableaux of shape μ with entries below n, that is, TauCeti.BoundedSSYT n μ.

Main results

• TauCeti.GTPattern.lt_tableauEntry_iff and SemistandardYoungTableau.lt_card_filter_rowLen_iff: the two counting maps are decided by the pattern entries, respectively by the tableau entries. Everything else is read off these two comparisons.
• TauCeti.card_gtPattern_topRow_eq_card_ssyt: the patterns with a given top row are as many as the semistandard tableaux of the corresponding shape with bounded entries, both counts being finite by TauCeti.GTPattern.finite_topRow_eq and TauCeti.finite_boundedSSYT.

Implementation notes

With the bound ∀ i j, T i j < n on every entry of the tableau, the bijection fails in exactly one case: for n = 0 and μ = ⊥ there is one (empty) pattern but no tableau at all, because the bound also constrains the entries off μ, which vanish. The bound is therefore imposed on the cells of μ, where it is the intended condition; whenever μ is nonempty the two readings agree, since a nonempty shape forces n ≠ 0.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), §15.3.

Initial segments cut out by a downward closed predicate

Patterns whose top row is a shape

theorem TauCeti.GTPattern.entry_top_eq {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) (i : ℕ) : P i n = ↑(μ.rowLen i)

The top row of a pattern whose top row is the shape μ is the row-length sequence of μ at every index: past n both sides vanish, because μ has at most n rows.

From a pattern to a tableau

def TauCeti.GTPattern.tableauEntry {n : ℕ} (P : GTPattern n) (i c : ℕ) : ℕ

The (i, c) entry of the tableau attached to a Gelfand-Tsetlin pattern: the number of rows j < n of the pattern whose i-th entry is at most c. The counted rows form an initial segment, so when some row v < n has c < λᵢ,ᵥ₊₁ the count is the least such v: the cell (i, c) first appears in the shape νᵛ⁺¹ of the chain recorded by the pattern, one step further along the chain than the value v carried by the cell. When no row does, every row is counted and the entry is n.

@[simp]

theorem TauCeti.GTPattern.tableauEntry_def {n : ℕ} (P : GTPattern n) (i c : ℕ) : P.tableauEntry i c = {j ∈ Finset.range n | P i (j + 1) ≤ ↑c}.card

The tableau entry of a pattern, unfolded: the count of the rows j < n whose i-th entry is at most c. The body of TauCeti.GTPattern.tableauEntry is not exposed, so this is how the count is reached.

theorem TauCeti.GTPattern.lt_tableauEntry_iff {n : ℕ} (P : GTPattern n) {i c j : ℕ} : j < P.tableauEntry i c ↔ j < n ∧ P i (j + 1) ≤ ↑c

The tableau entry, read off the pattern: j < T i c exactly when j < n and the i-th entry of row j + 1 is at most c. The i-th entries of a pattern increase weakly with the row index on the informative cells and vanish on the rest, where the bound holds anyway since c is a natural number, so the condition is downward closed in j and the count is an initial segment.

theorem TauCeti.GTPattern.tableauEntry_lt {n : ℕ} (P : GTPattern n) {i c : ℕ} (hc : ↑c < P i n) : P.tableauEntry i c < n

Tableau entries are bounded by the number of rows of the pattern: a cell strictly inside the top row is reached before the last shape of the chain.

theorem TauCeti.GTPattern.tableauEntry_mono {n : ℕ} (P : GTPattern n) (i : ℕ) {c c' : ℕ} (h : c ≤ c') : P.tableauEntry i c ≤ P.tableauEntry i c'

Tableau entries increase weakly along a row.

theorem TauCeti.GTPattern.tableauEntry_lt_tableauEntry_succ {n : ℕ} (P : GTPattern n) {i c : ℕ} (hlt : P.tableauEntry i c < n) : P.tableauEntry i c < P.tableauEntry (i + 1) c

Tableau entries increase strictly down a column, one step: the count m for row i is beaten by the count for row i + 1, because the second interlacing inequality carries each of the m rows witnessing the bound for row i one step up, while row 1 supplies a further witness.

theorem TauCeti.GTPattern.tableauEntry_lt_tableauEntry {n : ℕ} (P : GTPattern n) {c i₁ i₂ : ℕ} : i₁ < i₂ → (∀ (i : ℕ), i₁ ≤ i → i < i₂ → P.tableauEntry i c < n) → P.tableauEntry i₁ c < P.tableauEntry i₂ c

Tableau entries increase strictly down a column. Only the rows i₁ ≤ i < i₂ that the chain of one-step comparisons passes through need to be bounded.

def TauCeti.GTPattern.toTableau {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) : SemistandardYoungTableau μ

The semistandard Young tableau of a Gelfand-Tsetlin pattern whose top row is the shape μ: the cell (i, c) carries the entry j for which νʲ⁺¹ is the first shape in the chain that contains it, one less than the number of that shape.

@[simp]

theorem TauCeti.GTPattern.toTableau_apply {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) (i c : ℕ) : (P.toTableau hμ hP) i c = if (i, c) ∈ μ then P.tableauEntry i c else 0

The tableau of a pattern, unfolded: off μ the entry vanishes, and on μ it is the count TauCeti.GTPattern.tableauEntry.

theorem TauCeti.GTPattern.toTableau_apply_of_mem {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) {i c : ℕ} (h : (i, c) ∈ μ) : (P.toTableau hμ hP) i c = P.tableauEntry i c

On a cell of μ the tableau of a pattern is the count TauCeti.GTPattern.tableauEntry.

theorem TauCeti.GTPattern.toTableau_lt {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) {i c : ℕ} (h : (i, c) ∈ μ) : (P.toTableau hμ hP) i c < n

The tableau of a pattern with n rows has entries below n on the cells of its shape.

theorem TauCeti.GTPattern.toTableau_lt_iff {n : ℕ} {μ : YoungDiagram} (P : GTPattern n) (hμ : μ.colLen 0 ≤ n) (hP : ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i)) {i c j : ℕ} (hj : j ≤ n) (hc : (i, c) ∈ μ) : (P.toTableau hμ hP) i c < j ↔ ↑c < P i j

The defining comparison for the tableau of a pattern: the entry at a cell of μ is below j exactly when the i-th entry of row j of the pattern runs past c.

From a tableau to a pattern

def SemistandardYoungTableau.patternEntry {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n i j : ℕ) : ℤ

The (i, j) entry of the pattern attached to a semistandard Young tableau, as a pattern with n rows: for j ≤ n it is the number of cells of row i of μ whose entry is below j, that is, the length of row i of the shape filled by the entries < j. Past the top row, n < j, the entry is forced to 0, as a pattern with n rows carries no data there.

@[simp]

theorem SemistandardYoungTableau.patternEntry_def {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n i j : ℕ) : T.patternEntry n i j = if n < j then 0 else ↑{c ∈ Finset.range (μ.rowLen i) | T i c < j}.card

The pattern entry of a tableau, unfolded: 0 past the top row, and otherwise the count of the cells of row i of μ carrying an entry below j. The body of SemistandardYoungTableau.patternEntry is not exposed, so this is how the count is reached.

@[simp]

theorem SemistandardYoungTableau.lt_card_filter_rowLen_iff {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j c : ℕ} : c < {c' ∈ Finset.range (μ.rowLen i) | T i c' < j}.card ↔ c < μ.rowLen i ∧ T i c < j

The pattern entry, read off the tableau: c is counted in row j of the i-th row exactly when (i, c) is a cell of μ carrying an entry below j. The rows of a tableau increase weakly, so the condition is downward closed in c.

def SemistandardYoungTableau.toGTPattern {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n : ℕ) : TauCeti.GTPattern n

The Gelfand-Tsetlin pattern of a semistandard Young tableau, with n rows: row j is the row-length sequence of the shape filled by the entries < j. No bound on the entries is needed to build the pattern; a bound is what makes its top row the whole of μ (SemistandardYoungTableau.topRow_toGTPattern).

@[simp]

theorem SemistandardYoungTableau.toGTPattern_apply {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n i j : ℕ) : (T.toGTPattern n) i j = T.patternEntry n i j

The pattern of a tableau, unfolded.

theorem SemistandardYoungTableau.topRow_toGTPattern {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n : ℕ) (hT : ∀ (i c : ℕ), (i, c) ∈ μ → T i c < n) (i : Fin n) : (T.toGTPattern n).topRow i = ↑(μ.rowLen ↑i)

The top row of the pattern of a tableau of shape μ is the row-length sequence of μ: every entry lies below n, so the last shape of the chain is μ itself.

theorem SemistandardYoungTableau.toGTPattern_succ_le_iff {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (n : ℕ) {i c j : ℕ} (hj : j < n) (hc : (i, c) ∈ μ) : (T.toGTPattern n) i (j + 1) ≤ ↑c ↔ j < T i c

The defining comparison for the pattern of a tableau: the i-th entry of row j + 1 is at most c exactly when the cell (i, c) carries an entry above j.

The bijection

def TauCeti.gtPatternEquivSSYT (n : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n) : { P : GTPattern n // ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i) } ≃ BoundedSSYT n μ

Gelfand-Tsetlin patterns are semistandard Young tableaux. For a shape μ with at most n rows, the patterns with n rows and top row μ correspond to the semistandard Young tableaux of shape μ whose entries lie in {0, …, n - 1}: row j of the pattern is the row-length sequence of the shape filled by the entries below j, and the cell (i, c) of the tableau carries the number of rows of the pattern whose i-th entry does not yet run past c, one less than the index of the first row that does.

Together with the count of the patterns with a given top row, this is the tableau reading of the Gelfand-Tsetlin basis of an irreducible polynomial representation of GL n.

@[simp]

theorem TauCeti.gtPatternEquivSSYT_apply_coe (n : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n) (P : { P : GTPattern n // ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i) }) : ↑((gtPatternEquivSSYT n μ hμ) P) = (↑P).toTableau hμ ⋯

The bijection sends a pattern to the tableau TauCeti.GTPattern.toTableau it names.

@[simp]

theorem TauCeti.gtPatternEquivSSYT_symm_apply_coe (n : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n) (T : BoundedSSYT n μ) : ↑((gtPatternEquivSSYT n μ hμ).symm T) = (↑T).toGTPattern n

The inverse bijection sends a tableau to the pattern SemistandardYoungTableau.toGTPattern it names.

theorem TauCeti.card_gtPattern_topRow_eq_card_ssyt (n : ℕ) (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n) : Nat.card { P : GTPattern n // ∀ (i : Fin n), P.topRow i = ↑(μ.rowLen ↑i) } = Nat.card (BoundedSSYT n μ)

The pattern count is the tableau count: the patterns with top row the shape μ are as many as the semistandard Young tableaux of shape μ with entries below n. This is the form in which the bijection feeds the Gelfand-Tsetlin dimension count.