Brauer character basis theorem (source code)

= Brauer character basis theorem
{c}

Over a <splitting field for finite group representations> of characteristic $p$, the irreducible <Brauer characters> form a complex basis of the <class functions> on the <p-regular elements>. Independence is the character form of the <Brauer–Nesbitt theorem>. To obtain spanning, extend such a class function by zero on the p-singular classes. Ordinary irreducible characters form a basis of all class functions by <character orthogonality>. Restricting them to p-regular elements yields Brauer characters of reductions of an <integral form of a group representation> in a compatible splitting <p-modular system>; if needed, first extend scalars, which does not change the simple-module list under the splitting hypothesis. Each restriction is a nonnegative integral sum of simple Brauer characters by exact-sequence additivity and the <Jordan–Hölder theorem>. Thus these restrictions span, proving the assertion. Consequently the number of simple modules equals the number of p-regular conjugacy classes, and evaluation identifies the complexified <modular representation ring> with the product of one copy of $\mathbb C$ for each such class.