Dominance triangularity for maps out of a Specht module

A nonzero map of representations from the Specht module S^{lam} to the Young permutation module M^μ forces the shape of lam to dominate μ (TauCeti.dominates_of_intertwiningMap_ne_zero). Equivalently, Hom(S^{lam}, M^μ) vanishes unless lam dominates μ: the matrix of multiplicities of the Specht modules in the permutation modules is triangular for the dominance order. This is the shape-comparison half of the classification of the Specht modules, and it is what turns James's dominance lemma of TauCeti/RepresentationTheory/Symmetric/Dominance.lean into a statement about maps.

The proof has two steps beyond that lemma.

• Off the tabloid basis. James's dominance lemma sees the column antisymmetrizer b_t only on a single tabloid. When lam fails to dominate μ the lemma says b_t kills every tabloid, so by linearity it kills all of M^μ; that extension lives beside the lemma itself, as TauCeti.YoungTableau.dominates_of_asAlgebraHom_columnAntisymmetrizer_apply_ne_zero.
• Producing a preimage of the polytabloid inside S^{lam}. The polytabloid is e_t = b_t·{t}, but the tabloid {t} is not in the Specht module, so b_t cannot be moved across a map defined only on S^{lam}. The tabloid form supplies an invariant complement M^{lam} = S^{lam} ⊕ W (TauCeti.isCompl_orthogonalSubrepresentation_permutationModule); splitting {t} along it and applying b_t to both summands, the W-part lands in S^{lam} ⊓ W = ⊥, so the S^{lam}-part e already satisfies b_t·e = e_t (TauCeti.YoungTableau.exists_mem_asAlgebraHom_columnAntisymmetrizer_eq_polytabloid).

With those, a nonzero f : S^{lam} → M^μ is injective, because S^{lam} is irreducible, so f e ≠ 0 and b_t · f e = f (b_t · e) = f e_t ≠ 0, and the first step applies.

Combining the theorem with itself in both directions is what shows the Specht modules of distinct shapes to be non-isomorphic; that combination needs the Specht module of a partition of n presented inside the permutation module of the same index type Fin n, and is not carried out here.

Main results

• TauCeti.YoungTableau.exists_mem_asAlgebraHom_columnAntisymmetrizer_eq_polytabloid: the polytabloid is b_t applied to a vector already inside the Specht module.
• TauCeti.dominates_of_intertwiningMap_ne_zero: a nonzero map S^{lam} → M^μ forces dominance.
• TauCeti.intertwiningMap_eq_zero_of_not_dominates: the contrapositive, as the vanishing of the whole Hom space.

References

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

A preimage of the polytabloid inside the Specht module

theorem TauCeti.YoungTableau.exists_mem_asAlgebraHom_columnAntisymmetrizer_eq_polytabloid {lam : YoungDiagram} (t : YoungTableau lam) : ∃ e ∈ (spechtSubrepresentation lam).toSubmodule, ((permutationModule (shapePartition lam)).ρ.asAlgebraHom t.columnAntisymmetrizer) e = t.polytabloid

The polytabloid is already in the image of the column antisymmetrizer on S^{lam}. Splitting the tabloid {t} as e + w along the invariant orthogonal decomposition M^{lam} = S^{lam} ⊕ (S^{lam})ᗮ and applying b_t, the two images stay in their summands while their sum is the polytabloid e_t, which lies in S^{lam}; so the second image lies in the intersection of the two summands and vanishes.

This is what lets b_t be moved across a map that is defined only on the Specht module: the tabloid {t} itself is not available there, but e is.

Dominance from a nonzero map out of the Specht module

theorem TauCeti.dominates_of_intertwiningMap_ne_zero {lam : YoungDiagram} (μ : lam.card.Partition) {f : (spechtSubrepresentation lam).toRepresentation.IntertwiningMap (permutationModule μ).ρ} (hf : f ≠ 0) : Dominates (shapePartition lam) μ

The dominance triangularity of maps out of a Specht module. A nonzero map of representations from the Specht module of lam to the Young permutation module M^μ forces the shape of lam to dominate μ.

The Specht module is irreducible, so f is injective. Pick a lam-tableau t and a vector e of S^{lam} with b_t · e = e_t; then f e_t ≠ 0 and, because f intertwines the actions, b_t · f e = f (b_t · e) = f e_t, so b_t does not annihilate M^μ and James's dominance lemma applies.

theorem TauCeti.intertwiningMap_eq_zero_of_not_dominates {lam : YoungDiagram} (μ : lam.card.Partition) (h : ¬Dominates (shapePartition lam) μ) (f : (spechtSubrepresentation lam).toRepresentation.IntertwiningMap (permutationModule μ).ρ) : f = 0

The Hom space vanishes off the dominance order. If the shape of lam does not dominate μ, every map of representations from the Specht module of lam to M^μ is zero.