Young permutation modules

For a partition μ of n, the Young permutation module M^μ is the rational permutation representation of Equiv.Perm (Fin n) on the left cosets of the Young subgroup associated to μ. These cosets are the μ-tabloids.

This file records the tabloid basis and its action, computes the stabilizer of a tabloid as the group preserving its rows (TauCeti.stabilizer_quotientGroup_mk_youngSubgroup), identifies M^μ with the representation induced from the trivial representation of the Young subgroup, and computes its dimension and character. In particular, the dimension is the multinomial coefficient n! / ∏ i, μᵢ!, while the character at a permutation is the number of fixed tabloids.

Main definitions

• TauCeti.permutationModule is the Young permutation module M^μ.
• TauCeti.permutationModuleBasis is its basis indexed by μ-tabloids.
• TauCeti.permutationModuleIsoIndTrivial identifies M^μ with an induced trivial representation.
• TauCeti.permutationModuleFDRep is the finite-dimensional bundled form of M^μ.

References

• G. D. James, The Representation Theory of the Symmetric Groups, for Young permutation modules and tabloids.
• Schur-Weyl roadmap, Layer 1, “The permutation module”.

The tabloid model

@[reducible, inline]

noncomputable abbrev TauCeti.permutationModule {n : ℕ} (μ : n.Partition) : Rep.{0, 0, 0} ℚ (Equiv.Perm (Fin n))

The Young permutation module M^μ over ℚ.

Its standard basis is indexed by the left cosets of youngSubgroup μ; these cosets are the μ-tabloids, and the symmetric group acts on them by left multiplication.

Equations

• TauCeti.permutationModule μ = Rep.ofMulAction ℚ (Equiv.Perm (Fin n)) (Equiv.Perm (Fin n) ⧸ TauCeti.youngSubgroup μ)

@[reducible, inline]

noncomputable abbrev TauCeti.permutationModuleBasis {n : ℕ} (μ : n.Partition) : Module.Basis (Equiv.Perm (Fin n) ⧸ youngSubgroup μ) ℚ ↑(permutationModule μ)

The standard basis of M^μ, indexed by the μ-tabloids.

Equations

• TauCeti.permutationModuleBasis μ = MonoidAlgebra.basis (Equiv.Perm (Fin n) ⧸ TauCeti.youngSubgroup μ) ℚ

theorem TauCeti.stabilizer_quotientGroup_mk_youngSubgroup {n : ℕ} (μ : n.Partition) (g : Equiv.Perm (Fin n)) : MulAction.stabilizer (Equiv.Perm (Fin n)) ↑g = fiberSubgroup fun (x : Fin n) => youngBlock μ (g⁻¹ x)

The stabilizer of a tabloid. A permutation fixes the coset gH of the Young subgroup of μ exactly when it preserves every fiber of the block map transported by g, that is, when it permutes the labels within the rows of the tabloid.

Induction, dimension, and character

noncomputable def TauCeti.permutationModuleIsoIndTrivial {n : ℕ} (μ : n.Partition) : permutationModule μ ≅ Rep.ind (youngSubgroup μ).subtype (Rep.trivial ℚ ↥(youngSubgroup μ) ℚ)

The Young permutation module is induction of the trivial representation of the Young subgroup.

Equations

• TauCeti.permutationModuleIsoIndTrivial μ = (TauCeti.indTrivialIso ℚ (TauCeti.youngSubgroup μ)).symm

theorem TauCeti.finrank_permutationModule_eq_index {n : ℕ} (μ : n.Partition) : Module.finrank ℚ ↑(permutationModule μ) = (youngSubgroup μ).index

The dimension of M^μ is the index of its Young subgroup.

@[simp]

theorem TauCeti.finrank_permutationModule {n : ℕ} (μ : n.Partition) : Module.finrank ℚ ↑(permutationModule μ) = n.factorial / (Multiset.map Nat.factorial μ.parts).prod

The dimension of M^μ is the multinomial coefficient n! / ∏ i, μᵢ!.

theorem TauCeti.char_permutationModule {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : (permutationModule μ).ρ.character σ = ↑(Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup μ // σ • q = q })

The character of M^μ at σ is the number of μ-tabloids fixed by σ.

@[reducible, inline]

noncomputable abbrev TauCeti.permutationModuleFDRep {n : ℕ} (μ : n.Partition) : FDRep ℚ (Equiv.Perm (Fin n))

The Young permutation module bundled as a finite-dimensional representation.

Equations

• TauCeti.permutationModuleFDRep μ = FDRep.of (TauCeti.permutationModule μ).ρ

@[simp]

theorem TauCeti.finrank_permutationModuleFDRep {n : ℕ} (μ : n.Partition) : Module.finrank ℚ ↑(permutationModuleFDRep μ).V = n.factorial / (Multiset.map Nat.factorial μ.parts).prod

The bundled Young permutation module has the same multinomial dimension.

@[simp]

theorem TauCeti.char_permutationModuleFDRep {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) : (permutationModuleFDRep μ).character σ = ↑(Nat.card { q : Equiv.Perm (Fin n) ⧸ youngSubgroup μ // σ • q = q })

The character of the bundled Young permutation module counts fixed tabloids.