# mathlib3documentation

representation_theory.character

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

# TODO #

• Once we have the monoidal closed structure on fdRep k G and a better API for the rigid structure, char_dual and char_lin_hom should probably be stated in terms of Vᘁ and ihom V W.
noncomputable def fdRep.character {k : Type u} [field k] {G : Type u} [monoid G] (V : 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
theorem fdRep.char_mul_comm {k : Type u} [field k] {G : Type u} [monoid G] (V : 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 : G) :
@[simp]
theorem fdRep.char_tensor {k : Type u} [field k] {G : Type u} [monoid G] (V W : G) :
(V W).character =

The character is multiplicative under the tensor product.

theorem fdRep.char_iso {k : Type u} [field k] {G : Type u} [monoid G] {V W : G} (i : V W) :

The character of isomorphic representations is the same.

@[simp]
theorem fdRep.char_conj {k : Type u} [field k] {G : Type u} [group G] (V : 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 : G) (g : G) :
@[simp]
theorem fdRep.char_lin_hom {k : Type u} [field k] {G : Type u} [group G] (V W : G) (g : G) :
theorem fdRep.char_orthonormal {k : Type u} [field k] {G : Group} [fintype G] [invertible ] (V W : G)  :

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