The two extreme Young permutation modules

The Young permutation module M^μ of a partition μ of n interpolates between two extremes. For the coarsest partition (n) there is a single μ-tabloid and M^{(n)} is the trivial representation; for the all-ones partition (1ⁿ) the tabloids are the permutations themselves and M^{(1ⁿ)} is the regular representation ℚ[Sₙ].

The proofs go through the Young subgroups: youngSubgroup (n) = ⊤ and youngSubgroup (1ⁿ) = ⊥, so the two modules are the permutation representations of Sₙ on the cosets of the whole group and of the trivial subgroup respectively.

Main definitions

• TauCeti.permutationModuleIndiscreteIsoTrivial: M^{(n)} ≅ ℚ with the trivial action.
• TauCeti.permutationModuleOnesIsoLeftRegular: M^{(1ⁿ)} ≅ ℚ[Sₙ] with the left regular action.

Both isomorphisms come with the lemmas reading them, and their inverses, on the tabloid basis.

Main statements

• TauCeti.finrank_permutationModule_indiscrete and TauCeti.finrank_permutationModule_ones: the two dimensions, 1 and n !.
• TauCeti.char_permutationModule_indiscrete and TauCeti.char_permutationModule_ones: the two characters, the constant 1 and the regular character supported at the identity.

References

• G. D. James, The Representation Theory of the Symmetric Groups, §4.
• Schur-Weyl roadmap, Layer 1, “the base cases M^{(n)} = S^{(n)} (trivial) and M^{(1ⁿ)} = ℚ[Sₙ] (regular)”.

The coarsest partition (n)

Mathlib's Nat.Partition.indiscrete n is the partition with the single part n when n ≠ 0, and the empty partition of 0 when n = 0; either way its Young subgroup is all of Sₙ.

noncomputable def TauCeti.permutationModuleIndiscreteIsoTrivial (n : ℕ) : permutationModule (Nat.Partition.indiscrete n) ≅ Rep.trivial ℚ (Equiv.Perm (Fin n)) ℚ

The Young permutation module of the coarsest partition (n) is the trivial representation: there is only one (n)-tabloid.

Equations

• TauCeti.permutationModuleIndiscreteIsoTrivial n = TauCeti.quotientIsoCongr ℚ ⋯ ≪≫ TauCeti.quotientTopIsoTrivial ℚ

@[simp]

theorem TauCeti.permutationModuleIndiscreteIsoTrivial_hom_hom_single (n : ℕ) (t : Equiv.Perm (Fin n) ⧸ youngSubgroup (Nat.Partition.indiscrete n)) (r : ℚ) : (Rep.Hom.hom (permutationModuleIndiscreteIsoTrivial n).hom) (MonoidAlgebra.single t r) = r

Every (n)-tabloid is sent to 1.

@[simp]

theorem TauCeti.permutationModuleIndiscreteIsoTrivial_inv_hom_apply (n : ℕ) (r : ℚ) : (Rep.Hom.hom (permutationModuleIndiscreteIsoTrivial n).inv) r = MonoidAlgebra.single (↑1) r

The inverse sends r to r times the unique (n)-tabloid.

@[simp]

theorem TauCeti.finrank_permutationModule_indiscrete (n : ℕ) : Module.finrank ℚ ↑(permutationModule (Nat.Partition.indiscrete n)) = 1

The Young permutation module of the coarsest partition (n) is one-dimensional.

theorem TauCeti.char_permutationModule_indiscrete (n : ℕ) (σ : Equiv.Perm (Fin n)) : (permutationModule (Nat.Partition.indiscrete n)).ρ.character σ = 1

The character of the Young permutation module of (n) is constantly 1.

Not a simp lemma: char_ofMulAction already rewrites the left-hand side to the fixed-tabloid count.

The all-ones partition (1ⁿ)

noncomputable def TauCeti.permutationModuleOnesIsoLeftRegular (n : ℕ) : permutationModule (Nat.Partition.ones n) ≅ Rep.leftRegular ℚ (Equiv.Perm (Fin n))

The Young permutation module of the all-ones partition (1ⁿ) is the regular representation ℚ[Sₙ]: the (1ⁿ)-tabloids are the permutations themselves.

Equations

• TauCeti.permutationModuleOnesIsoLeftRegular n = TauCeti.quotientIsoCongr ℚ ⋯ ≪≫ TauCeti.quotientBotIsoLeftRegular ℚ

@[simp]

theorem TauCeti.permutationModuleOnesIsoLeftRegular_hom_hom_single (n : ℕ) (t : Equiv.Perm (Fin n) ⧸ youngSubgroup (Nat.Partition.ones n)) (r : ℚ) : (Rep.Hom.hom (permutationModuleOnesIsoLeftRegular n).hom) (MonoidAlgebra.single t r) = MonoidAlgebra.single (QuotientGroup.quotientBot ((Subgroup.quotientEquivOfEq ⋯) t)) r

A (1ⁿ)-tabloid is sent to the permutation it names.

@[simp]

theorem TauCeti.permutationModuleOnesIsoLeftRegular_hom_hom_single_mk (n : ℕ) (σ : Equiv.Perm (Fin n)) (r : ℚ) : (Rep.Hom.hom (permutationModuleOnesIsoLeftRegular n).hom) (MonoidAlgebra.single (↑σ) r) = MonoidAlgebra.single σ r

The (1ⁿ)-tabloid of a permutation is sent to that permutation.

@[simp]

theorem TauCeti.permutationModuleOnesIsoLeftRegular_inv_hom_single (n : ℕ) (σ : Equiv.Perm (Fin n)) (r : ℚ) : (Rep.Hom.hom (permutationModuleOnesIsoLeftRegular n).inv) (MonoidAlgebra.single σ r) = MonoidAlgebra.single (↑σ) r

The inverse sends a permutation back to its (1ⁿ)-tabloid.

@[simp]

theorem TauCeti.finrank_permutationModule_ones (n : ℕ) : Module.finrank ℚ ↑(permutationModule (Nat.Partition.ones n)) = n.factorial

The Young permutation module of the all-ones partition (1ⁿ) has dimension n !.

theorem TauCeti.char_permutationModule_ones (n : ℕ) (σ : Equiv.Perm (Fin n)) : (permutationModule (Nat.Partition.ones n)).ρ.character σ = if σ = 1 then ↑n.factorial else 0

The character of the Young permutation module of (1ⁿ) is the regular character: it is n ! at the identity and vanishes elsewhere.

Not a simp lemma: char_ofMulAction already rewrites the left-hand side to the fixed-tabloid count.