Essential idempotence of the Young symmetrizer

The Young symmetrizer c_t of a tableau t of shape μ satisfies c_t * c_t = κ • c_t for some rational κ; that much is the sandwich lemma TauCeti.YoungTableau.exists_eq_smul_youngSymmetrizer_sq, which leaves κ unidentified. This file identifies it:

c_t * c_t = (n! / dim ℚ[Sₙ] c_t) • c_t.

The proof is the classical trace computation. Right multiplication by c_t is a ℚ-linear endomorphism φ of ℚ[Sₙ] whose range is exactly the left ideal ℚ[Sₙ] c_t, and the identity c_t * c_t = κ • c_t says φ * φ = κ • φ. Such a φ is a scaled projection onto its range, so its trace is κ · dim (ℚ[Sₙ] c_t) (TauCeti.LinearMap.trace_eq_mul_finrank_range). On the other hand the matrix of φ in the basis of permutations has every diagonal entry equal to the coefficient of c_t at the identity, which is 1, so the trace is n! (TauCeti.MonoidAlgebra.trace_mulRight). Comparing gives κ · dim = n!, and the dimension is positive.

The roadmap states the scalar as n! / f^μ with f^μ the number of standard Young tableaux of shape μ. The two readings agree once the standard basis theorem identifies dim S^μ = f^μ; that identification needs the straightening algorithm and is not proved here, so the dimension of the ideal is what appears below. Nothing in this file assumes the comparison of ℚ[Sₙ] c_t with the polytabloid presentation of S^μ.

The two extreme shapes are the cases in which the dimension, and hence the scalar, can be read off directly; those evaluations live with the rest of the extreme-shape theory, in TauCeti.RepresentationTheory.Symmetric.Specht.Ideal.Extremes, which is downstream of this file.

Main statements

• TauCeti.YoungTableau.range_mulRight_youngSymmetrizer: right multiplication by c_t has the left ideal ℚ[Sₙ] c_t as its range.
• TauCeti.YoungTableau.finrank_spechtIdeal_smul_youngSymmetrizer_sq: the division-free form dim • (c_t * c_t) = n! • c_t.
• TauCeti.YoungTableau.youngSymmetrizer_sq: essential idempotence, c_t * c_t = (n! / dim) • c_t.
• TauCeti.YoungTableau.isIdempotentElem_smul_youngSymmetrizer: the normalisation (dim / n!) • c_t is idempotent.
• TauCeti.YoungTableau.youngSymmetrizerOver_sq: essential idempotence of the Young symmetrizer transported into a ℚ-algebra k, with the same scalar read in k.

Implementation notes

None of the identities below is a simp lemma. Their right-hand sides carry a dimension that no other lemma consumes, and rewriting c_t * c_t into a scaled c_t replaces a product that later simp sets do reduce (through TauCeti.YoungTableau.mul_youngSymmetrizer_left and its companions) by an opaque scalar.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lemma 4.26.
• Schur--Weyl roadmap, Layer 2, the “idempotent theory” item c_t * c_t = (n! / f^λ) • c_t.

theorem TauCeti.YoungTableau.range_mulRight_youngSymmetrizer {μ : YoungDiagram} (t : YoungTableau μ) : (LinearMap.mulRight ℚ t.youngSymmetrizer).range = Submodule.restrictScalars ℚ t.spechtIdeal

The left ideal generated by c_t is the range of right multiplication by c_t. This is the ℚ-linear description of ℚ[Sₙ] c_t that the trace computation needs.

theorem TauCeti.YoungTableau.trace_mulRight_youngSymmetrizer {μ : YoungDiagram} (t : YoungTableau μ) : (LinearMap.trace ℚ (MonoidAlgebra ℚ (Equiv.Perm (Fin μ.card)))) (LinearMap.mulRight ℚ t.youngSymmetrizer) = ↑μ.card.factorial

The trace of right multiplication by c_t on ℚ[Sₙ] is n!: every diagonal entry of its matrix in the basis of permutations is the coefficient of c_t at the identity, which is 1.

theorem TauCeti.YoungTableau.finrank_spechtIdeal_smul_youngSymmetrizer_sq {μ : YoungDiagram} (t : YoungTableau μ) : ↑(Module.finrank ℚ ↥t.spechtIdeal) • (t.youngSymmetrizer * t.youngSymmetrizer) = ↑μ.card.factorial • t.youngSymmetrizer

The essential idempotence of the Young symmetrizer, division-free. The dimension of the left ideal ℚ[Sₙ] c_t times the square of c_t is n! times c_t.

theorem TauCeti.YoungTableau.youngSymmetrizer_sq {μ : YoungDiagram} (t : YoungTableau μ) : t.youngSymmetrizer * t.youngSymmetrizer = (↑μ.card.factorial / ↑(Module.finrank ℚ ↥t.spechtIdeal)) • t.youngSymmetrizer

Essential idempotence of the Young symmetrizer. The square of c_t is c_t scaled by n! over the dimension of the left ideal ℚ[Sₙ] c_t.

The roadmap writes the scalar as n! / f^μ, with f^μ the number of standard Young tableaux of shape μ; the two agree once the standard basis theorem gives dim S^μ = f^μ, which is not available yet.

theorem TauCeti.YoungTableau.youngSymmetrizer_sq_ne_zero {μ : YoungDiagram} (t : YoungTableau μ) : t.youngSymmetrizer * t.youngSymmetrizer ≠ 0

The square of a Young symmetrizer is nonzero: the scalar n! / dim is positive and c_t itself is nonzero.

theorem TauCeti.YoungTableau.isIdempotentElem_smul_youngSymmetrizer {μ : YoungDiagram} (t : YoungTableau μ) : IsIdempotentElem ((↑(Module.finrank ℚ ↥t.spechtIdeal) / ↑μ.card.factorial) • t.youngSymmetrizer)

The normalised Young symmetrizer is idempotent. Scaling c_t by dim / n! turns the essential idempotence into genuine idempotence, so ℚ[Sₙ] c_t is generated by an idempotent.

theorem TauCeti.YoungTableau.youngSymmetrizerOver_sq {μ : YoungDiagram} (k : Type u_1) [CommSemiring k] [Algebra ℚ k] (t : YoungTableau μ) : youngSymmetrizerOver k t * youngSymmetrizerOver k t = (algebraMap ℚ k) (↑μ.card.factorial / ↑(Module.finrank ℚ ↥t.spechtIdeal)) • youngSymmetrizerOver k t

Essential idempotence over a ℚ-algebra. The Young symmetrizer transported into k[Sₙ] squares to the same scalar n! / dim ℚ[Sₙ] c_t times itself, the scalar now read in k.