mathlib3 documentation

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 #

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

The character is multiplicative under the tensor product.

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