Determinant shifts of Gelfand-Tsetlin patterns

Tensoring a rational representation of GL n by a power of the determinant adds the same integer to every component of its highest weight. On a Gelfand-Tsetlin pattern the corresponding operation adds that integer to every entry in the triangular array. This file constructs that translation as an equivalence and uses it to reduce patterns over an arbitrary dominant weight to the polynomial case.

For a dominant weight l of nonzero rank, subtracting its last entry gives the polynomial weight l.shift (-l.detShift), whose Young diagram is l.detShiftShape. A weight of rank zero has no last entry; there TauCeti.DominantWeight.detShift is 0 and the normalization does nothing, so the rank-zero case needs no separate treatment below. The equivalence TauCeti.GTPattern.detShiftEquivBoundedSSYT therefore identifies the patterns with top weight l with the bounded semistandard Young tableaux of that normalized shape. It is the rational-weight bridge between the Gelfand-Tsetlin pattern count and the existing pattern-tableau correspondence; the determinant twist changes no pattern-fiber cardinality.

In the entrywise additive monoid of patterns the shift by m is addition of the constant pattern TauCeti.GTPattern.const n m, and every pattern becomes a polynomial pattern, one with nonnegative entries, after a shift by a natural number.

Main definitions

• TauCeti.GTPattern.shift: add an integer to every informative entry of a pattern.
• TauCeti.GTPattern.shiftEquiv: translation of all patterns by a fixed integer.
• TauCeti.GTPattern.shiftTopWeightEquiv: translation between the fibers over l and l.shift m.
• TauCeti.GTPattern.detShiftEquivBoundedSSYT: patterns over an arbitrary dominant weight are equivalent to bounded semistandard tableaux of its determinant-normalized shape.

Main results

• TauCeti.GTPattern.topWeight_shift: shifting a pattern shifts its top weight.
• TauCeti.GTPattern.card_topWeight_shift: determinant translation preserves the pattern count.
• TauCeti.GTPattern.card_topWeight_eq_card_boundedSSYT_detShiftShape: the corresponding pattern and tableau fibers have the same cardinality.
• TauCeti.GTPattern.shift_eq_add_const: the determinant shift by m adds const n m.
• TauCeti.GTPattern.exists_zero_le_shift: every pattern becomes nonnegative after a determinant shift by a natural number.

References

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

Translation of patterns

def TauCeti.GTPattern.shift {n : ℕ} (P : GTPattern n) (m : ℤ) : GTPattern n

Add m to every informative entry of a Gelfand-Tsetlin pattern. Entries outside the triangle remain zero, so the representation of a pattern by an unrestricted function stays extensional.

theorem TauCeti.GTPattern.shift_apply {n : ℕ} (P : GTPattern n) (m : ℤ) (i j : ℕ) : (P.shift m) i j = if i < j ∧ j ≤ n then P i j + m else 0

The value of a shifted pattern before deciding whether the entry is informative.

@[simp]

theorem TauCeti.GTPattern.shift_apply_of_lt_of_le {n : ℕ} (P : GTPattern n) (m : ℤ) {i j : ℕ} (hij : i < j) (hj : j ≤ n) : (P.shift m) i j = P i j + m

On an informative cell, shifting a pattern adds the shift to the entry.

@[simp]

theorem TauCeti.GTPattern.shift_apply_of_not_lt_le {n : ℕ} (P : GTPattern n) (m : ℤ) {i j : ℕ} (h : ¬(i < j ∧ j ≤ n)) : (P.shift m) i j = 0

Outside the triangular array, a shifted pattern still has entry zero.

@[simp]

theorem TauCeti.GTPattern.shift_zero {n : ℕ} (P : GTPattern n) : P.shift 0 = P

Shifting by zero does not change a Gelfand-Tsetlin pattern.

@[simp]

theorem TauCeti.GTPattern.shift_shift {n : ℕ} (P : GTPattern n) (m m' : ℤ) : (P.shift m).shift m' = P.shift (m + m')

Successive shifts add their translation parameters.

def TauCeti.GTPattern.shiftEquiv (n : ℕ) (m : ℤ) : GTPattern n ≃ GTPattern n

Translation by m is a bijection on Gelfand-Tsetlin patterns, with inverse translation by -m.

@[simp]

theorem TauCeti.GTPattern.shiftEquiv_apply (n : ℕ) (m : ℤ) (P : GTPattern n) : (shiftEquiv n m) P = P.shift m

@[simp]

theorem TauCeti.GTPattern.shiftEquiv_symm_apply (n : ℕ) (m : ℤ) (P : GTPattern n) : (shiftEquiv n m).symm P = P.shift (-m)

Top weights and determinant normalization

@[simp]

theorem TauCeti.GTPattern.topRow_shift {n : ℕ} (P : GTPattern n) (m : ℤ) : (P.shift m).topRow = fun (i : Fin n) => P.topRow i + m

Translating every entry translates the top row by the same integer.

@[simp]

theorem TauCeti.GTPattern.topWeight_shift {n : ℕ} (P : GTPattern n) (m : ℤ) : (P.shift m).topWeight = P.topWeight.shift m

Translating every entry of a pattern translates its top weight, exactly as tensoring the corresponding representation by a determinant power translates its highest weight.

def TauCeti.GTPattern.shiftTopWeightEquiv {n : ℕ} (l : DominantWeight n) (m : ℤ) : { P : GTPattern n // P.topWeight = l } ≃ { P : GTPattern n // P.topWeight = l.shift m }

Shifting every pattern entry by m identifies the patterns of top weight l with the patterns of top weight l.shift m.

@[simp]

theorem TauCeti.GTPattern.shiftTopWeightEquiv_apply_coe {n : ℕ} (l : DominantWeight n) (m : ℤ) (P : { P : GTPattern n // P.topWeight = l }) : ↑((shiftTopWeightEquiv l m) P) = (↑P).shift m

@[simp]

theorem TauCeti.GTPattern.shiftTopWeightEquiv_symm_apply_coe {n : ℕ} (l : DominantWeight n) (m : ℤ) (P : { P : GTPattern n // P.topWeight = l.shift m }) : ↑((shiftTopWeightEquiv l m).symm P) = (↑P).shift (-m)

The inverse of TauCeti.GTPattern.shiftTopWeightEquiv subtracts the same translation from every entry.

theorem TauCeti.GTPattern.card_topWeight_shift {n : ℕ} (l : DominantWeight n) (m : ℤ) : Nat.card { P : GTPattern n // P.topWeight = l.shift m } = Nat.card { P : GTPattern n // P.topWeight = l }

A determinant translation does not change the number of Gelfand-Tsetlin patterns over a top weight.

noncomputable def TauCeti.GTPattern.detShiftEquivBoundedSSYT {n : ℕ} (l : DominantWeight n) : { P : GTPattern n // P.topWeight = l } ≃ BoundedSSYT n l.detShiftShape

Determinant normalization of Gelfand-Tsetlin patterns. Patterns whose top weight is an arbitrary dominant weight l correspond to bounded semistandard tableaux of the Young diagram of l - l.detShift. The first step subtracts l.detShift from every pattern entry; the existing pattern-tableau equivalence then applies to the resulting polynomial top weight.

@[simp]

theorem TauCeti.GTPattern.detShiftEquivBoundedSSYT_apply_coe {n : ℕ} (l : DominantWeight n) (P : { P : GTPattern n // P.topWeight = l }) : ↑((detShiftEquivBoundedSSYT l) P) = ((↑P).shift (-l.detShift)).toTableau ⋯ ⋯

Determinant normalization sends a pattern to the tableau of the pattern shifted to polynomial top weight.

@[simp]

theorem TauCeti.GTPattern.detShiftEquivBoundedSSYT_symm_apply_coe {n : ℕ} (l : DominantWeight n) (T : BoundedSSYT n l.detShiftShape) : ↑((detShiftEquivBoundedSSYT l).symm T) = ((↑T).toGTPattern n).shift l.detShift

The inverse determinant-normalization equivalence shifts the tableau's polynomial pattern back by the determinant weight.

theorem TauCeti.GTPattern.card_topWeight_eq_card_boundedSSYT_detShiftShape {n : ℕ} (l : DominantWeight n) : Nat.card { P : GTPattern n // P.topWeight = l } = Nat.card (BoundedSSYT n l.detShiftShape)

The rational pattern count reduces to the polynomial tableau count. The Gelfand-Tsetlin patterns over any dominant weight l are as numerous as the bounded semistandard tableaux of the determinant-normalized shape l.detShiftShape.

Determinant shifts as additions of constant patterns

theorem TauCeti.GTPattern.shift_eq_add_const {n : ℕ} (P : GTPattern n) (m : ℤ) : P.shift m = P + const n m

The determinant shift is addition of a constant pattern.

theorem TauCeti.GTPattern.exists_zero_le_shift {n : ℕ} (P : GTPattern n) : ∃ (m : ℕ), 0 ≤ P.shift ↑m

Every pattern is a polynomial pattern up to a determinant shift: some shift by a natural number makes all of its entries nonnegative.