Characters of induced representations

This file proves the coset-representative formula for the character of a representation induced from a finite-index subgroup. The formula is valid over any field and has no division by the subgroup order.

Main result

• TauCeti.character_indFDRep identifies the character of TauCeti.indFDRep with the character of Mathlib's Representation.ind, the two differing only by the small carrier model.
• TauCeti.character_indFDRep_sum_quotient expresses an induced character as a sum over left cosets.
• TauCeti.character_indFDRep_eq_zero_of_notMem: an induced character vanishes outside a normal subgroup of finite index.
• Subgroup.indClassFun_ofFDRep_character and Subgroup.indClassFunction_ofFDRep identify that coset sum with Subgroup.indClassFun, the induced class function.
• TauCeti.character_ind rewrites the coset sum as an average over the whole group when the subgroup order is invertible in the coefficient field; it is the specialization of Subgroup.indClassFun_eq_natCard_inv_mul_sum to a character.

References

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.

theorem TauCeti.character_indFDRep {k : Type u} {G : Type v} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (g : G) : (indFDRep A).character g = (Representation.ind S.subtype A.ρ).character g

The character of TauCeti.indFDRep is Mathlib's induced character. Passing to the finite-dimensional model only replaces the carrier of Representation.ind by a small one, which TauCeti.indFDRepForgetEquiv compares with it.

theorem TauCeti.character_indFDRep_sum_quotient {k : Type u} {G : Type v} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (g : G) : (indFDRep A).character g = ∑ t : G ⧸ S, if h : (Quotient.out t)⁻¹ * g * Quotient.out t ∈ S then A.character ⟨(Quotient.out t)⁻¹ * g * Quotient.out t, h⟩ else 0

The induced character at g is the sum of the original character over those left coset representatives t for which t⁻¹ g t belongs to the subgroup.

@[simp]

theorem TauCeti.character_indFDRep_eq_zero_of_notMem {k : Type u} {G : Type v} [Field k] [Group G] {S : Subgroup G} [S.Normal] [S.FiniteIndex] (A : FDRep k ↥S) {g : G} (hg : g ∉ S) : (indFDRep A).character g = 0

An induced character vanishes outside a normal subgroup. For a normal subgroup S of finite index, the character of a representation induced from S is supported on S, so computing it only takes describing its values on S.

@[simp]

theorem Subgroup.indClassFun_ofFDRep_character {k : Type u} {G : Type v} [Field k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : FDRep k ↥S) : S.indClassFun A.character = (TauCeti.indFDRep A).character

The character of an induced representation is the induced class function of its character.

@[simp]

theorem Subgroup.indClassFunction_ofFDRep {k : Type u} {G : Type v} [Field k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : FDRep k ↥S) : S.indClassFunction (TauCeti.ClassFunction.ofFDRep A) = TauCeti.ClassFunction.ofFDRep (TauCeti.indFDRep A)

Inducing the class function of a finite-dimensional representation gives the class function of the induced representation.

theorem TauCeti.character_ind {k : Type u} {G : Type v} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hS : IsUnit ↑(Nat.card ↥S)) (A : FDRep k ↥S) (g : G) : (indFDRep A).character g = (↑(Nat.card ↥S))⁻¹ * ∑ x : G, if h : x⁻¹ * g * x ∈ S then A.character ⟨x⁻¹ * g * x, h⟩ else 0

The induced character at g, written as an average over the whole group. The subgroup order must be invertible in the coefficient field; without this hypothesis, character_indFDRep_sum_quotient is the division-free formula to use.

This is the specialization of Subgroup.indClassFun_eq_natCard_inv_mul_sum to a character.