Goal
Define the complex character table of a finite group G (the square array of irreducible complex character values on conjugacy-class representatives) and the rational character table (grouping Galois-conjugate characters).
What already exists
- mathlib: representation theory (
FDRep, Representation), class functions and characters (FDRep.character), orthogonality of characters, conjugacy classes (ConjClasses), Monoid.exponent. The theory is largely present; the computed table object is not.
What's missing
characterTable G : Matrix (Irr G) (ConjClasses G) ℂ (rows = irreducibles, columns = classes), the column/row orthogonality relations as matrix statements, and the rational character table (sums over Galois orbits of irreducibles).
Test cases
C_n, S_3, S_4, Q_8, A_5 — known character tables.
LMFDB targets
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Define the complex character table of a finite group
G(the square array of irreducible complex character values on conjugacy-class representatives) and the rational character table (grouping Galois-conjugate characters).What already exists
FDRep,Representation), class functions and characters (FDRep.character), orthogonality of characters, conjugacy classes (ConjClasses),Monoid.exponent. The theory is largely present; the computed table object is not.What's missing
characterTable G : Matrix (Irr G) (ConjClasses G) ℂ(rows = irreducibles, columns = classes), the column/row orthogonality relations as matrix statements, and the rational character table (sums over Galois orbits of irreducibles).Test cases
C_n,S_3,S_4,Q_8,A_5— known character tables.LMFDB targets
group.complex_character_tablegroup.conjugacy_classgroup.label_complex_group_charNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.