Dominant weights for the general linear group

The irreducible rational representations of GL n are indexed by the weakly decreasing integer sequences λ₁ ≥ ⋯ ≥ λₙ, the dominant weights of the diagonal torus. This file builds that index type and its dictionary with Young diagrams, before any representation is attached to a weight: the combinatorics is exactly the bookkeeping that separates the polynomial representations from the general rational ones.

Two facts organize the file. First, the dominant weights with nonnegative entries — the TauCeti.DominantWeight.IsPolynomial ones — are precisely the Young diagrams with at most n rows, an equivalence TauCeti.shapeEquivPolynomialWeight. Second, every dominant weight is a determinant twist of a polynomial one: writing m = λₙ for its last entry (TauCeti.DominantWeight.detShift) and subtracting it leaves a weight with nonnegative entries whose own last entry vanishes, so its Young diagram TauCeti.DominantWeight.detShiftShape has at most n - 1 rows, and λ is recovered from that diagram by shifting back by m. The vanishing last entry is what makes the pair (m, μ) unique: without the row bound the same λ is μ + m·(1, …, 1) for many pairs. Downstream this is the statement that a rational irreducible is det^m tensored with a polynomial one.

A third fact ties the weights to the symmetric group acting on ℤⁿ by permuting coordinates: every orbit of that action contains exactly one dominant weight (TauCeti.existsUnique_dominantWeight), the weakly decreasing rearrangement TauCeti.dominantWeightOf of any of its members. So a dominant weight is the canonical representative of its orbit; that these representatives index the irreducibles of GL n is the highest-weight classification, which is not proved here.

The last entry λₙ is read through the dedicated accessor TauCeti.DominantWeight.detShift, which is 0 for n = 0, so that the empty weight needs no special casing at the use sites. Being an accessor rather than a shift, it is compatible with TauCeti.DominantWeight.shift only for a nonempty weight (TauCeti.DominantWeight.detShift_shift).

Main definitions

• TauCeti.DominantWeight: the weakly decreasing sequences Fin n → ℤ.
• TauCeti.DominantWeight.shift: translating a weight by an integer multiple of (1, …, 1).
• TauCeti.DominantWeight.detShift: the last entry λₙ, the determinant-twist exponent.
• TauCeti.DominantWeight.IsPolynomial: having nonnegative entries.
• TauCeti.DominantWeight.shape and TauCeti.weightOfShape: the two directions of the dictionary between weights and Young diagrams.
• TauCeti.DominantWeight.detShiftShape: the Young diagram of the polynomial part λ - λₙ.
• TauCeti.dominantSort and TauCeti.dominantWeightOf: the permutation sorting an arbitrary weight into weakly decreasing order, and the dominant weight it produces.

Main results

• TauCeti.DominantWeight.isPolynomial_iff_zero_le_detShift: a weight is polynomial as soon as its last entry is nonnegative.
• TauCeti.shapeEquivPolynomialWeight: the Young diagrams with at most n rows are the polynomial dominant weights of GL n.
• TauCeti.DominantWeight.shift_weightOfShape_detShiftShape: the determinant twist λ = μ + λₙ·(1, …, 1) with μ = detShiftShape λ, together with TauCeti.DominantWeight.colLen_zero_detShiftShape_le_pred, which bounds μ by n - 1 rows.
• TauCeti.DominantWeight.eq_detShift_and_eq_detShiftShape: that decomposition is the only one whose diagram has at most n - 1 rows.
• TauCeti.DominantWeight.detShiftShape_eq_detShiftShape_iff: the polynomial part is a complete invariant of a weight modulo the constant weights, and TauCeti.DominantWeight.detShiftShape_weightOfShape shows every diagram with at most n - 1 rows occurs as one.
• TauCeti.existsUnique_dominantWeight: each orbit of the symmetric group permuting the coordinates of ℤⁿ contains exactly one dominant weight.

References

• Classical groups roadmap, Layer 3, “Dominant weights”, and Layer 4, “The rational character is Laurent”.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

@[reducible, inline]

abbrev TauCeti.DominantWeight (n : ℕ) : Type

A dominant weight for GL n: a weakly decreasing sequence λ₁ ≥ ⋯ ≥ λₙ of integers. These index the irreducible rational representations of GL n; the ones with nonnegative entries (TauCeti.DominantWeight.IsPolynomial) index the polynomial ones.

Equations

• TauCeti.DominantWeight n = { l : Fin n → ℤ // Antitone l }

theorem TauCeti.DominantWeight.antitone {n : ℕ} (l : DominantWeight n) : Antitone ↑l

def TauCeti.DominantWeight.shift {n : ℕ} (l : DominantWeight n) (m : ℤ) : DominantWeight n

Translating a dominant weight by m·(1, …, 1). On representations this is tensoring with the m-th power of the determinant.

Equations

• l.shift m = ⟨fun (i : Fin n) => ↑l i + m, ⋯⟩

@[simp]

theorem TauCeti.DominantWeight.shift_apply {n : ℕ} (l : DominantWeight n) (m : ℤ) (i : Fin n) : ↑(l.shift m) i = ↑l i + m

@[simp]

theorem TauCeti.DominantWeight.shift_zero {n : ℕ} (l : DominantWeight n) : l.shift 0 = l

@[simp]

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

def TauCeti.DominantWeight.detShift {n : ℕ} : DominantWeight n → ℤ

The determinant-twist exponent of a dominant weight: its last entry λₙ, and 0 for the empty weight.

Equations

• x_2.detShift = 0
• l.detShift = ↑l (Fin.last n)

@[simp]

theorem TauCeti.DominantWeight.detShift_eq_zero_of_isEmpty (l : DominantWeight 0) : l.detShift = 0

@[simp]

theorem TauCeti.DominantWeight.detShift_succ {n : ℕ} (l : DominantWeight (n + 1)) : l.detShift = ↑l (Fin.last n)

theorem TauCeti.DominantWeight.detShift_le {n : ℕ} (l : DominantWeight n) (i : Fin n) : l.detShift ≤ ↑l i

The determinant-twist exponent is the smallest entry of a dominant weight.

@[simp]

theorem TauCeti.DominantWeight.detShift_shift {n : ℕ} (l : DominantWeight (n + 1)) (m : ℤ) : (l.shift m).detShift = l.detShift + m

Shifting a nonempty dominant weight shifts its last entry. The hypothesis is not decoration: for n = 0 the accessor is 0 by convention and the identity fails.

def TauCeti.DominantWeight.IsPolynomial {n : ℕ} (l : DominantWeight n) : Prop

A dominant weight is polynomial when all its entries are nonnegative. These are the weights of the representations occurring in tensor powers of the standard representation, as opposed to the general rational ones, which need a negative power of the determinant.

Equations

• l.IsPolynomial = ∀ (i : Fin n), 0 ≤ ↑l i

theorem TauCeti.DominantWeight.isPolynomial_iff_zero_le_detShift {n : ℕ} (l : DominantWeight n) : l.IsPolynomial ↔ 0 ≤ l.detShift

Since a dominant weight decreases, only its last entry has to be tested for polynomiality. This is not a simp lemma: rewriting IsPolynomial away would put the simp lemmas whose statement or hypothesis mentions it — TauCeti.isPolynomial_weightOfShape and TauCeti.weightOfShape_shape — out of simp normal form.

theorem TauCeti.DominantWeight.isPolynomial_shift_neg_detShift {n : ℕ} (l : DominantWeight n) : (l.shift (-l.detShift)).IsPolynomial

Subtracting its last entry makes any dominant weight polynomial.

theorem TauCeti.DominantWeight.toNat_antitone {n : ℕ} (l : DominantWeight n) : Antitone fun (i : Fin n) => (↑l i).toNat

The entries of a dominant weight, truncated to ℕ, are still weakly decreasing.

def TauCeti.DominantWeight.shape {n : ℕ} (l : DominantWeight n) : YoungDiagram

The Young diagram of a dominant weight: its i-th row has length λᵢ. Negative entries are truncated to 0, so this reads off the intended diagram exactly on the polynomial weights, where TauCeti.DominantWeight.natCast_rowLen_shape recovers the entries.

Equations

• l.shape = YoungDiagram.ofRowLensFin (fun (i : Fin n) => (↑l i).toNat) ⋯

@[simp]

theorem TauCeti.DominantWeight.rowLen_shape {n : ℕ} (l : DominantWeight n) (i : Fin n) : l.shape.rowLen ↑i = (↑l i).toNat

@[simp]

theorem TauCeti.DominantWeight.rowLen_shape_eq_zero_of_le {n : ℕ} (l : DominantWeight n) {i : ℕ} (hi : n ≤ i) : l.shape.rowLen i = 0

@[simp]

theorem TauCeti.DominantWeight.colLen_zero_shape_le {n : ℕ} (l : DominantWeight n) : l.shape.colLen 0 ≤ n

theorem TauCeti.DominantWeight.natCast_rowLen_shape {n : ℕ} {l : DominantWeight n} (hl : l.IsPolynomial) (i : Fin n) : ↑(l.shape.rowLen ↑i) = ↑l i

On a polynomial weight the row lengths of its Young diagram are the entries themselves.

theorem TauCeti.DominantWeight.natCast_card_shape {n : ℕ} {l : DominantWeight n} (hl : l.IsPolynomial) : ↑l.shape.card = ∑ i : Fin n, ↑l i

The Young diagram of a polynomial weight has ∑ λᵢ cells.

def TauCeti.weightOfShape (n : ℕ) (μ : YoungDiagram) : DominantWeight n

The dominant weight read off the first n row lengths of a Young diagram. It is the weight intended by μ exactly when μ has at most n rows; a taller diagram is silently truncated.

Equations

• TauCeti.weightOfShape n μ = ⟨fun (i : Fin n) => ↑(μ.rowLen ↑i), ⋯⟩

@[simp]

theorem TauCeti.weightOfShape_apply (n : ℕ) (μ : YoungDiagram) (i : Fin n) : ↑(weightOfShape n μ) i = ↑(μ.rowLen ↑i)

@[simp]

theorem TauCeti.isPolynomial_weightOfShape (n : ℕ) (μ : YoungDiagram) : (weightOfShape n μ).IsPolynomial

@[simp]

theorem TauCeti.shape_weightOfShape {n : ℕ} {μ : YoungDiagram} (hμ : μ.colLen 0 ≤ n) : (weightOfShape n μ).shape = μ

@[simp]

theorem TauCeti.weightOfShape_shape {n : ℕ} {l : DominantWeight n} (hl : l.IsPolynomial) : weightOfShape n l.shape = l

def TauCeti.shapeEquivPolynomialWeight (n : ℕ) : { μ : YoungDiagram // μ.colLen 0 ≤ n } ≃ { l : DominantWeight n // l.IsPolynomial }

The polynomial weights are the bounded shapes: the Young diagrams with at most n rows are exactly the dominant weights of GL n with nonnegative entries.

Equations

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

@[simp]

theorem TauCeti.shapeEquivPolynomialWeight_apply_coe (n : ℕ) (μ : { μ : YoungDiagram // μ.colLen 0 ≤ n }) : ↑((shapeEquivPolynomialWeight n) μ) = weightOfShape n ↑μ

@[simp]

theorem TauCeti.shapeEquivPolynomialWeight_symm_apply_coe (n : ℕ) (l : { l : DominantWeight n // l.IsPolynomial }) : ↑((shapeEquivPolynomialWeight n).symm l) = (↑l).shape

def TauCeti.DominantWeight.detShiftShape {n : ℕ} (l : DominantWeight n) : YoungDiagram

The Young diagram of the polynomial part λ - λₙ of a dominant weight: its i-th row has length λᵢ - λₙ. Together with TauCeti.DominantWeight.detShift it presents λ as a determinant twist of a polynomial weight.

Equations

• l.detShiftShape = (l.shift (-l.detShift)).shape

@[simp]

theorem TauCeti.DominantWeight.rowLen_detShiftShape {n : ℕ} (l : DominantWeight n) (i : Fin n) : l.detShiftShape.rowLen ↑i = (↑l i - l.detShift).toNat

@[simp]

theorem TauCeti.DominantWeight.rowLen_detShiftShape_eq_zero_of_le {n : ℕ} (l : DominantWeight n) {i : ℕ} (hi : n ≤ i) : l.detShiftShape.rowLen i = 0

theorem TauCeti.DominantWeight.natCast_rowLen_detShiftShape_add_detShift {n : ℕ} (l : DominantWeight n) (i : Fin n) : ↑(l.detShiftShape.rowLen ↑i) + l.detShift = ↑l i

The polynomial part of a dominant weight recovers it after shifting back by λₙ.

@[simp]

theorem TauCeti.DominantWeight.weightOfShape_detShiftShape {n : ℕ} (l : DominantWeight n) : weightOfShape n l.detShiftShape = l.shift (-l.detShift)

The weight of the polynomial part of λ is λ itself, shifted down by λₙ.

theorem TauCeti.DominantWeight.shift_weightOfShape_detShiftShape {n : ℕ} (l : DominantWeight n) : (weightOfShape n l.detShiftShape).shift l.detShift = l

The determinant twist: every dominant weight is the weight of a Young diagram, shifted by its last entry.

theorem TauCeti.DominantWeight.colLen_zero_detShiftShape_le_pred {n : ℕ} (l : DominantWeight n) : l.detShiftShape.colLen 0 ≤ n - 1

The polynomial part of a dominant weight for GL n has at most n - 1 rows: its last entry is λₙ - λₙ = 0 when there is one, and the empty weight has the empty diagram. This is the row bound that makes the determinant twist unique.

theorem TauCeti.DominantWeight.colLen_zero_detShiftShape_le {n : ℕ} (l : DominantWeight n) : l.detShiftShape.colLen 0 ≤ n

The polynomial part of a dominant weight for GL n has at most n rows, the bound in the form consumed by the dictionary between weights and Young diagrams.

@[simp]

theorem TauCeti.DominantWeight.detShiftShape_shift {n : ℕ} (l : DominantWeight n) (m : ℤ) : (l.shift m).detShiftShape = l.detShiftShape

Shifting does not move the polynomial part: λ and λ + m·(1, …, 1) have the same Young diagram, because the shift moves the last entry by m as well and is then subtracted off again. So the polynomial part only depends on the class of λ modulo the constant weights.

@[simp]

theorem TauCeti.DominantWeight.detShiftShape_weightOfShape {n : ℕ} {μ : YoungDiagram} (hμ : μ.colLen 0 ≤ n - 1) : (weightOfShape n μ).detShiftShape = μ

The polynomial part of the weight of a Young diagram with at most n - 1 rows is that diagram again: such a weight has vanishing last entry, so nothing is subtracted. Together with TauCeti.DominantWeight.colLen_zero_detShiftShape_le_pred this makes the polynomial part a surjection onto the Young diagrams with at most n - 1 rows.

theorem TauCeti.DominantWeight.detShiftShape_eq_detShiftShape_iff {n : ℕ} (l l' : DominantWeight n) : l.detShiftShape = l'.detShiftShape ↔ ∃ (m : ℤ), l' = l.shift m

The polynomial part is a complete invariant of a weight modulo the constant weights: two dominant weights have the same polynomial part exactly when they differ by an integer multiple of (1, …, 1). With TauCeti.DominantWeight.detShiftShape_weightOfShape and TauCeti.DominantWeight.colLen_zero_detShiftShape_le_pred this identifies the dominant weights of GL n taken modulo the constant weights with the Young diagrams of at most n - 1 rows; those classes, not the weights themselves, are what a representation of SL n can see.

theorem TauCeti.DominantWeight.eq_detShift_and_eq_detShiftShape {n : ℕ} (l : DominantWeight (n + 1)) {μ : YoungDiagram} (hμ : μ.colLen 0 ≤ n) {m : ℤ} (hm : ∀ (i : Fin (n + 1)), ↑(μ.rowLen ↑i) + m = ↑l i) : m = l.detShift ∧ μ = l.detShiftShape

Uniqueness of the determinant twist: a dominant weight for GL (n + 1) is μ + m·(1, …, 1) for exactly one integer m and one Young diagram μ with at most n rows, namely m = λₙ₊₁ and μ its polynomial part. The row bound is essential: dropping it lets μ and m trade a constant against each other.

Sorting a weight into the dominant chamber

noncomputable def TauCeti.dominantSort {n : ℕ} (l : Fin n → ℤ) : Equiv.Perm (Fin n)

A permutation rearranging a weight into weakly decreasing order. It is Tuple.sort of the weight read in the order dual, since Tuple.sort produces monotone rearrangements.

Equations

• TauCeti.dominantSort l = Tuple.sort fun (i : Fin n) => OrderDual.toDual (l i)

theorem TauCeti.antitone_comp_dominantSort {n : ℕ} (l : Fin n → ℤ) : Antitone (l ∘ ⇑(dominantSort l))

Sorting makes a weight weakly decreasing.

noncomputable def TauCeti.dominantWeightOf {n : ℕ} (l : Fin n → ℤ) : DominantWeight n

The dominant weight in the Sₙ-orbit of a weight: its weakly decreasing rearrangement.

Equations

• TauCeti.dominantWeightOf l = ⟨l ∘ ⇑(TauCeti.dominantSort l), ⋯⟩

@[simp]

theorem TauCeti.coe_dominantWeightOf {n : ℕ} (l : Fin n → ℤ) : ↑(dominantWeightOf l) = l ∘ ⇑(dominantSort l)

theorem TauCeti.coe_dominantWeightOf_eq_of_antitone {n : ℕ} {l : Fin n → ℤ} {σ : Equiv.Perm (Fin n)} (h : Antitone (l ∘ ⇑σ)) : ↑(dominantWeightOf l) = l ∘ ⇑σ

Any weakly decreasing rearrangement of a weight is its dominant representative.

@[simp]

theorem TauCeti.dominantWeightOf_coe {n : ℕ} (d : DominantWeight n) : dominantWeightOf ↑d = d

A dominant weight is its own dominant representative.

@[simp]

theorem TauCeti.dominantWeightOf_comp {n : ℕ} (l : Fin n → ℤ) (σ : Equiv.Perm (Fin n)) : dominantWeightOf (l ∘ ⇑σ) = dominantWeightOf l

Rearranging a weight does not change its dominant representative.

theorem TauCeti.existsUnique_dominantWeight {n : ℕ} (l : Fin n → ℤ) : ∃! d : DominantWeight n, ∃ (σ : Equiv.Perm (Fin n)), ↑d = l ∘ ⇑σ

Each Sₙ-orbit of weights contains exactly one dominant weight, so the dominant weights are a set of representatives for the action of the Weyl group on the weight lattice.