In a sense, group algebras are the source of all you need to know about representation theory.

The primary reference is [james2001representations] for understanding FG-module, Group algebra, the presentation of groups, Clifford theory (which is the standard method of constructing representations and characters of semi-direct products, see [woit2017quantum], and "3.6 Clifford theory" in [lux2010representations]), Schur indices etc. We also need to check [lux2010representations] for its introduction to GAP, and we should pay close attention to the progress of GAP-LEAN. [sims1994computation] might also be interesting in a similar manner as [lux2010representations] but with emphasis on the presentation of groups.

See also group algebra on nlab, particularly that "A group algebra is in particular a Hopf algebra and a \(G\)-graded algebra."

The related Zulip thread is here, and I have preliminary explorations and experiments in Lean here.

This interest originates from reading Robert A. Wilson's work [wilson2024discrete]. The ultimate goal is to understand the group algebra of the binary tetrahedral group (\(Q_8 \rtimes Z_3\)), then the three-dimensional complex reflection group (\(G_{27} \rtimes Q_8 \rtimes Z_3\)), a.k.a. the triple cover of the Hessian group, which can be interpreted as a finite analogue of the complete gauge group \(U(1) \times SU(2) \times SU(3)\).

A further neccecity arises from reading [hamilton2023supergeometric] and [hamilton2023unification].