Young symmetrizers #

For a Young tableau t, this file defines the row symmetrizer a_t, the column antisymmetrizer b_t, and the Young symmetrizer c_t = a_t b_t in the rational group algebra of the symmetric group on the entries of t.

The defining coefficient formulas are accompanied by the translation laws that characterize the two factors: the row group fixes a_t, while the column group acts on b_t through the sign character. In particular, each factor squares to its subgroup order times itself. Both factors are instances of a single construction: the character sum ∑_{h ∈ H} χ(h) h of a multiplicative character over a finite subgroup, TauCeti.subgroupCharSum. The row symmetrizer is the trivial character over the row group and the column antisymmetrizer is the sign character over the column group, so the coefficient formula, the two translation laws, the square, and the values on a trivial or full subgroup are read off from that shared API instead of being proved once for each factor. These are the elementary inputs to the essential-idempotence theorem for c_t and the construction of Specht modules. The two extreme shapes are also evaluated here: a trivial row or column group collapses the corresponding factor to 1, so on a shape with at most one row the whole group fixes c_t, and on a shape with at most one column it scales c_t by the sign. The same two degeneracies evaluate the transported symmetrizer youngSymmetrizerOver outright, as the full symmetrization ∑_σ σ and the full antisymmetrization ∑_σ sgn(σ) σ of the group algebra. Finally, b_t acting on an arbitrary representation is unfolded into the signed sum over the column group, which is how every downstream computation with the operator b_t begins.

The file closes with a third signed sum at the sign character, TauCeti.antisymmetrizerOn X: the sum ∑ sgn(σ) σ over the permutations of an arbitrary type fixing everything outside a finite set X. It is b_t with the column group replaced by the pointwise fixing subgroup of the complement of X, so it shares the coefficient formula, the translation law and the vanishing criterion with b_t, and it is the element the Garnir relations of TauCeti/RepresentationTheory/Symmetric/Specht/Garnir.lean are stated for. Nothing about it refers to a tableau, only to the sign character TauCeti.signLinearCharacter.

The symmetrizers are built over ℚ, which is what the essential-idempotence theorem and the Specht-module constructions downstream of this file work over. The coefficients of c_t are in fact integral -- each is a sum of signs -- so nothing about c_t itself demands rational coefficients; it is this definition, over ℚ, whose coefficients are transported when c_t is made to act on a module over another ring, which is youngSymmetrizerOver. That transport goes along algebraMap ℚ k, so it asks the target ring to be a ℚ-algebra. The restriction is one of the present implementation, not of the mathematics: an integral c_t, over ℤ or over an arbitrary commutative ring, would remove it, and is a separate construction.

References #

G. D. James, The Representation Theory of the Symmetric Groups, Chapter 2.
Schur--Weyl roadmap, Layer 2.

Young symmetrizers #

References #

The symmetrizers of an extreme shape #

The column antisymmetrizer as an operator #

The antisymmetrizer of a set of points #