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.

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

• FdRep.character V g = (LinearMap.trace k (CoeSort.coe V)) ((FdRep.ρ V) g)

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)

@[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))

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.

@[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.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj (Action.FunctorCategoryEquivalence.functor.toPrefunctor.obj V) (Action.FunctorCategoryEquivalence.functor.toPrefunctor.obj W))) = FdRep.character V * FdRep.character W

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.

@[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.

@[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⁻¹

@[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

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 : G) => FdRep.character V g) = ↑(FiniteDimensional.finrank k ↥(Representation.invariants (FdRep.ρ V)))

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 : ↑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.