The row-column factorization of a permutation #
For a μ-tableau t with row group Row(t) and column group Col(t), the key vanishing lemma
of TauCeti.RepresentationTheory.Symmetric.Vanishing kills the sandwich a_t σ b_t whenever a
row of t meets a column of relabel σ t twice, and the converse direction there shows that the
criterion never fires on a permutation of the form p q with p ∈ Row(t) and q ∈ Col(t). What
was missing is that these two cases are exhaustive: this file proves the row-column
factorization, that a permutation on which the criterion does not fire already factors as
p q (TauCeti.YoungTableau.mem_mul_of_not_rowMeetsColumnTwice).
The combinatorial content is the counting lemma
TauCeti.YoungTableau.colIndex_lt_rowLen_of_injective of
TauCeti.Combinatorics.Young.Tableau. Write r for rowIndex t and c for colIndex t: the
failure of the criterion says exactly that x ↦ (r x, c (u x)) is injective, for u = σ⁻¹, and
the counting lemma then puts (r x, c (u x)) back inside μ. Sending x to the label of that
cell is an injective, hence bijective, self-map of the labels which preserves rows, and it splits
u into a column permutation times a row permutation.
The factorization completes the sandwich calculation. Every sandwich a_t x b_t is a scalar
multiple of the Young symmetrizer c_t = a_t b_t
(TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer): on a permutation the two cases above give
0 or sign q • c_t, and the general case follows by linearity. Consequently c_t is
essentially idempotent, c_t x c_t ∈ ℚ ∙ c_t for every x
(TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer_mul_mul), and in particular
c_t ^ 2 = n_t • c_t (TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer_sq). The same holds
for the symmetrizer transported to any ℚ-algebra k, with x now ranging over k[Sₙ]
(TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizerOver_mul_mul). Identifying the
scalar n_t as μ.card ! / f^μ, and with it the idempotent generating the Specht ideal, needs the
dimension count of the Specht module and is not done here.
References #
- W. Fulton, Young Tableaux, Section 7.2, Lemma 3.
- W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lemma 4.24 and Lemma 4.26.
- Schur--Weyl roadmap, Layer 3.
The factorization #
The row-column factorization. A permutation on which the row/column criterion does not
fire lies in the product set Row(t) · Col(t).
Together with TauCeti.YoungTableau.notMem_mul_of_rowMeetsColumnTwice this makes the criterion an
exact description of the complement of Row(t) · Col(t), so the two cases of the sandwich
calculation are exhaustive.
The row/column criterion fires on exactly the permutations outside Row(t) · Col(t).
The symmetrizer sandwich #
The sandwich of a permutation between the row symmetrizer and the column antisymmetrizer is a
multiple of the Young symmetrizer: it vanishes off Row(t) · Col(t) by the key vanishing lemma,
and on p q it is sign q • c_t.
Every symmetrizer sandwich is a multiple of the Young symmetrizer: for every element x
of the group algebra, a_t x b_t ∈ ℚ ∙ c_t. This is the linear extension of
TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer_single.
The Young symmetrizer is essentially idempotent: c_t x c_t is a multiple of c_t for
every element x of the group algebra. Writing c_t = a_t b_t turns the sandwich c_t x c_t
into the sandwich a_t (b_t x a_t) b_t.
The square of a Young symmetrizer is a multiple of it. Identifying the scalar needs the
dimension of the left ideal ℚ[Sₙ] c_t, so it is done downstream, in
TauCeti.YoungTableau.youngSymmetrizer_sq, which proves the scalar is
μ.card ! / finrank ℚ (ℚ[Sₙ] c_t). The roadmap writes it as μ.card ! / f^μ, with f^μ the
number of standard tableaux of shape μ; that form needs the standard basis theorem
dim S^μ = f^μ, which is not available yet.
The transported Young symmetrizer is essentially idempotent: over a ℚ-algebra k,
c_t x c_t is a k-multiple of c_t for every element x of k[Sₙ].