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.

noncomputable 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.

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.

noncomputable def Representation.character {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) : k

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

theorem Representation.char_mul_comm {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g h : G) : ρ.character (h * g) = ρ.character (g * h)

@[simp]

theorem Representation.char_one {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) : ρ.character 1 = ↑(Module.finrank k V)

@[simp]

theorem Representation.char_tensor {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.tprod σ).character = ρ.character * σ.character

The character is multiplicative under the tensor product.

theorem Representation.char_iso {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (φ : ρ.Equiv σ) : ρ.character = σ.character

The character of isomorphic representations is the same.

@[simp]

theorem Representation.char_conj {G : Type u_1} {k : Type u_2} {V : Type u_3} [Group G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g h : G) : ρ.character (h * g * h⁻¹) = ρ.character g

The character of a representation is constant on conjugacy classes.

@[simp]

theorem Representation.char_dual {G : Type u_1} {k : Type u_2} {V : Type u_3} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (g : G) : ρ.dual.character g = ρ.character g⁻¹

@[simp]

theorem Representation.char_linHom {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) (g : G) : (ρ.linHom σ).character g = ρ.character g⁻¹ * σ.character g

theorem Representation.card_inv_mul_sum_char_eq_finrank {G : Type u_1} {k : Type u_2} {V : Type u_3} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [Fintype G] [Invertible ↑(Nat.card G)] : (↑(Nat.card G))⁻¹ * ∑ g : G, ρ.character g = ↑(Module.finrank k ↥ρ.invariants)

theorem Representation.card_inv_mul_sum_char_mul_char_eq_finrank {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [Fintype G] [Invertible ↑(Nat.card G)] : (↑(Nat.card G))⁻¹ * ∑ g : G, σ.character g * ρ.character g⁻¹ = ↑(Module.finrank k (ρ.IntertwiningMap σ))

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 Representation.char_orthonormal {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Group G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [Fintype G] [Invertible ↑(Nat.card G)] [IsAlgClosed k] [ρ.IsIrreducible] [σ.IsIrreducible] : (↑(Nat.card G))⁻¹ * ∑ g : G, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) 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.