The dominance lemma for tableaux

Two tableaux of different shapes can be compared by asking how the rows of one meet the columns of the other. The dominance lemma says that if the labels of each row of a μ-tableau s land in pairwise distinct columns of a ν-tableau t, then ν dominates μ.

The proof is a double count. Write the labels of the first k rows of s as a set X; it has μ₁ + ⋯ + μ_k elements. Inside a fixed column of t each of those k rows contributes at most one label, so X meets that column in at most k labels, and of course in at most as many labels as the column is long. Summing over the columns of t, the cells of ν in its first k rows -- of which there are exactly min k (colLen j) in column j -- already accommodate X, so μ₁ + ⋯ + μ_k ≤ ν₁ + ⋯ + ν_k.

The counting itself is YoungDiagram.card_filter_le_sum_take_rowLens from TauCeti/Combinatorics/Young/Diagram.lean, stated for an arbitrary finite index type carrying a row function and an injection into the cells: this is what the tableau statement, where the index type is the set of labels, unfolds to, and it keeps the counting free of any tableau bookkeeping. The lemma is the combinatorial engine behind the triangularity of the Specht modules in the dominance order: a homomorphism from the Specht module S^ν into the permutation module M^μ is nonzero only when ν dominates μ, because the column antisymmetrizer of a ν-tableau kills every μ-tabloid unless the row/column condition below holds.

Main results

• TauCeti.YoungTableau.sum_take_rowLens_le_of_injective: the dominance lemma for two tableaux.
• TauCeti.dominates_of_rowIndex_colIndex_injective: the dominance lemma for partitions.
• TauCeti.exists_ne_rowIndex_eq_colIndex_eq_of_not_dominates: its contrapositive, producing two distinct labels sharing a row of s and a column of t when dominance fails.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Lemma 3.15.
• B. E. Sagan, The Symmetric Group, 2nd edition (2001), Lemma 2.2.4.
• Schur--Weyl roadmap, Layer 4, "Distinctness and completeness".

theorem TauCeti.YoungTableau.sum_take_rowLens_le_of_injective {lam m : YoungDiagram} (t : YoungTableau lam) (s : YoungTableau m) (σ : Fin m.card ≃ Fin lam.card) (h : ∀ (x y : Fin m.card), s.rowIndex x = s.rowIndex y → t.colIndex (σ x) = t.colIndex (σ y) → x = y) (k : ℕ) : (List.take k m.rowLens).sum ≤ (List.take k lam.rowLens).sum

The dominance lemma. Let s be an m-tableau and t a lam-tableau whose labels are identified by σ. If the labels of each row of s occupy pairwise distinct columns of t, then every partial sum of the row lengths of m is at most the corresponding partial sum for lam.

The hypothesis says that no row of s meets a column of t in two distinct labels, once the labels are matched up by σ.

theorem TauCeti.dominates_of_rowIndex_colIndex_injective {n : ℕ} {μ ν : n.Partition} (t : YoungTableau (diagramOf ν)) (s : YoungTableau (diagramOf μ)) (σ : Fin (diagramOf μ).card ≃ Fin (diagramOf ν).card) (h : ∀ (x y : Fin (diagramOf μ).card), s.rowIndex x = s.rowIndex y → t.colIndex (σ x) = t.colIndex (σ y) → x = y) : Dominates ν μ

The dominance lemma for partitions. If the labels of each row of a μ-tableau s land in pairwise distinct columns of a ν-tableau t, along an identification σ of their labels, then ν dominates μ.

theorem TauCeti.exists_ne_rowIndex_eq_colIndex_eq_of_not_dominates {n : ℕ} {μ ν : n.Partition} (t : YoungTableau (diagramOf ν)) (s : YoungTableau (diagramOf μ)) (σ : Fin (diagramOf μ).card ≃ Fin (diagramOf ν).card) (h : ¬Dominates ν μ) : ∃ (x : Fin (diagramOf μ).card) (y : Fin (diagramOf μ).card), x ≠ y ∧ s.rowIndex x = s.rowIndex y ∧ t.colIndex (σ x) = t.colIndex (σ y)

The contrapositive of the dominance lemma. When ν fails to dominate μ, every ν-tableau has a column meeting a row of every μ-tableau in two distinct labels.