Class functions give central elements

The group-algebra element attached to a conjugation-invariant coefficient function is central — pure coefficient algebra, no representation theory.

noncomputable def RS.classElem {G : Type u_1} [Group G] [Fintype G] (c : G → ℂ) : MonoidAlgebra ℂ G

The group-algebra element attached to a coefficient function.

Equations

• RS.classElem c = ∑ g : G, c g • MonoidAlgebra.single g 1

theorem RS.classElem_coeff {G : Type u_1} [Group G] [Fintype G] (c : G → ℂ) (k : G) : (classElem c).coeff k = c k

The element built from a coefficient function has exactly those coefficients.

theorem RS.classElem_mul_comm {G : Type u_1} [Group G] [Fintype G] (c : G → ℂ) (hc : ∀ (g h : G), c (h * g * h⁻¹) = c g) (y : MonoidAlgebra ℂ G) : classElem c * y = y * classElem c

Class functions give central elements.