Documentation

TauCeti.RepresentationTheory.Symmetric.Specht.Straightening

The Garnir element and the straightening algorithm #

The Garnir relation of TauCeti/RepresentationTheory/Symmetric/Specht/Garnir.lean says that the signed sum

∑_{σ} sgn(σ) e_{σt} = 0

over the permutations σ supported in a set X whose labels cannot be spread over the rows available to them vanishes. As it stands the relation does not rewrite e_t: the permutations that lie in the column group of t contribute further copies of e_t rather than of anything else, so isolating the identity term rewrites e_t in terms of itself. This file performs the repackaging that Garnir's file leaves open -- e_t is a rational combination of the polytabloids e_{σt} of those σ that do not preserve the columns of t -- and runs the resulting straightening step to exhaustion: every polytabloid is a rational combination of the polytabloids of the standard tableaux of the same shape, which is what makes the standard polytabloids span the Specht module.

Splitting the relation #

The whole content is that the terms of the relation indexed by the column group of t are all equal to e_t on the nose. A column permutation q scales the polytabloid by its sign (TauCeti.YoungTableau.polytabloid_relabel_of_mem_colSubgroup), so its term sgn(q) e_{qt} = sgn(q)² e_t is e_t. Splitting the sum accordingly gives

N · e_t + ∑_{σ ∉ colSubgroup t} sgn(σ) e_{σt} = 0,

where N counts the permutations supported in X that preserve the columns of t; N is positive because the identity is one of them, so e_t is -1/N times the second sum. This is the classical passage from the antisymmetrizer of X to the Garnir element, a signed sum over a transversal of the internal permutations, written here without choosing a transversal: the terms are constant on the cosets, so counting them suffices.

Which permutations are internal #

For the Garnir set X of t at a cell (i, j) -- the labels of t in column j from row i down together with those in column j + 1 from row i up -- the internal permutations are exactly the ones preserving the column-j half TauCeti.YoungTableau.garnirSetLeft, by TauCeti.YoungTableau.mem_colSubgroup_iff_image_garnirSetLeft_eq of Garnir's file. The straightening step therefore rewrites e_t in terms of the polytabloids of the tableaux obtained by genuinely exchanging labels between the two columns, which is what makes it progress towards a standard tableau.

The straightening algorithm #

The straightening step is the second of two moves that rewrite an arbitrary polytabloid into standard ones. If two labels of one column of t are out of order, exchanging them is a permutation of the column group of t, so it changes the polytabloid only by its sign (TauCeti.YoungTableau.polytabloid_relabel_of_mem_colSubgroup). If instead the columns of t increase but two labels of one row are out of order, then two labels in adjacent columns of one row are, and the straightening step at that cell writes e_t in terms of the polytabloids of the relabelings by the permutations of the Garnir set that move a label between the two columns it straddles.

Both moves increase a numerical measure of the tableau that is bounded above, so the rewriting terminates. The measure is built from the two moments ∑_k c_k · k and ∑_k r_k · k, weighting each label by the index of its column, respectively of its row. The first move fixes every label in its column and raises the row moment, since it moves the smaller of the two labels up. The second move raises the column moment: because the columns of t increase and its row does not at the chosen cell, every label of the Garnir set lying in the earlier column exceeds every label of it lying in the later one, so a permutation of the set that does not preserve the columns exchanges labels of the earlier column for strictly smaller ones. Weighting the column moment heavily enough that a gain in it outweighs any loss of row moment combines the two into one measure.

A tableau on which neither move applies increases down its columns and along its rows, so it is standard (TauCeti.exists_standardYoungTableau_toTableau_eq_iff).

Main results #

References #

Collecting the column-group terms of a Garnir relation #

source
theorem TauCeti.YoungTableau.card_nsmul_polytabloid_add_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) | (∀ k ∉ X, σ k = k) ∧ σ ∈ t.colSubgroup}.card • t.polytabloid + ∑ σ : Equiv.Perm (Fin μ.card) with (∀ k ∉ X, σ k = k) ∧ σ ∉ t.colSubgroup, ↑↑(Equiv.Perm.sign σ) • (relabel σ t).polytabloid = 0

The Garnir element relation. Under the hypotheses of the Garnir relation TauCeti.YoungTableau.sum_sign_smul_polytabloid_relabel_eq_zero -- every label of X lying in a column of μ with at most r cells, and X having more than r elements -- the permutations supported in X that preserve the columns of t contribute one copy of e_t each, so the relation reads as a multiple of e_t cancelling against the remaining terms.

This is the form the straightening algorithm uses: the multiplicity N of e_t is the number of internal permutations, and it is positive, the identity being one of them.

source
theorem TauCeti.YoungTableau.polytabloid_mem_span_polytabloid_relabel {μ : YoungDiagram} (t : YoungTableau μ) {X : Finset (Fin μ.card)} {r : ℕ} (hX : ∀ k ∈ X, μ.colLen (t.colIndex k) ≤ r) (hcard : r < X.card) :
t.polytabloid ∈ Submodule.span ℚ ((fun (σ : Equiv.Perm (Fin μ.card)) => (relabel σ t).polytabloid) '' {σ : Equiv.Perm (Fin μ.card) | (∀ k ∉ X, σ k = k) ∧ σ ∉ t.colSubgroup})

The straightening step, in the abstract. Under the hypotheses of the Garnir relation, the polytabloid of t lies in the rational span of the polytabloids of the relabelings σt for the permutations σ that are supported in X and do not preserve the columns of t.

This is the division-free reading of TauCeti.YoungTableau.card_nsmul_polytabloid_add_sum_sign_smul_polytabloid_relabel_eq_zero, whose multiple of e_t is nonzero.

The straightening step at a Garnir set #

source
theorem TauCeti.YoungTableau.polytabloid_mem_span_polytabloid_relabel_garnirSet {μ : YoungDiagram} (t : YoungTableau μ) {i j : ℕ} (h : (i, j + 1) ∈ μ) :
t.polytabloid ∈ Submodule.span ℚ ((fun (σ : Equiv.Perm (Fin μ.card)) => (relabel σ t).polytabloid) '' {σ : Equiv.Perm (Fin μ.card) | (∀ k ∉ t.garnirSet i j, σ k = k) ∧ Finset.image (⇑σ) (t.garnirSetLeft i j) ≠ t.garnirSetLeft i j})

The straightening step. As soon as (i, j + 1) is a cell of μ, the polytabloid of t lies in the rational span of the polytabloids of the relabelings σt by the permutations σ that are supported in the Garnir set of t at (i, j) and move a label between its two halves, that is between columns j and j + 1.

Applied at a cell where the rows of t fail to increase, this is the rewriting the straightening algorithm performs on the way to the standard basis of the Specht module.

The straightening measure #

Exchanging two labels of one column #

The Garnir step increases the measure #

The straightening algorithm #

source
theorem TauCeti.YoungTableau.polytabloid_mem_span_polytabloid_standard {μ : YoungDiagram} (t : YoungTableau μ) :
t.polytabloid ∈ Submodule.span ℚ (Set.range fun (T : StandardYoungTableau μ) => T.toTableau.polytabloid)

The straightening algorithm: every polytabloid is a rational combination of the polytabloids of the standard tableaux of the same shape. The straightening measure increases at every rewriting step and is bounded, so the rewriting terminates, and it terminates only at a tableau increasing down its columns and along its rows.