The Garnir relations

The polytabloids e_t of the μ-tableaux span the Specht module S^μ, and the standard basis theorem says that the polytabloids of the standard tableaux already do. The relations that the straightening algorithm rewrites an arbitrary polytabloid with are the Garnir relations, and this file proves them.

Write A_X for the signed sum ∑ sgn(σ) σ over the permutations σ fixing every label outside a finite set X (TauCeti.antisymmetrizerOn, defined with the other signed sums in TauCeti/RepresentationTheory/Symmetric/Symmetrizer.lean). The Garnir relation is

A_X · e_t = 0

whenever X is too large to be spread over the rows available to it: all the labels of X lie in columns of μ of length at most r, and X has more than r elements (TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_polytabloid_eq_zero). Applied to the polytabloid it reads as the vanishing of a signed sum of the polytabloids e_{σt} (TauCeti.YoungTableau.sum_sign_smul_polytabloid_relabel_eq_zero).

Two facts drive the proof.

• A signed sum kills whatever an odd permutation in it fixes. Absorbing an odd permutation supported in X turns A_X into its own negative, so A_X annihilates every vector that permutation fixes (TauCeti.asAlgebraHom_antisymmetrizerOn_apply_eq_zero).
• Pigeonhole in the columns. A column permutation q of t moves a label only within its own column, so in the tabloid q · {t} the labels of X still lie in columns of length at most r, that is, in r rows. As X has more than r elements, two of them share a row of q · {t}, and the transposition swapping those two fixes that tabloid. Every tabloid occurring in e_t is of this form, so A_X kills them all.

The sets X the relation is applied to are the Garnir sets TauCeti.YoungTableau.garnirSet t i j: the labels of t in column j from row i downwards together with those in column j + 1 from row i upwards. As soon as (i, j + 1) is a cell of μ there are μ.colLen j + 1 of them (TauCeti.YoungTableau.card_garnirSet) while they occupy only the μ.colLen j rows of column j, so the relation applies (TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_garnirSet_polytabloid_eq_zero). Those are the sets the straightening algorithm uses at a cell (i, j) where the rows of the tableau fail to increase. Their two halves are described here as well: TauCeti.YoungTableau.garnirSetLeft names the column-j half, and a permutation supported in the set preserves the columns of t exactly when it maps that half onto itself (TauCeti.YoungTableau.mem_colSubgroup_iff_image_garnirSetLeft_eq), which is the classical description of the permutations internal to the halves as a product of two symmetric groups.

The straightening step itself is not proved here, and the relation as stated does not supply it. The permutations σ supported in X that lie in the column group of t satisfy e_{σt} = sgn(σ) e_t, so their terms in the signed sum are further copies of e_t rather than of anything nearer to standard; simply isolating the identity term of the sum therefore rewrites e_t in terms of itself. The classical Garnir element avoids this by summing only over a transversal of the permutations internal to the two halves of the set, so that A_X factors as the signed sum over those internal permutations times the Garnir element, and the identity coset contributes e_t alone. That repackaging is left to the file that performs the straightening induction; here the relation is proved, and stated, for the whole of A_X.

Main definitions

• TauCeti.YoungTableau.garnirSet: the Garnir set of a tableau at a row and a column.
• TauCeti.YoungTableau.garnirSetLeft: its column-j half.

Main results

• TauCeti.YoungTableau.exists_ne_rowIndex_relabel_eq: the pigeonhole step, two labels of an oversized set share a row after any column permutation.
• TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_polytabloid_eq_zero: the Garnir relation.
• TauCeti.YoungTableau.sum_sign_smul_polytabloid_relabel_eq_zero: the relation as the vanishing of a signed sum of polytabloids.
• TauCeti.YoungTableau.card_garnirSet: a Garnir set has one more element than the column it straddles has cells.
• TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_garnirSet_polytabloid_eq_zero: the Garnir relation at a Garnir set.
• TauCeti.YoungTableau.mem_colSubgroup_iff_image_garnirSetLeft_eq: the permutations of a Garnir set internal to its halves are those preserving its left half.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Section 7.
• B. E. Sagan, The Symmetric Group, Section 2.6.
• Schur--Weyl roadmap, Layer 5, whose standard basis of the Specht module these relations straighten towards.

The Garnir relation

theorem TauCeti.YoungTableau.exists_ne_rowIndex_relabel_eq {μ : YoungDiagram} (t : YoungTableau μ) {X : Finset (Fin μ.card)} {r : ℕ} (hX : ∀ k ∈ X, μ.colLen (t.colIndex k) ≤ r) (hcard : r < X.card) {q : Equiv.Perm (Fin μ.card)} (hq : q ∈ t.colSubgroup) : ∃ x ∈ X, ∃ y ∈ X, x ≠ y ∧ (relabel q t).rowIndex x = (relabel q t).rowIndex y

Pigeonhole in the columns. Suppose every label of X lies in a column of μ with at most r cells, and X has more than r elements. Then a column permutation q of t leaves two distinct labels of X in a common row of qt: it moves each of them only inside its own column, so all of them still lie in the top r rows.

theorem TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_polytabloid_eq_zero {μ : YoungDiagram} (t : YoungTableau μ) {X : Finset (Fin μ.card)} {r : ℕ} (hX : ∀ k ∈ X, μ.colLen (t.colIndex k) ≤ r) (hcard : r < X.card) : ((permutationModule (shapePartition μ)).ρ.asAlgebraHom (antisymmetrizerOn X)) t.polytabloid = 0

The Garnir relation. If every label of the finite set X lies in a column of μ with at most r cells and X has more than r elements, then the antisymmetrizer of X annihilates the polytabloid of t.

The labels of X cannot be spread over the rows of those columns, so every tabloid occurring in e_t has two of them in a common row and is killed by the signed sum.

theorem TauCeti.YoungTableau.sum_sign_smul_polytabloid_relabel_eq_zero {μ : YoungDiagram} (t : YoungTableau μ) {X : Finset (Fin μ.card)} {r : ℕ} (hX : ∀ k ∈ X, μ.colLen (t.colIndex k) ≤ r) (hcard : r < X.card) [DecidablePred fun (σ : Equiv.Perm (Fin μ.card)) => ∀ k ∉ X, σ k = k] : ∑ σ : Equiv.Perm (Fin μ.card) with ∀ k ∉ X, σ k = k, ↑↑(Equiv.Perm.sign σ) • (relabel σ t).polytabloid = 0

The Garnir relation, as a signed sum of polytabloids. Under the hypotheses of TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_polytabloid_eq_zero, the signed sum of the polytabloids of the relabelings σt, over the permutations σ supported in X, vanishes.

Garnir sets

def TauCeti.YoungTableau.garnirSet {μ : YoungDiagram} (t : YoungTableau μ) (i j : ℕ) : Finset (Fin μ.card)

The Garnir set of a tableau t at row i and column j: the labels of t lying in column j from row i downwards, together with those lying in column j + 1 from row i upwards.

When (i, j + 1) is a cell of μ this set has one element more than column j has cells, while its labels stay in column j or j + 1 under a column permutation of t; that is what makes the Garnir relation apply to it.

Equations

• t.garnirSet i j = {k : Fin μ.card | t.colIndex k = j ∧ i ≤ t.rowIndex k ∨ t.colIndex k = j + 1 ∧ t.rowIndex k ≤ i}

@[simp]

theorem TauCeti.YoungTableau.mem_garnirSet {μ : YoungDiagram} {t : YoungTableau μ} {i j : ℕ} {k : Fin μ.card} : k ∈ t.garnirSet i j ↔ t.colIndex k = j ∧ i ≤ t.rowIndex k ∨ t.colIndex k = j + 1 ∧ t.rowIndex k ≤ i

theorem TauCeti.YoungTableau.colLen_colIndex_le_colLen_of_mem_garnirSet {μ : YoungDiagram} {t : YoungTableau μ} {i j : ℕ} {k : Fin μ.card} (hk : k ∈ t.garnirSet i j) : μ.colLen (t.colIndex k) ≤ μ.colLen j

Every label of a Garnir set at column j lies in a column with at most as many cells as column j has, since columns of a Young diagram shorten to the right.

theorem TauCeti.YoungTableau.card_garnirSet {μ : YoungDiagram} (t : YoungTableau μ) {i j : ℕ} (h : (i, j + 1) ∈ μ) : (t.garnirSet i j).card = μ.colLen j + 1

A Garnir set is one bigger than the column it straddles. Column j contributes its cells from row i down and column j + 1 its cells from row i up, and (i, j + 1) ∈ μ makes both counts available.

theorem TauCeti.YoungTableau.asAlgebraHom_antisymmetrizerOn_garnirSet_polytabloid_eq_zero {μ : YoungDiagram} (t : YoungTableau μ) {i j : ℕ} (h : (i, j + 1) ∈ μ) : ((permutationModule (shapePartition μ)).ρ.asAlgebraHom (antisymmetrizerOn (t.garnirSet i j))) t.polytabloid = 0

The Garnir relation at a Garnir set. If (i, j + 1) is a cell of μ, the antisymmetrizer of the Garnir set of t at (i, j) annihilates the polytabloid of t.

The left half of a Garnir set

def TauCeti.YoungTableau.garnirSetLeft {μ : YoungDiagram} (t : YoungTableau μ) (i j : ℕ) : Finset (Fin μ.card)

The left half of a Garnir set: the labels of t lying in column j from row i downwards. The Garnir set of t at (i, j) is this set together with the labels in column j + 1 from row i upwards, and the permutations of the Garnir set that preserve the columns of t are exactly those preserving this half (TauCeti.YoungTableau.mem_colSubgroup_iff_image_garnirSetLeft_eq).

Equations

• t.garnirSetLeft i j = {k : Fin μ.card | t.colIndex k = j ∧ i ≤ t.rowIndex k}

@[simp]

theorem TauCeti.YoungTableau.mem_garnirSetLeft {μ : YoungDiagram} {t : YoungTableau μ} {i j : ℕ} {k : Fin μ.card} : k ∈ t.garnirSetLeft i j ↔ t.colIndex k = j ∧ i ≤ t.rowIndex k

theorem TauCeti.YoungTableau.garnirSetLeft_subset_garnirSet {μ : YoungDiagram} (t : YoungTableau μ) (i j : ℕ) : t.garnirSetLeft i j ⊆ t.garnirSet i j

The left half of a Garnir set is part of it, being the first of the two cases of its definition.

theorem TauCeti.YoungTableau.colIndex_eq_of_mem_garnirSet_of_notMem_garnirSetLeft {μ : YoungDiagram} {t : YoungTableau μ} {i j : ℕ} {k : Fin μ.card} (hk : k ∈ t.garnirSet i j) (hk' : k ∉ t.garnirSetLeft i j) : t.colIndex k = j + 1

A label of a Garnir set outside its left half lies in column j + 1, the two halves being the two cases of the definition of the Garnir set.

theorem TauCeti.YoungTableau.mem_colSubgroup_iff_image_garnirSetLeft_eq {μ : YoungDiagram} {t : YoungTableau μ} {i j : ℕ} {σ : Equiv.Perm (Fin μ.card)} (hσ : ∀ k ∉ t.garnirSet i j, σ k = k) : σ ∈ t.colSubgroup ↔ Finset.image (⇑σ) (t.garnirSetLeft i j) = t.garnirSetLeft i j

The internal permutations of a Garnir set are those preserving its left half. A permutation supported in the Garnir set of t at (i, j) preserves the columns of t exactly when it maps the column-j half of that set onto itself; it then automatically preserves the column-(j + 1) half as well, so the internal permutations are the product of the two symmetric groups on the halves.