Class sums in a finite group algebra

This file defines the element of a group algebra obtained by summing the members of a conjugacy class. It proves that every class sum is central, the first input to the class-algebra side of finite-group character theory.

noncomputable def TauCeti.classSum {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [Semiring k] (C : ConjClasses G) : MonoidAlgebra k G

The sum in k[G] of the elements in the conjugacy class C.

Equations

• TauCeti.classSum k C = ∑ x : ↑C.carrier, (MonoidAlgebra.of k G) ↑x

theorem TauCeti.classSum_eq_sum {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {k : Type u_2} [Semiring k] (C : ConjClasses G) : classSum k C = ∑ x : ↑C.carrier, (MonoidAlgebra.of k G) ↑x

A class sum is the sum of the basis elements in its conjugacy class.

@[simp]

theorem TauCeti.classSum_coeff {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {k : Type u_2} [Semiring k] (C : ConjClasses G) (g : G) : (classSum k C).coeff g = if ConjClasses.mk g = C then 1 else 0

The coefficient of g in the class sum of C is 1 if g lies in C, and 0 otherwise.

def TauCeti.conjugateCarrierEquiv {G : Type u_1} [Group G] (g : G) (C : ConjClasses G) : ↑C.carrier ≃ ↑C.carrier

Conjugation by g permutes every conjugacy class.

Equations

• TauCeti.conjugateCarrierEquiv g C = { toFun := fun (x : ↑C.carrier) => ⟨g * ↑x * g⁻¹, ⋯⟩, invFun := fun (x : ↑C.carrier) => ⟨g⁻¹ * ↑x * g, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.conjugateCarrierEquiv_apply {G : Type u_1} [Group G] (g : G) (C : ConjClasses G) (x : ↑C.carrier) : ↑((conjugateCarrierEquiv g C) x) = g * ↑x * g⁻¹

conjugateCarrierEquiv g C sends x to its conjugate g * x * g⁻¹.

theorem TauCeti.classSum_commutes {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {k : Type u_2} [Semiring k] (C : ConjClasses G) (g : G) : classSum k C * (MonoidAlgebra.of k G) g = (MonoidAlgebra.of k G) g * classSum k C

A class sum commutes with each group element in the group algebra.

@[simp]

theorem TauCeti.classSum_mk_one {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [Semiring k] : classSum k (ConjClasses.mk 1) = 1

The class sum of the conjugacy class of 1 is the unit of the group algebra: that class is the singleton {1} (TauCeti.ConjClasses.carrier_mk_one).

theorem TauCeti.classSum_mem_center {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (k : Type u_2) [CommSemiring k] (C : ConjClasses G) : classSum k C ∈ Subalgebra.center k (MonoidAlgebra k G)

Every class sum lies in the center of the group algebra.