Documentation

TauCeti.RepresentationTheory.Symmetric.Dominance

Dominance between the shape of a tableau and the shape of a tabloid #

A μ-tabloid is a coset of the Young subgroup youngSubgroup μ, so it records a partition of the labels into rows and nothing more. This file compares such a tabloid with a tableau t of a Young diagram lam, and proves James's dominance lemma: if the column antisymmetrizer b_t does not annihilate the μ-tabloid q inside the Young permutation module M^μ, then the shape of t dominates μ (TauCeti.dominates_of_asAlgebraHom_columnAntisymmetrizer_ne_zero).

The argument runs in three steps. The tabloid q = gH has rows the fibers of youngBlock μ ∘ g⁻¹, and its stabilizer is exactly the group of permutations preserving those fibers (TauCeti.stabilizer_quotientGroup_mk_youngSubgroup); counting the labels in the first k of those rows recovers the partial sums of μ (TauCeti.card_filter_youngBlock_lt), which is what feeds the counting core YoungDiagram.card_filter_le_sum_take_rowLens of TauCeti/Combinatorics/Young/Diagram.lean and yields dominance from the row/column condition. That condition is then supplied by the sign cancellation: if two labels sharing a column of t lie in a common row of q, their transposition is an odd element of the column group fixing q, which b_t absorbs at the cost of its sign while leaving q alone, so b_t · q = 0.

This is the shape-comparison half of the argument that the Specht modules are pairwise non-isomorphic: a nonzero map S^{lam} → M^μ sends a polytabloid b_t · {t} to a combination of the vectors b_t · q, so one of them survives. Producing that map from an isomorphism of Specht modules, which needs a complement to S^{lam} in M^{lam}, is a separate step and is not proved here.

Main results #

References #

source
theorem TauCeti.dominates_of_youngBlock_colIndex_injective {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) (g : Equiv.Perm (Fin lam.card)) (h : ∀ (x y : Fin lam.card), youngBlock μ (g⁻¹ x) = youngBlock μ (g⁻¹ y) → t.colIndex x = t.colIndex y → x = y) :
Dominates (shapePartition lam) μ

The dominance lemma for a tableau and a tabloid. If the labels of each row of the μ-tabloid gH occupy pairwise distinct columns of the lam-tableau t, then the shape of t dominates μ.

source
theorem TauCeti.dominates_of_forall_swap_smul_ne {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) (q : Equiv.Perm (Fin lam.card) ⧸ youngSubgroup μ) (h : ∀ (x y : Fin lam.card), x ≠ y → t.colIndex x = t.colIndex y → Equiv.swap x y • q ≠ q) :
Dominates (shapePartition lam) μ

The dominance lemma in its group-theoretic form. If no transposition of two labels lying in a common column of the lam-tableau t fixes the μ-tabloid q, then the shape of t dominates μ.

This is the form the Specht-module argument uses: such a transposition is an odd element of the column group of t fixing q, and its presence is exactly what makes the column antisymmetrizer of t annihilate q.

The column antisymmetrizer acting on a tabloid #

source
theorem TauCeti.asAlgebraHom_columnAntisymmetrizer_single_eq_zero {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) (q : Equiv.Perm (Fin lam.card) ⧸ youngSubgroup μ) {p : Equiv.Perm (Fin lam.card)} (hp : p ∈ t.colSubgroup) (hsign : Equiv.Perm.sign p = -1) (hfix : p • q = q) :
((permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer) (MonoidAlgebra.single q 1) = 0

The column antisymmetrizer kills a tabloid fixed by an odd column permutation. The antisymmetrizer absorbs such a permutation up to its sign, which is -1, while the tabloid is left alone, so the value is its own negative.

source
theorem TauCeti.dominates_of_asAlgebraHom_columnAntisymmetrizer_ne_zero {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) (q : Equiv.Perm (Fin lam.card) ⧸ youngSubgroup μ) (h : ((permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer) (MonoidAlgebra.single q 1) ≠ 0) :
Dominates (shapePartition lam) μ

James's dominance lemma. If the column antisymmetrizer of a lam-tableau t does not annihilate the μ-tabloid q, then the shape of t dominates μ.

This is the statement the classification of the Specht modules consumes: a homomorphism M^{lam} → M^μ that does not kill the polytabloid b_t · {t} carries it to a combination of the vectors b_t · q, so one of those is nonzero and the shape of t dominates μ.

source
theorem TauCeti.YoungTableau.asAlgebraHom_columnAntisymmetrizer_apply_eq_zero_of_not_dominates {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) (h : ¬Dominates (shapePartition lam) μ) (x : ↑(permutationModule μ)) :
((permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer) x = 0

The column antisymmetrizer of a non-dominating shape annihilates the whole permutation module. James's dominance lemma says that b_t kills every μ-tabloid once the shape of t fails to dominate μ; the tabloids span M^μ, so b_t kills all of it.

This is to TauCeti.dominates_of_asAlgebraHom_columnAntisymmetrizer_ne_zero what TauCeti.YoungTableau.exists_eq_smul_polytabloid is to TauCeti.YoungTableau.exists_eq_smul_polytabloid_single: the same statement, extended off the tabloid basis by linearity.

source
theorem TauCeti.YoungTableau.dominates_of_asAlgebraHom_columnAntisymmetrizer_apply_ne_zero {lam : YoungDiagram} (t : YoungTableau lam) (μ : lam.card.Partition) {x : ↑(permutationModule μ)} (hx : ((permutationModule μ).ρ.asAlgebraHom t.columnAntisymmetrizer) x ≠ 0) :
Dominates (shapePartition lam) μ

James's dominance lemma for an arbitrary vector. If the column antisymmetrizer of a lam-tableau does not annihilate some vector of M^μ, then the shape of lam dominates μ.