The specification a character table satisfies, and the labeled uniqueness it forces #

Let G be a finite group. Its complex character table TauCeti.characterTable ℂ G is a square matrix whose rows are indexed by an arbitrary enumeration of the irreducible characters and whose columns are labeled by the conjugacy classes themselves. This file writes down a property TauCeti.IsCharacterTableSpec of an arbitrary such matrix, proves that the character table has it, and proves that it pins the character table down: any matrix with this property is the character table up to a permutation of its rows.

The property is the checker of the Burnside--Dixon--Schneider algorithm. Its three ingredients are the data that algorithm produces and can verify without knowing any representation theory:

the identity column consists of positive integers dividing |G| whose squares sum to |G|;
the rows are orthonormal for the class-size weighted Hermitian pairing;
each normalized row ω_i(K_C) = |C| · M i C / M i 1 (TauCeti.centralCharacterRow) is a common left eigenrow of the class-multiplication matrices, the eigenvalue at C being its own value there.

Uniqueness is the reason this is worth having: an algorithm that returns a matrix passing the checker has returned the character table. The proof matches each normalized row with a row of the central character table Ω (TauCeti.isClassEigenrow_iff_exists_centralCharacterTable_eq, which identifies the normalized common left eigenrows with the central characters of the irreducibles), recovers the degree of that irreducible from the self-pairing of the row, and reads the ordinary row off Ω by TauCeti.characterTable_eq_div. Distinct rows of the matrix stay distinct because orthonormality forbids repetitions, so the matching is a permutation.

Main definitions #

TauCeti.centralCharacterRow: the normalized row ω_i of a candidate character table.
TauCeti.IsCharacterTableSpec: the specification itself.

Main results #

TauCeti.isCharacterTableSpec_characterTable: the character table satisfies the specification.
TauCeti.characterTable_unique_rows: labeled uniqueness, a matrix satisfying the specification is the character table up to a permutation of rows. With TauCeti.IsCharacterTableSpec.submatrix, that a row permutation preserves the specification, this becomes the characterization TauCeti.isCharacterTableSpec_iff_exists_perm of the matrices satisfying it, and TauCeti.IsCharacterTableSpec.exists_perm_eq: any two of them differ by a permutation of rows.
TauCeti.IsCharacterTableSpec.sum_apply_mk_one_eq_sum_characterDegree: the identity column of such a matrix sums to the sum of the character degrees.
TauCeti.IsCharacterTableSpec.exists_eq_characterTable: the row-by-row form of uniqueness, that every row is a row of the character table.

Implementation notes #

The specification is stated over ℂ, where the roadmap pins it: its orthonormality condition is the Hermitian one, which is the form the algorithm checks. The normalized row TauCeti.centralCharacterRow needs no such restriction and is defined over any field, so that TauCeti.centralCharacterRow_characterTable (the normalized rows of the character table are the rows of the central character table) is available wherever the two tables are. Normalizing reads only the row it is given, so it is also defined for a matrix with any row index type, and only TauCeti.centralCharacterRow_characterTable and the specification itself ask for the character table's.

The group is an explicit argument of TauCeti.IsCharacterTableSpec, as the roadmap pins it: the specification is read as a statement about G, and IsCharacterTableSpec G M says what it says without having to recover G from the type of M.

Three of the four conditions do the work in TauCeti.characterTable_unique_rows: the positivity and integrality of the degrees, row orthonormality, and the eigenrow condition. The divisibility dᵢ ∣ |G| and the identity ∑ dᵢ² = |G| are part of the checker as the roadmap pins it, being what the algorithm tests after the eigenvector search and before lifting; they are recorded here because the character table satisfies them, not because uniqueness needs them.

References #

This is the specification and the labeled uniqueness of Layer 5 of the character theory roadmap (IsCharacterTableSpec, isCharacterTableSpec_characterTable and characterTable_unique_rows in that roadmap's Suggested.lean). See J. D. Dixon, High speed computation of group characters, Numer. Math. 10 (1967) 446-450, and I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 3.