# mathlibdocumentation

representation_theory.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_lin_hom should probably be stated in terms of Vᘁ and ihom V W.
noncomputable def fdRep.character {k G : Type u} [field k] [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 G : Type u} [field k] [monoid G] (V : G) (g h : G) :
V.character (h * g) = V.character (g * h)
@[simp]
theorem fdRep.char_one {k G : Type u} [field k] [monoid G] (V : G) :
@[simp]
theorem fdRep.char_tensor {k G : Type u} [field k] [monoid G] (V W : G) :
(V W).character =

The character is multiplicative under the tensor product.

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

The character of isomorphic representations is the same.

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