# 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`

.

theorem
FdRep.char_mul_comm
{k : Type u}
[Field k]
{G : Type u}
[Monoid G]
(V : FdRep k G)
(g : G)
(h : G)
:

FdRep.character V (h * g) = FdRep.character V (g * h)

@[simp]

theorem
FdRep.char_one
{k : Type u}
[Field k]
{G : Type u}
[Monoid G]
(V : FdRep k G)
:

FdRep.character V 1 = ↑(FiniteDimensional.finrank k (CoeSort.coe V))

@[simp]

theorem
FdRep.char_tensor'
{k : Type u}
[Field k]
{G : Type u}
[Monoid G]
(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))) = FdRep.character V * FdRep.character W

@[simp]

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

FdRep.character V (h * g * h⁻¹) = FdRep.character V g

The character of a representation is constant on conjugacy classes.

@[simp]

theorem
FdRep.char_dual
{k : Type u}
[Field k]
{G : Type u}
[Group G]
(V : FdRep k G)
(g : G)
:

FdRep.character (FdRep.of (Representation.dual (FdRep.ρ V))) g = FdRep.character V g⁻¹

@[simp]

theorem
FdRep.char_linHom
{k : Type u}
[Field k]
{G : Type u}
[Group G]
(V : FdRep k G)
(W : FdRep k G)
(g : G)
:

FdRep.character (FdRep.of (Representation.linHom (FdRep.ρ V) (FdRep.ρ W))) g = FdRep.character V g⁻¹ * FdRep.character W g

theorem
FdRep.average_char_eq_finrank_invariants
{k : Type u}
[Field k]
{G : Type u}
[Group G]
[Fintype G]
[Invertible ↑(Fintype.card G)]
(V : FdRep k G)
:

(⅟↑(Fintype.card G) • Finset.sum Finset.univ fun g => FdRep.character V g) = ↑(FiniteDimensional.finrank k { x // x ∈ Representation.invariants (FdRep.ρ V) })

theorem
FdRep.char_orthonormal
{k : Type u}
[Field k]
{G : GroupCat}
[IsAlgClosed k]
[Fintype ↑G]
[Invertible ↑(Fintype.card ↑G)]
(V : FdRep k ↑G)
(W : FdRep k ↑G)
[CategoryTheory.Simple V]
[CategoryTheory.Simple W]
:

(⅟↑(Fintype.card ↑G) • Finset.sum Finset.univ fun g => FdRep.character V g * FdRep.character W 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.