The class-multiplication matrices of a finite group

The centre of the group algebra k[G] of a finite group has the class sums K_C as a k-basis (TauCeti.classSumBasis), and multiplication in that basis is described by the structure constants aᵢⱼₖ (TauCeti.structureConstant). This file records the matrices of that multiplication.

The class-multiplication matrix classMultMatrix Cᵢ is the integer matrix with entries (Mᵢ)ⱼₖ = aᵢₖⱼ. The index order is not an accident: it makes Mᵢ exactly the matrix of left multiplication by K_{Cᵢ} on the centre, taken in the class-sum basis, which is Mathlib's Algebra.leftMulMatrix. That identification (TauCeti.classMultMatrix_map_intCast) is the content of the file, and everything else follows from it:

• TauCeti.classMultMatrix_commute: the matrices Mᵢ commute pairwise, because the centre is a commutative ring and Algebra.leftMulMatrix is an algebra homomorphism;
• TauCeti.classMultMatrix_injective: distinct classes give distinct matrices;
• TauCeti.classMultMatrix_mk_one: the matrix at the class of 1 is the identity matrix;
• TauCeti.classMultMatrix_mulVec: Mᵢ acts on the coordinate vector of a central element by multiplication by K_{Cᵢ}.

Since TauCeti.structureConstant is a genuine def on [Fintype G] [DecidableEq G] data, so is classMultMatrix; these integers and matrices are the whole input to the Burnside--Dixon--Schneider character-table algorithm. The eigenvector orientation there is pinned, and the index order above is what pins it: writing vⱼ = ω(K_{Cⱼ}) for the values of a central character on the class sums, the row vector v is a common left eigenvector of the family {Mᵢ}, acting from the left via Matrix.vecMul (ᵥ*), with v ᵥ* Mᵢ = ω(K_{Cᵢ}) • v. It is not a column eigenvector under Matrix.mulVec (*ᵥ): that convention would require the transposed matrix aᵢⱼₖ instead. The *ᵥ action recorded below in TauCeti.classMultMatrix_mulVec is a different statement — that Mᵢ carries class-sum coordinates to the coordinates of the product, which is exactly what makes Mᵢ a matrix of left multiplication — and not an eigenvector relation. The eigenvector theorem itself needs central characters, so it is deferred to the layer that constructs them.

References

This implements the object classMultMatrix and the milestone classMultMatrix_commute of Layer 5 of the character theory roadmap and its suggested declarations.

theorem TauCeti.leftMulMatrix_classSumCenter_apply {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [CommSemiring k] (Cᵢ Cⱼ Cₖ : ConjClasses G) : (Algebra.leftMulMatrix classSumBasis) (classSumCenter Cᵢ) Cⱼ Cₖ = ↑(structureConstant Cᵢ Cₖ Cⱼ)

The structure constants are the matrix of multiplication by a class sum, entrywise: the matrix of left multiplication by K_{Cᵢ} on the centre of k[G], in the class-sum basis, has (Cⱼ, Cₖ) entry aᵢₖⱼ.

def TauCeti.classMultMatrix {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ : ConjClasses G) : Matrix (ConjClasses G) (ConjClasses G) ℤ

The class-multiplication matrix of a conjugacy class Cᵢ of a finite group: the integer matrix with (Cⱼ, Cₖ) entry the structure constant aᵢₖⱼ.

The transposed index order is fixed so that classMultMatrix Cᵢ is the matrix of left multiplication by the class sum K_{Cᵢ} on the centre of the group algebra, taken in the class-sum basis (TauCeti.classMultMatrix_map_intCast).

Equations

• TauCeti.classMultMatrix Cᵢ = Matrix.of fun (Cⱼ Cₖ : ConjClasses G) => ↑(TauCeti.structureConstant Cᵢ Cₖ Cⱼ)

@[simp]

theorem TauCeti.classMultMatrix_apply {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cⱼ Cₖ : ConjClasses G) : classMultMatrix Cᵢ Cⱼ Cₖ = ↑(structureConstant Cᵢ Cₖ Cⱼ)

theorem TauCeti.classMultMatrix_map_intCast {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [CommRing k] (Cᵢ : ConjClasses G) : (classMultMatrix Cᵢ).map Int.cast = (Algebra.leftMulMatrix classSumBasis) (classSumCenter Cᵢ)

The class-multiplication matrix is the matrix of multiplication by the class sum: pushing classMultMatrix Cᵢ into any commutative ring k gives the matrix of left multiplication by K_{Cᵢ} on the centre of k[G], taken in the class-sum basis.

theorem TauCeti.classMultMatrix_eq_leftMulMatrix {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ : ConjClasses G) : classMultMatrix Cᵢ = (Algebra.leftMulMatrix classSumBasis) (classSumCenter Cᵢ)

The class-multiplication matrix over ℤ is itself a matrix of multiplication by a class sum, namely in the centre of the integral group algebra ℤ[G].

theorem TauCeti.classMultMatrix_commute {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cⱼ : ConjClasses G) : Commute (classMultMatrix Cᵢ) (classMultMatrix Cⱼ)

The class-multiplication matrices commute pairwise. They are the images of the class sums under an algebra homomorphism out of the centre of ℤ[G], which is commutative.

theorem TauCeti.classMultMatrix_injective {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] : Function.Injective classMultMatrix

Distinct conjugacy classes have distinct class-multiplication matrices: multiplication by a class sum determines it, and the class sums are a basis of the centre.

@[simp]

theorem TauCeti.classMultMatrix_mk_one {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] : classMultMatrix (ConjClasses.mk 1) = 1

The class-multiplication matrix at the conjugacy class of 1 is the identity matrix: the class sum of {1} is the unit of the group algebra.

theorem TauCeti.classMultMatrix_mulVec {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [CommRing k] (Cᵢ : ConjClasses G) (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) : ((classMultMatrix Cᵢ).map Int.cast).mulVec (centerToConjClasses z) = centerToConjClasses (classSumCenter Cᵢ * z)

The class-multiplication matrix acts by multiplication by the class sum: it sends the vector of class-sum coordinates of a central element z to the coordinates of K_{Cᵢ} * z.

This *ᵥ action is the defining property of a matrix of left multiplication; it is not the pinned eigenvector relation, which is a ᵥ* action on the central-character row vectors.