Characters of representations #
This file introduces characters of representation and proves basic lemmas about how characters behave under various operations on representations.
TODO #
- Once we have the monoidal closed structure on
fdRep k G
and a better API for the rigid structure,char_dual
andchar_lin_hom
should probably be stated in terms ofVᘁ
andihom V W
.
@[simp]
theorem
fdRep.char_one
{k G : Type u}
[field k]
[monoid G]
(V : fdRep k G) :
V.character 1 = ↑(finite_dimensional.finrank k ↥V)
theorem
fdRep.average_char_eq_finrank_invariants
{k G : Type u}
[field k]
[group G]
[fintype G]
[invertible ↑(fintype.card G)]
(V : fdRep k G) :
⅟ ↑(fintype.card G) • finset.univ.sum (λ (g : G), V.character g) = ↑(finite_dimensional.finrank k ↥(representation.invariants V.ρ))