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

source

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

(fun x => k) (↑(FdRep.ρ V) g)

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

Instances For

source

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

FdRep.character V (h * g) = FdRep.character V (g * h)

source

@[simp]

theorem FdRep.char_one {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FdRep k G) :

FdRep.character V 1 = ↑(FiniteDimensional.finrank k (CoeSort.coe V))

source

theorem FdRep.char_tensor {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FdRep k G) (W : FdRep k G) :

FdRep.character (CategoryTheory.MonoidalCategory.tensorObj V W) = FdRep.character V * FdRep.character W

The character is multiplicative under the tensor product.

source

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

source

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) :

FdRep.character V = FdRep.character W

The character of isomorphic representations is the same.

source

@[simp]

theorem FdRep.char_conj {k : Type u} [Field k] {G : Type u} [Group G] (V : FdRep k G) (g : G) (h : G) :

FdRep.character V (h * g * h⁻¹) = FdRep.character V g

The character of a representation is constant on conjugacy classes.

source

@[simp]

theorem FdRep.char_dual {k : Type u} [Field k] {G : Type u} [Group G] (V : FdRep k G) (g : G) :

FdRep.character (FdRep.of (Representation.dual (FdRep.ρ V))) g = FdRep.character V g⁻¹

source

@[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.character (FdRep.of (Representation.linHom (FdRep.ρ V) (FdRep.ρ W))) g = FdRep.character V g⁻¹ * FdRep.character W g

source

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.sum Finset.univ fun g => FdRep.character V g) = ↑(FiniteDimensional.finrank k { x // x ∈ Representation.invariants (FdRep.ρ V) })

source

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.sum Finset.univ fun g => FdRep.character V g * FdRep.character W 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.