Interlacing shapes and the branching of bounded tableaux

A Young diagram ν interlaces μ when their row lengths alternate, μ₀ ≥ ν₀ ≥ μ₁ ≥ ν₁ ≥ ⋯; equivalently ν ⊆ μ and the skew shape μ / ν is a horizontal strip, having at most one cell in each column. This file defines that relation, YoungDiagram.InterlacedBy, packages the shapes interlacing a fixed μ and having at most n rows as a Finset, YoungDiagram.interlacingShapes, and proves the combinatorial heart of the GLₙ₊₁ ↓ GLₙ branching rule.

That heart is a bijection. A semistandard tableau of shape μ written in the n + 1 letters {0, …, n} is the same thing as a choice of a shape ν interlacing μ together with a semistandard tableau of shape ν written in the n letters {0, …, n - 1}: the cells carrying the top letter n are exactly the cells of μ / ν. Interlacing is precisely the condition making this work. One direction is easy — rows increase weakly, so in each row the cells with a small entry form a prefix, and columns increase strictly, so μᵢ₊₁ ≤ νᵢ. The converse is where interlacing does its work: filling every cell of μ / ν with the single letter n keeps the columns strict exactly because μ / ν has no two cells in a column, which is μᵢ₊₁ ≤ νᵢ.

Interlacing also has a reading on beta-numbers, TauCeti.forall_betaNumber_le_iff_interlacedBy: shifting the row lengths by the staircase turns the alternating inequalities into the statement that the comparisons ν_j + (N - 1 - j) ≤ μ_i + (N - 1 - i) hold exactly for i ≤ j. That is the form in which horizontal strips appear in the Pieri rule.

The bijection is stated fibrewise, as TauCeti.BoundedSSYT.fiberEquiv: the tableaux of shape μ whose sub-shape of small entries is a given ν are the tableaux of shape ν. Phrasing it this way keeps every type non-dependent, so the resulting sum decomposition TauCeti.BoundedSSYT.sum_eq_sum_interlacingShapes needs no transport along an equality of shapes.

Main definitions

• YoungDiagram.InterlacedBy: InterlacedBy μ ν says that ν interlaces μ, that is μ.rowLen (i + 1) ≤ ν.rowLen i and ν.rowLen i ≤ μ.rowLen i for every i. The shape being interlaced is written first, as in TauCeti.Interlaces for integer sequences.
• YoungDiagram.interlacingShapes: the shapes interlacing μ with at most n rows.
• TauCeti.BoundedSSYT.restrictShape: the cells of μ whose entry is smaller than n.
• TauCeti.BoundedSSYT.restrict and TauCeti.BoundedSSYT.extend: erasing the cells carrying the top letter, and putting them back.

Main results

• YoungDiagram.sum_interlacingShapes_eq_sum_piFinset: the shapes with at most n rows interlacing a shape with at most n + 1 rows are parametrized by their row lengths, the j-th drawn freely from [μ_{j+1}, μ_j].
• TauCeti.forall_betaNumber_le_iff_interlacedBy: interlacing read on beta-numbers, the comparisons of the beta-numbers of the two shapes cutting out the initial segments.
• TauCeti.BoundedSSYT.restrictShape_mem_interlacingShapes: the sub-shape of small entries interlaces μ and has at most n rows.
• TauCeti.BoundedSSYT.content_restrict: erasing the top letter leaves unchanged how often each of the remaining letters occurs.
• TauCeti.BoundedSSYT.fiberEquiv: the tableaux of shape μ in n + 1 letters with a given sub-shape ν of small entries are the tableaux of shape ν in n letters.
• TauCeti.BoundedSSYT.sum_eq_sum_interlacingShapes: the resulting decomposition of a sum over the tableaux of shape μ, indexed by the interlacing shapes, and TauCeti.BoundedSSYT.card_eq_sum_interlacingShapes: its counting form, the branching rule for the number of tableaux.

References

• W. Fulton, Young Tableaux, Section 2.2.
• Classical groups roadmap, Layer 6, "branching rules".

def YoungDiagram.InterlacedBy (μ ν : YoungDiagram) : Prop

YoungDiagram.InterlacedBy μ ν says that the Young diagram ν interlaces μ: the two sequences of row lengths alternate, μ₀ ≥ ν₀ ≥ μ₁ ≥ ν₁ ≥ ⋯. Equivalently ν ⊆ μ and the skew shape μ / ν is a horizontal strip: no column of μ contains two of its cells.

As for the integer sequences of TauCeti.Interlaces, the shape being interlaced is written first.

Equations

• μ.InterlacedBy ν = ∀ (i : ℕ), μ.rowLen (i + 1) ≤ ν.rowLen i ∧ ν.rowLen i ≤ μ.rowLen i

@[simp]

theorem YoungDiagram.interlacedBy_iff {μ ν : YoungDiagram} : μ.InterlacedBy ν ↔ ∀ (i : ℕ), μ.rowLen (i + 1) ≤ ν.rowLen i ∧ ν.rowLen i ≤ μ.rowLen i

Interlacing unfolded: the pair of inequalities at each row. This is the introduction and elimination rule for YoungDiagram.InterlacedBy, whose body is not exposed.

theorem YoungDiagram.InterlacedBy.rowLen_succ_le {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (i : ℕ) : μ.rowLen (i + 1) ≤ ν.rowLen i

An interlacing shape reaches at least as far as the next row of the shape it interlaces.

theorem YoungDiagram.InterlacedBy.rowLen_le {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (i : ℕ) : ν.rowLen i ≤ μ.rowLen i

An interlacing shape reaches no further than the shape it interlaces.

theorem YoungDiagram.InterlacedBy.le {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) : ν ≤ μ

An interlacing shape is a sub-diagram.

theorem YoungDiagram.InterlacedBy.mem_of_lt {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) {i₁ i₂ j : ℕ} (hi : i₁ < i₂) (hc : (i₂, j) ∈ μ) : (i₁, j) ∈ ν

A horizontal strip has at most one cell in a column: if ν interlaces μ, then a cell of μ strictly below row i already lies in ν at row i. This is the form of interlacing that keeps a column strict when the whole of μ / ν is filled with one letter.

noncomputable def YoungDiagram.interlacingShapes (n : ℕ) (μ : YoungDiagram) : Finset YoungDiagram

The shapes interlacing μ with at most n rows. These index the summands of the GLₙ₊₁ ↓ GLₙ branching rule; the row bound is genuine, since a shape may interlace μ and still be too tall to be written in n letters.

Equations

• YoungDiagram.interlacingShapes n μ = ⋯.toFinset

@[simp]

theorem YoungDiagram.mem_interlacingShapes {μ ν : YoungDiagram} {n : ℕ} : ν ∈ interlacingShapes n μ ↔ μ.InterlacedBy ν ∧ ν.colLen 0 ≤ n

theorem YoungDiagram.sum_interlacingShapes_eq_sum_piFinset {μ : YoungDiagram} {M : Type u_1} [AddCommMonoid M] {n : ℕ} (hμ : μ.colLen 0 ≤ n + 1) (f : (Fin n → ℕ) → M) : (∑ ν ∈ interlacingShapes n μ, f fun (j : Fin n) => ν.rowLen ↑j) = ∑ r ∈ Fintype.piFinset fun (j : Fin n) => Finset.Icc (μ.rowLen (↑j + 1)) (μ.rowLen ↑j), f r

The shapes interlacing μ are parametrized by their row lengths. For a shape μ with at most n + 1 rows, a shape ν with at most n rows interlaces μ exactly when its j-th row length lies in [μ_{j+1}, μ_j] for each j < n, and it is determined by those row lengths. So a sum over the interlacing shapes is a sum over the families r : Fin n → ℕ drawn from those intervals.

theorem TauCeti.forall_betaNumber_le_iff_interlacedBy {N : ℕ} {μ ν : YoungDiagram} (hμ : μ.colLen 0 ≤ N) (hν : ν.colLen 0 ≤ N) : (∀ (i j : Fin N), ν.betaNumber N ↑j ≤ μ.betaNumber N ↑i ↔ i ≤ j) ↔ μ.InterlacedBy ν

Interlacing, read on beta-numbers. For diagrams μ and ν with at most N rows, the beta-number of ν at j is at most the beta-number of μ at i exactly for i ≤ j precisely when the row lengths interlace, μ₀ ≥ ν₀ ≥ μ₁ ≥ ⋯, that is, when μ / ν is a horizontal strip.

def TauCeti.BoundedSSYT.restrictShape {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) : YoungDiagram

The sub-shape of small entries: the cells of μ whose entry is smaller than the top letter n. It is a Young diagram because the entries increase weakly to the right and downwards.

Equations

• T.restrictShape = { cells := {c ∈ μ.cells | ↑T c.1 c.2 < n}, isLowerSet := ⋯ }

@[simp]

theorem TauCeti.BoundedSSYT.mem_restrictShape {n : ℕ} {μ : YoungDiagram} {T : BoundedSSYT (n + 1) μ} {i j : ℕ} : (i, j) ∈ T.restrictShape ↔ (i, j) ∈ μ ∧ ↑T i j < n

theorem TauCeti.BoundedSSYT.mem_iff_of_restrictShape_eq {n : ℕ} {μ ν : YoungDiagram} {T : BoundedSSYT (n + 1) μ} (hν : T.restrictShape = ν) {i j : ℕ} : (i, j) ∈ ν ↔ (i, j) ∈ μ ∧ ↑T i j < n

Reading the defining property of TauCeti.BoundedSSYT.restrictShape off an equation naming it.

theorem TauCeti.BoundedSSYT.restrictShape_le {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) : T.restrictShape ≤ μ

The sub-shape of small entries is a sub-diagram.

theorem TauCeti.BoundedSSYT.interlacedBy_restrictShape {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) : μ.InterlacedBy T.restrictShape

The sub-shape of small entries interlace the shape. Every cell of μ in row i + 1 carries an entry at most n, so column strictness makes the entry of the cell directly above it smaller than n, and that cell is therefore small: this is the inequality μᵢ₊₁ ≤ νᵢ.

theorem TauCeti.BoundedSSYT.colLen_zero_restrictShape_le {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) : T.restrictShape.colLen 0 ≤ n

The sub-shape of small entries is written in n letters, so it has at most n rows: the entry in row i is at least i.

theorem TauCeti.BoundedSSYT.restrictShape_mem_interlacingShapes {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) : T.restrictShape ∈ YoungDiagram.interlacingShapes n μ

The sub-shape of small entries is one of the shapes the branching rule sums over.

def TauCeti.BoundedSSYT.restrict {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) (ν : YoungDiagram) (hν : T.restrictShape = ν) : BoundedSSYT n ν

Erasing the top letter: a tableau of shape μ in the letters {0, …, n} restricts to a tableau of shape ν in the letters {0, …, n - 1}, where ν is its sub-shape of small entries. The shape is passed as a parameter, together with the equation identifying it, so that the result lives in a type that does not depend on T.

Equations

• T.restrict ν hν = ⟨TauCeti.BoundedSSYT.restrictTableau✝ T ν hν, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.restrict_apply {n : ℕ} {μ : YoungDiagram} (T : BoundedSSYT (n + 1) μ) (ν : YoungDiagram) (hν : T.restrictShape = ν) (i j : ℕ) : ↑(T.restrict ν hν) i j = if (i, j) ∈ ν then ↑T i j else 0

The entries of a restricted tableau.

@[simp]

theorem TauCeti.BoundedSSYT.content_restrict {n : ℕ} {μ ν : YoungDiagram} (T : BoundedSSYT (n + 1) μ) (hν : T.restrictShape = ν) {i : ℕ} (hi : i < n) : (↑(T.restrict ν hν)).content i = (↑T).content i

Erasing the top letter changes no other multiplicity: the cells of μ carrying a letter smaller than the top letter n are exactly the cells of the sub-shape ν, and there the two tableaux agree, so each such letter occupies as many cells of ν as it does of μ.

def TauCeti.BoundedSSYT.extend {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (T : BoundedSSYT n ν) : BoundedSSYT (n + 1) μ

Restoring the top letter: filling every cell of μ / ν with the letter n turns a tableau of shape ν in n letters into a tableau of shape μ in n + 1 letters.

Equations

• TauCeti.BoundedSSYT.extend h T = ⟨TauCeti.BoundedSSYT.extendTableau✝ h T, ⋯⟩

@[simp]

theorem TauCeti.BoundedSSYT.extend_apply {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (T : BoundedSSYT n ν) (i j : ℕ) : ↑(extend h T) i j = if (i, j) ∈ ν then ↑T i j else if (i, j) ∈ μ then n else 0

The entries of an extended tableau.

@[simp]

theorem TauCeti.BoundedSSYT.restrictShape_extend {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (T : BoundedSSYT n ν) : (extend h T).restrictShape = ν

Restoring the top letter on the cells of μ / ν gives back ν as the sub-shape of small entries.

def TauCeti.BoundedSSYT.fiberEquiv {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) : { T : BoundedSSYT (n + 1) μ // T.restrictShape = ν } ≃ BoundedSSYT n ν

The branching bijection, fibrewise. The tableaux of shape μ in the letters {0, …, n} whose sub-shape of small entries is a given ν are exactly the tableaux of shape ν in the letters {0, …, n - 1}: erasing and restoring the top letter are mutually inverse.

Equations

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

@[simp]

theorem TauCeti.BoundedSSYT.fiberEquiv_apply {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (T : { T : BoundedSSYT (n + 1) μ // T.restrictShape = ν }) : (fiberEquiv h) T = (↑T).restrict ν ⋯

The branching bijection erases the top letter.

@[simp]

theorem TauCeti.BoundedSSYT.fiberEquiv_symm_apply {n : ℕ} {μ ν : YoungDiagram} (h : μ.InterlacedBy ν) (T : BoundedSSYT n ν) : (fiberEquiv h).symm T = ⟨extend h T, ⋯⟩

The inverse of the branching bijection restores the top letter.

theorem TauCeti.BoundedSSYT.sum_eq_sum_interlacingShapes {M : Type u_1} [AddCommMonoid M] (n : ℕ) (μ : YoungDiagram) (f : (ν : YoungDiagram) → BoundedSSYT n ν → M) : ∑ T : BoundedSSYT (n + 1) μ, f T.restrictShape (T.restrict T.restrictShape ⋯) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, ∑ T : BoundedSSYT n ν, f ν T

The branching decomposition of a sum over tableaux: summing over the tableaux of shape μ in the letters {0, …, n} is summing, over the shapes ν interlacing μ with at most n rows, over the tableaux of shape ν in the letters {0, …, n - 1}.

theorem TauCeti.BoundedSSYT.card_eq_sum_interlacingShapes (n : ℕ) (μ : YoungDiagram) : Fintype.card (BoundedSSYT (n + 1) μ) = ∑ ν ∈ YoungDiagram.interlacingShapes n μ, Fintype.card (BoundedSSYT n ν)

The branching rule for the number of tableaux: the tableaux of shape μ in n + 1 letters are counted by the tableaux of the shapes interlacing μ, written in n letters. The statement is purely combinatorial; when μ has at most n + 1 rows it is, over ℂ, the counting shadow of the multiplicity-free GLₙ₊₁ ↓ GLₙ branching of the irreducible of highest weight μ, whose dimension is the number of such tableaux.