mathlib documentation

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 #

noncomputable def fdRep.character {k G : Type u} [field k] [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
theorem fdRep.char_mul_comm {k G : Type u} [field k] [monoid G] (V : fdRep k 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 : fdRep k G) :
@[simp]
theorem fdRep.char_tensor {k G : Type u} [field k] [monoid G] (V W : fdRep k G) :

The character is multiplicative under the tensor product.

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