Structure constants of the class algebra

For conjugacy classes Cᵢ, Cⱼ, and Cₖ of a finite group, the structure constant structureConstant Cᵢ Cⱼ Cₖ counts factorizations x * y = g, where x ∈ Cᵢ, y ∈ Cⱼ, and g is any representative of Cₖ. Conjugating both factors proves that this count is independent of the representative.

These natural numbers are the coefficients for multiplication in the class-sum basis of the center of the group algebra. They are the integral input to the Dixon--Schneider character-table algorithm. The class of 1 is a unit for them (TauCeti.structureConstant_mk_one_right), since its class sum is the unit of the group algebra.

def TauCeti.structureConstant {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cⱼ Cₖ : ConjClasses G) : ℕ

The number of factorizations x * y = g, for x ∈ Cᵢ, y ∈ Cⱼ, and any representative g of Cₖ. This is independent of the representative by simultaneous conjugation.

Equations

• TauCeti.structureConstant Cᵢ Cⱼ Cₖ = Quotient.liftOn Cₖ (fun (g : G) => Fintype.card (TauCeti.StructureConstantFiber✝ Cᵢ Cⱼ g)) ⋯

@[simp]

theorem TauCeti.structureConstant_mk {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cⱼ : ConjClasses G) (g : G) : structureConstant Cᵢ Cⱼ (ConjClasses.mk g) = {p ∈ Finset.univ ×ˢ Finset.univ | ↑p.1 * ↑p.2 = g}.card

The structure constant at the conjugacy class of g counts the corresponding factorizations of g.

theorem TauCeti.classSum_mul {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [Semiring k] (Cᵢ Cⱼ : ConjClasses G) : classSum k Cᵢ * classSum k Cⱼ = ∑ Cₖ : ConjClasses G, ↑(structureConstant Cᵢ Cⱼ Cₖ) • classSum k Cₖ

Multiplication of class sums is governed by the structure constants.

theorem TauCeti.classSumCenter_mul {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [CommSemiring k] (Cᵢ Cⱼ : ConjClasses G) : classSumCenter Cᵢ * classSumCenter Cⱼ = ∑ Cₖ : ConjClasses G, ↑(structureConstant Cᵢ Cⱼ Cₖ) • classSumCenter Cₖ

The coordinate identity: multiplication of class sums inside the centre of the group algebra expands in the class-sum basis with the structure constants as coefficients. This is TauCeti.classSum_mul read in the centre, where the class sums are a basis.

theorem TauCeti.coeff_classSum_mul {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [Semiring k] (Cᵢ Cⱼ : ConjClasses G) (g : G) : (classSum k Cᵢ * classSum k Cⱼ).coeff g = ↑(structureConstant Cᵢ Cⱼ (ConjClasses.mk g))

The coefficient of g in a product of two class sums is the structure constant at the conjugacy class of g. This is the pointwise form of TauCeti.classSum_mul.

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

The structure constants are symmetric in their two class arguments, because the two class sums commute in the group algebra.

@[simp]

theorem TauCeti.structureConstant_mk_one_right {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cₖ : ConjClasses G) : structureConstant Cᵢ (ConjClasses.mk 1) Cₖ = if Cₖ = Cᵢ then 1 else 0

The class of 1 is a unit for the structure constants: because K_{Cᵢ} · K_{[1]} = K_{Cᵢ}, the constant aᵢ,[1],ₖ is 1 when Cₖ = Cᵢ and 0 otherwise.

@[simp]

theorem TauCeti.structureConstant_mk_one_left {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cⱼ Cₖ : ConjClasses G) : structureConstant (ConjClasses.mk 1) Cⱼ Cₖ = if Cₖ = Cⱼ then 1 else 0

The symmetric companion of TauCeti.structureConstant_mk_one_right.

theorem TauCeti.structureConstant_mk_eq_card_filter {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (Cᵢ Cⱼ : ConjClasses G) (g : G) : structureConstant Cᵢ Cⱼ (ConjClasses.mk g) = {q : G × G | ConjClasses.mk q.1 = Cᵢ ∧ ConjClasses.mk q.2 = Cⱼ ∧ q.1 * q.2 = g}.card

The structure constant at the class of g, as a count of pairs of group elements: the pairs (x, y) in G × G with x in Cᵢ, y in Cⱼ and x * y = g. This is TauCeti.structureConstant_mk with the membership in the two class carriers turned into conditions on a pair of group elements, so that it can be compared with, or computed alongside, other counts indexed by G.