Documentation

TauCeti.RepresentationTheory.Symmetric.Specht.Basis

The Specht character basis #

The characters of the complex Specht modules form a basis of the class functions of Sₙ. This uses their irreducibility and pairwise distinctness, together with the correspondence between partitions and conjugacy classes.

source
noncomputable def TauCeti.spechtCharacterBasis (n : ℕ) :
Module.Basis n.Partition ℂ ↥(ClassFunction ℂ (Equiv.Perm (Fin n)))

The complex Specht characters give every class function on Sₙ a unique expansion.

Instances For
    source
    @[simp]
    theorem TauCeti.spechtCharacterBasis_apply {n : ℕ} (μ : n.Partition) :
    (spechtCharacterBasis n) μ = ClassFunction.ofCharacter (spechtModuleℂ μ).ρ

    The μ-th vector in the class-function basis is the character of the complex Specht module S^μ.

    source
    @[simp]
    theorem TauCeti.spechtCharacterBasis_repr {n : ℕ} (f : ↥(ClassFunction ℂ (Equiv.Perm (Fin n)))) (μ : n.Partition) :
    ((spechtCharacterBasis n).repr f) μ = (ClassFunction.characterPairing (ClassFunction.ofCharacter (spechtModuleℂ μ).ρ)) f

    The coordinate of a class function at a Specht character is its character pairing with that character.