Characters of representations #
This file introduces characters of representation and proves basic lemmas about how characters behave under various operations on representations.
A key result is the orthogonality of characters for irreducible representations of finite group
over an algebraically closed field whose characteristic doesn't divide the order of the group. It
is the theorem char_orthonormal
Implementation notes #
Irreducible representations are implemented categorically, using the CategoryTheory.Simple
class
defined in Mathlib.CategoryTheory.Simple
TODO #
- Once we have the monoidal closed structure on
FdRep k G
and a better API for the rigid structure,char_dual
andchar_linHom
should probably be stated in terms ofVᘁ
andihom V W
.
If V
are W
are finite-dimensional representations of a finite group, then the
scalar product of their characters is equal to the dimension of the space of
equivariant maps from V
to W
.
Orthogonality of characters for irreducible representations of finite group over an algebraically closed field whose characteristic doesn't divide the order of the group.