The eigenrows of the class-multiplication matrices are the central characters #

Let G be a finite group and k an algebraically closed field in which |G| is invertible. The class sums K_C are a basis of the centre Z(k[G]), and the class-multiplication matrices Mᵢ record multiplication by K_{Cᵢ} in that basis. A normalized common left eigenrow of the family {Mᵢ} is a function v on the conjugacy classes with v (ConjClasses.mk 1) = 1 and v ᵥ* Mᵢ = v Cᵢ • v for every class; TauCeti.isClassEigenrow_iff_exists_algHom identifies these with the k-algebra homomorphisms Z(k[G]) →ₐ[k] k, by a computation inside the class algebra that knows nothing about representations.

This file supplies the representation theory that computation is missing: those algebra homomorphisms are exactly the central characters ωᵪ of the irreducible representations of G. Collecting their values on the class sums gives the central character table TauCeti.centralCharacterTable k G, the matrix Ω of the Burnside--Dixon--Schneider algorithm, and TauCeti.isClassEigenrow_iff_exists_centralCharacterTable_eq says that its rows are precisely the normalized common left eigenrows. So an eigenrow computed from the structure constants alone is a central character, and there are exactly as many of them as G has conjugacy classes.

The proof runs through a Wedderburn presentation k[G] ≃ₐ[k] ∏ᵢ Matₙᵢ(k). Such a presentation splits the centre as the product algebra ∏ᵢ k (TauCeti.centerMonoidAlgebraAlgEquivPi), whose only algebra homomorphisms to k are the coordinate evaluations (AlgHom.eq_piEvalAlgHom); the evaluation at a block is the central character of the representation that block carries (TauCeti.centralCharacter_blockRepresentation), and every irreducible representation is equivalent to a block, hence has the same central character as one.

Main definitions #

TauCeti.centralCharacterTable: the central character table Ω of G.
TauCeti.finEquivCentralCharacter: the enumeration of the algebra homomorphisms out of Z(k[G]) by the irreducible representations, and TauCeti.finEquivEigenrow, the same for the normalized common left eigenrows.
TauCeti.basisCentralCharacterTable: the rows of Ω, as a basis of the functions on the conjugacy classes.

Main statements #

TauCeti.exists_centralCharacter_eq: every algebra homomorphism out of the centre is a central character, and TauCeti.centralCharacter_irreducibleRepresentation_injective: distinct irreducibles have distinct central characters.
TauCeti.isClassEigenrow_iff_exists_centralCharacterTable_eq: the normalized common left eigenrows of the class-multiplication matrices are exactly the rows of Ω, and TauCeti.card_normalized_isClassEigenrow: there are as many of them as conjugacy classes. The version requiring only a split centre is TauCeti.card_normalized_isClassEigenrow_of_nonempty_center_algEquiv. Dropping the normalization only adds scalar multiples: TauCeti.exists_eq_smul_centralCharacterTable says every nonzero common left eigenvector of the class-multiplication matrices is a multiple of a row of Ω, and TauCeti.linearIndependent_centralCharacterTable says those rows are linearly independent, hence a basis.
TauCeti.eq_of_centralCharacter_eq: the central characters separate the points of the centre.
TauCeti.centralCharacterTable_mul_characterDegree: the conversion ωᵪ(K_C) · χ(1) = |C| · χ(g) between Ω and the ordinary character table TauCeti.characterTable, with the two quotient forms TauCeti.centralCharacterTable_eq_div and TauCeti.characterTable_eq_div reading each table off the other.

Implementation notes #

The rows of Ω are indexed by the same enumeration TauCeti.finEquivIrreducibleCharacters of the irreducible characters as the rows of TauCeti.characterTable, so the two tables are aligned row by row and TauCeti.centralCharacterTable_mul_characterDegree converts between them entry by entry.

That conversion is stated without division, so it holds over every algebraically closed field in which |G| is invertible. Dividing it out in either direction needs the corresponding factor to be invertible: TauCeti.characterTable_eq_div divides by the class size |C|, which the standing hypotheses already make invertible, while TauCeti.centralCharacterTable_eq_div divides by the degree χ(1) and so takes its nonvanishing as an explicit hypothesis rather than assuming characteristic zero.

TauCeti.centralCharacter_blockRepresentation carries the irreducibility of the block as an instance argument rather than deriving it: the central character is only defined for an irreducible representation, and irreducibility of a block is the theorem TauCeti.isIrreducible_blockRepresentation, which mentions the chosen presentation e and so cannot be an instance. Callers supply it with have := isIrreducible_blockRepresentation e i.

References #

This is the step that Layer 5 of the character theory roadmap calls for after normalized_eigenrow_iff_algHom: the identification of the algebra homomorphisms out of the centre with the central characters, and the central table Ω itself. See I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 3, or J. D. Dixon, High speed computation of group characters, Numer. Math. 10 (1967).