The tabloid form on a Young permutation module

The Young permutation module M^μ has a basis indexed by the μ-tabloids, and the bilinear form declaring that basis orthonormal is the tabloid form. It is the specialisation to M^μ of the invariant form on a permutation representation, so the whole orthogonality API of TauCeti.permutationForm applies verbatim: the tabloid form is symmetric, positive definite, and preserved by the symmetric group, and the orthogonal complement of a subrepresentation of M^μ is again a subrepresentation and is a complement.

This file names the form, reads it on the tabloid basis and on coset representatives, and records the two statements that the theory of Specht modules uses: invariance under the symmetric group and complementation. The orthogonality relation itself is the tool behind James's submodule theorem, which compares a submodule of M^μ with the orthogonal complement of the Specht module inside it.

Main definitions

• TauCeti.tabloidForm: the tabloid form on M^μ.

Main results

• TauCeti.tabloidForm_basis_basis: the tabloid basis is orthonormal.
• TauCeti.tabloidForm_single_coe_single_coe_of_mem and TauCeti.tabloidForm_single_coe_single_coe_of_notMem: two tabloids given by permutations pair to 1 or to 0 according to whether the permutations differ by an element of the Young subgroup.
• TauCeti.tabloidForm_invariant: the symmetric group acts on M^μ by isometries of the tabloid form.
• TauCeti.isCompl_orthogonalSubrepresentation_permutationModule: a subrepresentation of M^μ is complemented by its orthogonal complement.

References

• G. D. James, The Representation Theory of the Symmetric Groups, Chapter 1, where the form is introduced by declaring the tabloids orthonormal, and Chapter 4 for the submodule theorem.
• Schur-Weyl roadmap, Layer 3, "The submodule theorem (James)", which asks for the tabloid bilinear form as an API in its own right.

@[reducible, inline]

noncomputable abbrev TauCeti.tabloidForm {n : ℕ} (μ : n.Partition) : LinearMap.BilinForm ℚ (MonoidAlgebra ℚ (Equiv.Perm (Fin n) ⧸ youngSubgroup μ))

The tabloid form on the Young permutation module M^μ: the bilinear form for which the tabloid basis is orthonormal.

Equations

• TauCeti.tabloidForm μ = TauCeti.permutationForm ℚ (Equiv.Perm (Fin n) ⧸ TauCeti.youngSubgroup μ)

theorem TauCeti.tabloidForm_basis_basis {n : ℕ} (μ : n.Partition) (i j : Equiv.Perm (Fin n) ⧸ youngSubgroup μ) [Decidable (i = j)] : ((tabloidForm μ) ((permutationModuleBasis μ) i)) ((permutationModuleBasis μ) j) = if i = j then 1 else 0

The tabloid basis of M^μ is orthonormal for the tabloid form.

theorem TauCeti.tabloidForm_single_coe_single_coe_of_mem {n : ℕ} (μ : n.Partition) {g h : Equiv.Perm (Fin n)} (hgh : g⁻¹ * h ∈ youngSubgroup μ) : ((tabloidForm μ) (MonoidAlgebra.single (↑g) 1)) (MonoidAlgebra.single (↑h) 1) = 1

Two permutations describe the same μ-tabloid exactly when they differ by an element of the Young subgroup, and then the corresponding basis vectors pair to 1.

theorem TauCeti.tabloidForm_single_coe_single_coe_of_notMem {n : ℕ} (μ : n.Partition) {g h : Equiv.Perm (Fin n)} (hgh : g⁻¹ * h ∉ youngSubgroup μ) : ((tabloidForm μ) (MonoidAlgebra.single (↑g) 1)) (MonoidAlgebra.single (↑h) 1) = 0

Permutations lying in different cosets of the Young subgroup describe distinct μ-tabloids, so the corresponding basis vectors pair to 0.

theorem TauCeti.tabloidForm_invariant {n : ℕ} (μ : n.Partition) (σ : Equiv.Perm (Fin n)) (v w : MonoidAlgebra ℚ (Equiv.Perm (Fin n) ⧸ youngSubgroup μ)) : ((tabloidForm μ) (((permutationModule μ).ρ σ) v)) (((permutationModule μ).ρ σ) w) = ((tabloidForm μ) v) w

The symmetric group acts on M^μ by isometries of the tabloid form: it permutes the tabloid basis.

theorem TauCeti.isCompl_orthogonalSubrepresentation_permutationModule {n : ℕ} (μ : n.Partition) (σ : Subrepresentation (permutationModule μ).ρ) : IsCompl σ (orthogonalSubrepresentation σ)

Invariant orthogonal complements in M^μ. A subrepresentation of the Young permutation module is complemented by its orthogonal complement for the tabloid form. Unlike the complement produced by Maschke's theorem, this one is canonical: it is cut out by an explicit pairing.