Characters of representations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file introduces characters of representation and proves basic lemmas about how characters
behave under various operations on representations.
- Once we have the monoidal closed structure on
fdRep k G and a better API for the rigid
char_lin_hom should probably be stated in terms of
ihom V W.
The character of a representation
V : fdRep k G is the function associating to
g : G the
trace of the linear map
The character is multiplicative under the tensor product.
The character of isomorphic representations is the same.
The character of a representation is constant on conjugacy classes.
Orthogonality of characters for irreducible representations of finite group over an
algebraically closed field whose characteristic doesn't divide the order of the group.