Characters of representations

This file introduces characters of representation and proves basic lemmas about how characters behave under various operations on representations.

A key result is the orthogonality of characters for irreducible representations of finite group over an algebraically closed field whose characteristic doesn't divide the order of the group. It is the theorem char_orthonormal

Implementation notes

Irreducible representations are implemented categorically, using the CategoryTheory.Simple class defined in Mathlib/CategoryTheory/Simple.lean

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

• V.character g = (LinearMap.trace k ↑V.V) (V.ρ g)

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) : V.character 1 = ↑(Module.finrank k ↑V.V)

@[simp]

theorem FDRep.char_tensor {k : Type u} [Field k] {G : Type u} [Monoid G] (V W : FDRep k G) : (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).character = V.character * W.character

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) : V.character = W.character

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) : (of (Representation.dual V.ρ)).character g = V.character g⁻¹

@[simp]

theorem FDRep.char_linHom {k : Type u} [Field k] {G : Type u} [Group G] (V W : FDRep k G) (g : G) : (of (Representation.linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character 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) • ∑ g : G, V.character g = ↑(Module.finrank k ↥(Representation.invariants V.ρ))

theorem FDRep.scalar_product_char_eq_finrank_equivariant {k : Type u} [Field k] {G : Type u} [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (V W : FDRep k G) : ⅟↑(Fintype.card G) • ∑ g : G, W.character g * V.character g⁻¹ = ↑(Module.finrank k (V ⟶ W))

If V are W are finite-dimensional representations of a finite group, then the scalar product of their characters is equal to the dimension of the space of equivariant maps from V to W.

theorem FDRep.char_orthonormal {k : Type u} [Field k] {G : Type u} [Group G] [IsAlgClosed k] [Fintype G] [Invertible ↑(Fintype.card G)] (V W : FDRep k G) [CategoryTheory.Simple V] [CategoryTheory.Simple W] : ⅟↑(Fintype.card G) • ∑ g : G, V.character g * W.character 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.