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 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 and char_linHom should probably be stated in terms of Vᘁ and ihom V W.

def FdRep.character {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FdRep k G) (g : G) : k

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

Equations

• V.character g = (LinearMap.trace k (CoeSort.coe V)) (V.ρ g)

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

@[simp]

theorem FdRep.char_one {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FdRep k G) : V.character 1 = ↑(FiniteDimensional.finrank k (CoeSort.coe V))

theorem FdRep.char_tensor {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FdRep k G) (W : FdRep k G) : (CategoryTheory.MonoidalCategory.tensorObj V W).character = V.character * W.character

The character is multiplicative under the tensor product.

@[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))) = V.character * W.character

theorem FdRep.char_iso {k : Type u} [Field k] {G : Type u} [Monoid G] {V : FdRep k G} {W : FdRep k G} (i : V ≅ W) : V.character = W.character

The character of isomorphic representations is the same.

@[simp]

theorem FdRep.char_conj {k : Type u} [Field k] {G : Type u} [Group G] (V : FdRep k G) (g : G) (h : G) : V.character (h * g * h⁻¹) = V.character 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.of (Representation.dual V.ρ)).character g = V.character 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.of (Representation.linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character 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.univ.sum fun (g : G) => V.character g) = ↑(FiniteDimensional.finrank k ↥(Representation.invariants 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.univ.sum fun (g : ↑G) => V.character g * W.character 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.