Definition. characters, class functions, and the character table [fgap-001M]
✍️source
basisOfIrreducibleCharacters characterTable card_inv_mul_sum_characterTable_mul_characterTable_inv card_conjClass_mul_sum_characterTable_mul_characterTable_inv
L∃∀N

For a finite-dimensional representation \(\rho \) over a characteristic-zero field, its character is \(\chi _\rho (g)=\operatorname {tr}(\rho (g))\). Trace is unchanged by conjugation, so \(\chi _\rho \) is a class function. A character table places the irreducible characters in rows and the conjugacy classes in columns. Tau Ceti identifies class functions with functions on conjugacy classes in TauCeti.ClassFunction.equivConjClasses.

Over \(\mathbb C\), the irreducible characters form an orthonormal basis of the class functions. Thus the table is square: the number of irreducible characters equals the number of conjugacy classes. This also counts the Wedderburn blocks and gives the dimension of the center. See [james2001representations, thm. 16.4, pp. 159--166].

Definition. characters, class functions, and the character table [fgap-001M]
✍️source
basisOfIrreducibleCharacters characterTable card_inv_mul_sum_characterTable_mul_characterTable_inv card_conjClass_mul_sum_characterTable_mul_characterTable_inv
L∃∀N

Reference. Representations and characters of groups [james2001representations]

The human-curated Group-Algebra route [fgap-001G]
📄PDF

Definition. the Group Algebra and its universal extension [fgap-001H]

MonoidAlgebra.lift MonoidAlgebra.lift_single
L∃∀N

Theorem. representations are Group-Algebra modules [fgap-001I]

Representation.asModule Representation.ofModule Rep.equivalenceModuleMonoidAlgebra
L∃∀N

Proof.

Example. the regular representation reads the basis [fgap-001J]

Theorem. Maschke averaging [fgap-001K]

MonoidAlgebra.Submodule.exists_isCompl
L∃∀N

Proof.

Theorem. Wedderburn blocks over an algebraically closed field [fgap-001L]

exists_algEquiv_pi_matrix_conjClasses
L∃∀N

Definition. characters, class functions, and the character table [fgap-001M]
✍️source
basisOfIrreducibleCharacters characterTable card_inv_mul_sum_characterTable_mul_characterTable_inv card_conjClass_mul_sum_characterTable_mul_characterTable_inv
L∃∀N

Theorem. primitive central idempotents as block projectors [fgap-001N]

primitiveCentralIdempotent asAlgebraHom_primitiveCentralIdempotent primitiveCentralIdempotent_mul_primitiveCentralIdempotent
L∃∀N

Theorem. the Frobenius--Schur trichotomy [fgap-0021]

frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one frobeniusSchurIndicator_eq_one_iff frobeniusSchurIndicator_eq_neg_one_iff frobeniusSchurIndicator_eq_zero_iff
L∃∀N

Remark. real types are not Schur indices [fgap-001Y]

Definition. conjugate constituents and the inertia subgroup [fgap-001O]

Theorem. the single orbit in Clifford restriction [fgap-001P]

isSemisimpleRepresentation_comp_subtype exists_isAtom_forall_nonempty_linearEquiv_conjSubrep
L∃∀N

Theorem. Clifford homogeneity and the semidirect route [fgap-001Q]

Example. semidirect products make Clifford theory concrete [fgap-0020]

Remark. from a presentation to checked representation data [fgap-001R]

Definition. factor sets and twisted Group Algebras [fgap-001S]

of_mul_of lift isProjectiveRepEquivAlgHom
L∃∀N

Remark. the qualified Clifford bridge [fgap-001Z]

Remark. the inertia obstruction is projective [fgap-001T]

proposition. the canonical grading of a Group Algebra [fgap-001U]

AddMonoidAlgebra.grade.isInternal AddMonoidAlgebra.grade.gradedAlgebra AddMonoidAlgebra.single_mem_grade
L∃∀N

proposition. the standard Hopf structure on a Group Algebra [fgap-001V]

MonoidAlgebra.instHopfAlgebra MonoidAlgebra.counit_single MonoidAlgebra.comul_single MonoidAlgebra.antipode_single
L∃∀N

Proof.

Remark. what the real quaternion example settles [fgap-001W]

Remark. the Hessian-group outlook [fgap-001X]