Documentation

Mathlib.RepresentationTheory.Character

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 Simple class defined in Mathlib.CategoryTheory.Simple

TODO #

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
Instances For
    theorem FDRep.char_mul_comm {k : Type u} [Field k] {G : Type u} [Monoid G] (V : FDRep k G) (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 = (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) :
    (CategoryTheory.MonoidalCategory.tensorObj V W).character = V.character * W.character

    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.obj (CategoryTheory.MonoidalCategory.tensorObj (Action.FunctorCategoryEquivalence.functor.obj V) (Action.FunctorCategoryEquivalence.functor.obj W))) = V.character * W.character
    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) :
    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 : 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) :
    (FDRep.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 : FDRep k G) (W : FDRep k G) (g : G) :
    (FDRep.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 = (FiniteDimensional.finrank k (Representation.invariants V))
    theorem FDRep.char_orthonormal {k : Type u} [Field k] {G : Grp} [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) 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.