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 #

Once we have the monoidal closed structure on fdRep k G and a better API for the rigid structure, char_dual and char_lin_hom should probably be stated in terms of Vᘁ and ihom V W.

source

noncomputable def fdRep.character {k : Type u} [field k] {G : Type u} [monoid G] (V : fdRep k G) (g : 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.

Equations

V.character g = ⇑(linear_map.trace k ↥V) (⇑(V.ρ) g)

source

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)

source

@[simp]

theorem fdRep.char_one {k : Type u} [field k] {G : Type u} [monoid G] (V : fdRep k G) :

V.character 1 = ↑(finite_dimensional.finrank k ↥V)

source

@[simp]

theorem fdRep.char_tensor {k : Type u} [field k] {G : Type u} [monoid G] (V W : fdRep k G) :

(V ⊗ W).character = V.character * W.character

The character is multiplicative under the tensor product.

source

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.

source

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

source

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

source

@[simp]

theorem fdRep.char_lin_hom {k : Type u} [field k] {G : Type u} [group G] (V W : fdRep k G) (g : G) :

(fdRep.of (representation.lin_hom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character 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.univ.sum (λ (g : G), V.character g) = ↑(finite_dimensional.finrank k ↥(representation.invariants V.ρ))

source

theorem fdRep.char_orthonormal {k : Type u} [field k] {G : Group} [is_alg_closed k] [fintype ↥G] [invertible ↑(fintype.card ↥G)] (V W : fdRep k ↥G) [category_theory.simple V] [category_theory.simple W] :

⅟ ↑(fintype.card ↥G) • finset.univ.sum (λ (g : ↥G), V.character g * W.character g⁻¹) = ite (nonempty (V ≅ W)) ↑1 ↑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.