The standard basis of the Specht module

The polytabloid e_t of a μ-tableau t is the signed sum, over the column group of t, of the tabloids {q t}, and the Specht module S^μ is the span of all of them. This file proves that the polytabloids of the standard tableaux -- those increasing along rows and down columns -- are a basis of S^μ, so that its dimension is the number f^μ of standard Young tableaux of shape μ.

Linear independence

The first half is the triangularity of the standard polytabloids against the tabloid basis. Order the tabloids by dominance: {t} dominates {u} when, for every m and every i, at least as many of the labels below m sit in the first i + 1 rows of t as sit in the first i + 1 rows of u (TauCeti.YoungTableau.rowCount, TauCeti.YoungTableau.TabloidDominates). Two facts about that order do the work.

• The tabloid of a standard tableau is the largest one occurring in its polytabloid (TauCeti.YoungTableau.tabloidDominates_relabel_of_mem_colSubgroup). Fix a column j and a row bound i. The labels of T in column j and in the first i + 1 rows are, because T increases down its columns, exactly the smallest ones of that column, so no other set of that many labels of the column has more members below a given m. A column permutation q replaces them by another such set, and summing the resulting inequality over the columns is the claim.
• A standard tableau is determined by its tabloid (TauCeti.StandardYoungTableau.rowIndex_injective), since a standard tableau writes the labels of each row in increasing order.

Dominance is only a partial order (antisymmetric up to equality of tabloids, TauCeti.YoungTableau.TabloidDominates.antisymm), so the maximum is taken along a numerical weight private to this file, the sum of all the counts in the range where they can differ: dominance makes it larger, and a dominating tableau of no greater weight has every count equal, which pins the rows down. Taking the standard tableau of largest weight among those with a nonzero coefficient, its tabloid can occur in no other standard polytabloid of the combination, and its coefficient is the coefficient of that tabloid in the combination, hence zero.

Spanning: the straightening algorithm

The second half is the straightening algorithm TauCeti.YoungTableau.polytabloid_mem_span_polytabloid_standard of TauCeti/RepresentationTheory/Symmetric/Specht/Straightening.lean, which rewrites an arbitrary polytabloid as a rational combination of standard ones. The polytabloids span S^μ by definition, so the standard ones already do.

Main results

• TauCeti.YoungTableau.TabloidDominates.antisymm: dominance both ways is equality of tabloids.
• TauCeti.YoungTableau.tabloidDominates_relabel_of_mem_colSubgroup: a column permutation of a standard tableau lowers its tabloid.
• TauCeti.linearIndependent_polytabloid: the standard polytabloids are linearly independent.
• TauCeti.spechtSubrepresentation_eq_span_standard: the standard polytabloids span the Specht module.
• TauCeti.standardPolytabloidBasis: the standard basis of the Specht module, with TauCeti.spechtModuleStandardBasis its partition-indexed form.
• TauCeti.finrank_spechtSubrepresentation and TauCeti.finrank_spechtModule: dim S^μ = f^μ.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Sections 7 and 8.
• B. E. Sagan, The Symmetric Group, Sections 2.5 and 2.6.

Counting the labels of a tableau by row

def TauCeti.YoungTableau.rowCount {μ : YoungDiagram} (t : YoungTableau μ) (m i : ℕ) : ℕ

The number of labels below m that the μ-tableau t places in one of its first i + 1 rows. It depends on t only through its tabloid.

Equations

• t.rowCount m i = {k : Fin μ.card | ↑k < m ∧ t.rowIndex k ≤ i}.card

theorem TauCeti.YoungTableau.rowCount_congr {μ : YoungDiagram} {t u : YoungTableau μ} (h : t.rowIndex = u.rowIndex) (m i : ℕ) : t.rowCount m i = u.rowCount m i

theorem TauCeti.YoungTableau.rowCount_succ {μ : YoungDiagram} (t : YoungTableau μ) (k : Fin μ.card) (i : ℕ) : t.rowCount (↑k + 1) i = t.rowCount (↑k) i + if t.rowIndex k ≤ i then 1 else 0

Passing from the labels below k to the labels below k + 1 adds the label k itself.

theorem TauCeti.YoungTableau.rowIndex_eq_of_rowCount_eq {μ : YoungDiagram} {t u : YoungTableau μ} (h : ∀ m ≤ μ.card, ∀ i < μ.colLen 0, t.rowCount m i = u.rowCount m i) : t.rowIndex = u.rowIndex

The counts determine the rows. A tableau puts a label in the first row for which the count jumps.

The dominance order on tabloids

def TauCeti.YoungTableau.TabloidDominates {μ : YoungDiagram} (t u : YoungTableau μ) : Prop

The dominance order on tabloids. The tabloid of t dominates the tabloid of u when, for every m and i, the labels below m that t puts in its first i + 1 rows are at least as many as those that u does.

Equations

• t.TabloidDominates u = ∀ (m i : ℕ), u.rowCount m i ≤ t.rowCount m i

theorem TauCeti.YoungTableau.tabloidDominates_refl {μ : YoungDiagram} (t : YoungTableau μ) : t.TabloidDominates t

theorem TauCeti.YoungTableau.TabloidDominates.trans {μ : YoungDiagram} {t u v : YoungTableau μ} (h : t.TabloidDominates u) (h' : u.TabloidDominates v) : t.TabloidDominates v

theorem TauCeti.YoungTableau.tabloidDominates_congr {μ : YoungDiagram} {t t' u u' : YoungTableau μ} (ht : t.tabloid = t'.tabloid) (hu : u.tabloid = u'.tabloid) : t.TabloidDominates u ↔ t'.TabloidDominates u'

Dominance depends on the tableaux only through their tabloids.

theorem TauCeti.YoungTableau.TabloidDominates.antisymm {μ : YoungDiagram} {t u : YoungTableau μ} (h : t.TabloidDominates u) (h' : u.TabloidDominates t) : t.tabloid = u.tabloid

Dominance is antisymmetric up to equality of tabloids.

A column permutation lowers the tabloid of a standard tableau

theorem TauCeti.YoungTableau.tabloidDominates_relabel_of_mem_colSubgroup {μ : YoungDiagram} (T : StandardYoungTableau μ) {q : Equiv.Perm (Fin μ.card)} (hq : q ∈ T.toTableau.colSubgroup) : T.toTableau.TabloidDominates (relabel q T.toTableau)

A column permutation lowers the tabloid of a standard Young tableau. In each column of a standard tableau the labels of the first rows are the smallest ones of the column, so moving them about inside their columns can only push labels down.

Linear independence of the standard polytabloids

theorem TauCeti.linearIndependent_polytabloid (μ : YoungDiagram) : LinearIndependent ℚ fun (T : StandardYoungTableau μ) => T.toTableau.polytabloid

The standard polytabloids are linearly independent. Among the standard tableaux carrying a nonzero coefficient, one of largest weight has a tabloid that no other standard polytabloid of the combination reaches, so its coefficient is read off the combination.

The standard basis of the Specht module

theorem TauCeti.spechtSubrepresentation_eq_span_standard (μ : YoungDiagram) : (spechtSubrepresentation μ).toSubmodule = Submodule.span ℚ (Set.range fun (T : StandardYoungTableau μ) => T.toTableau.polytabloid)

The standard polytabloids span the Specht module. The polytabloids span S^μ by definition, and every one of them is a combination of the standard ones by TauCeti.YoungTableau.polytabloid_mem_span_polytabloid_standard.

noncomputable def TauCeti.standardPolytabloidBasis (μ : YoungDiagram) : Module.Basis (StandardYoungTableau μ) ℚ ↥(spechtSubrepresentation μ).toSubmodule

The standard basis theorem. The polytabloids of the standard μ-tableaux are a basis of the Specht module S^μ: they are linearly independent by TauCeti.linearIndependent_polytabloid and they span by TauCeti.spechtSubrepresentation_eq_span_standard.

Equations

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

@[simp]

theorem TauCeti.coe_standardPolytabloidBasis (μ : YoungDiagram) (T : StandardYoungTableau μ) : ↑((standardPolytabloidBasis μ) T) = T.toTableau.polytabloid

The basis vector of the standard polytabloid basis indexed by a standard Young tableau T is the polytabloid of T.

noncomputable def TauCeti.spechtModuleStandardBasis {n : ℕ} (μ : n.Partition) : Module.Basis (StandardYoungTableau (diagramOf μ)) ℚ ↑(spechtModule μ).V

The standard basis of the Specht module S^μ of a partition μ of n, the partition-indexed packaging TauCeti.spechtModule of TauCeti.standardPolytabloidBasis: S^μ has the polytabloids of the standard tableaux of shape diagramOf μ as a basis.

Equations

• TauCeti.spechtModuleStandardBasis μ = TauCeti.standardPolytabloidBasis (TauCeti.diagramOf μ)

@[simp]

theorem TauCeti.coe_spechtModuleStandardBasis {n : ℕ} (μ : n.Partition) (T : StandardYoungTableau (diagramOf μ)) : ↑((spechtModuleStandardBasis μ) T) = T.toTableau.polytabloid

The basis vector of the standard basis of the Specht module S^μ indexed by a standard Young tableau T is the polytabloid of T.

@[simp]

theorem TauCeti.finrank_spechtSubrepresentation (μ : YoungDiagram) : Module.finrank ℚ ↥(spechtSubrepresentation μ).toSubmodule = standardCount μ

The dimension of the Specht module is the number of standard Young tableaux, dim S^μ = f^μ.

theorem TauCeti.finrank_spechtModule {n : ℕ} (μ : n.Partition) : Module.finrank ℚ ↑(spechtModule μ).V = standardCount (diagramOf μ)

The dimension of the Specht module S^μ of a partition μ of n is the number f^μ of standard Young tableaux of shape μ.