# Documentation

Mathlib.RepresentationTheory.Character

# 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 and char_linHom should probably be stated in terms of Vᘁ and ihom V W.
def FdRep.character {k : Type u} [] {G : Type u} [] (V : FdRep k G) (g : G) :
(fun x => k) (↑() g)

The character of a representation V : FdRep k G is the function associating to g : G the trace of the linear map V.ρ g.

Instances For
theorem FdRep.char_mul_comm {k : Type u} [] {G : Type u} [] (V : FdRep k G) (g : G) (h : G) :
@[simp]
theorem FdRep.char_one {k : Type u} [] {G : Type u} [] (V : FdRep k G) :
= ↑()
theorem FdRep.char_tensor {k : Type u} [] {G : Type u} [] (V : FdRep k G) (W : FdRep k G) :

The character is multiplicative under the tensor product.

@[simp]
theorem FdRep.char_tensor' {k : Type u} [] {G : Type u} [] (V : FdRep k G) (W : FdRep k G) :
FdRep.character (Action.FunctorCategoryEquivalence.inverse.obj (CategoryTheory.MonoidalCategory.tensorObj (Action.FunctorCategoryEquivalence.functor.obj V) (Action.FunctorCategoryEquivalence.functor.obj W))) =
theorem FdRep.char_iso {k : Type u} [] {G : Type u} [] {V : FdRep k G} {W : FdRep k G} (i : V W) :

The character of isomorphic representations is the same.

@[simp]
theorem FdRep.char_conj {k : Type u} [] {G : Type u} [] (V : FdRep k G) (g : G) (h : G) :

The character of a representation is constant on conjugacy classes.

@[simp]
theorem FdRep.char_dual {k : Type u} [] {G : Type u} [] (V : FdRep k G) (g : G) :
=
@[simp]
theorem FdRep.char_linHom {k : Type u} [] {G : Type u} [] (V : FdRep k G) (W : FdRep k G) (g : G) :
theorem FdRep.average_char_eq_finrank_invariants {k : Type u} [] {G : Type u} [] [] [] (V : FdRep k G) :
(↑() Finset.sum Finset.univ fun g => ) = ↑(FiniteDimensional.finrank k { x // })
theorem FdRep.char_orthonormal {k : Type u} [] {G : GroupCat} [] [Fintype G] [Invertible ↑()] (V : FdRep k G) (W : FdRep k G) :
(↑() Finset.sum Finset.univ fun g => ) = if Nonempty (V W) then 1 else 0

Orthogonality of characters for irreducible representations of finite group over an algebraically closed field whose characteristic doesn't divide the order of the group.