Burnside's vanishing theorem for character values

Let χ be the character of an irreducible representation of a finite group G, and let g be an element whose conjugacy class C has size coprime to the degree χ(1). Then χ(g) is as far from generic as it can be: either it vanishes, or it has the largest absolute value a character value can have, namely χ(1).

The proof has two halves.

The arithmetic of the average. Bézout writes 1 = a·|C| + b·χ(1) with integers a and b, so

χ(g) / χ(1) = a · (|C| χ(g) / χ(1)) + b · χ(g) = a · ωᵪ(K_C) + b · χ(g),

with ωᵪ the central character and K_C the class sum. Both ωᵪ(K_C) and χ(g) are algebraic integers (TauCeti.Representation.isIntegral_centralCharacter_classSumCenter and Representation.isIntegral_char), so the average χ(g) / χ(1) is one too. That is Representation.isIntegral_char_div_finrank, proved over any algebraically closed field. This first half is where the coprimality is spent.

Kronecker's theorem. Over ℂ the value χ(g) is a sum of χ(1) roots of unity, so once the average is known to be an algebraic integer the dichotomy follows, with no arithmetic hypothesis of its own: this is TauCeti.sum_eq_zero_or_norm_sum_eq_card_of_isIntegral.

The classical use of the dichotomy is Burnside's pᵃqᵇ theorem, which applies it to an element whose class has prime-power size. Turning the second alternative ‖χ(g)‖ = χ(1) into the statement that ρ g is a scalar is the equality case of the triangle inequality for a sum of roots of unity, Representation.exists_apply_eq_smul_of_norm_char_eq_finrank; combined with the dichotomy it gives Representation.char_eq_zero_or_exists_apply_eq_smul, the form of Isaacs' Theorem 3.8.

Main statements

• Representation.isIntegral_char_div_finrank and its bundled form FDRep.isIntegral_char_div_finrank: when the class size and the degree are coprime, the average χ(g) / χ(1) is an algebraic integer.
• Representation.char_eq_zero_or_norm_char_eq_finrank and its bundled form FDRep.char_eq_zero_or_norm_char_eq_finrank: Burnside's vanishing theorem, the dichotomy χ(g) = 0 ∨ ‖χ(g)‖ = χ(1).
• Representation.char_eq_zero_or_exists_apply_eq_smul and its bundled form FDRep.char_eq_zero_or_exists_apply_eq_smul: the same dichotomy with the second alternative read as ρ g being a scalar.

References

• I. M. Isaacs, Character Theory of Finite Groups (1976), Theorem 3.8.

theorem Representation.isIntegral_char_div_finrank {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [Group G] [Finite G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank k V)) : IsIntegral ℤ (ρ.character g / ↑(Module.finrank k V))

The average of an irreducible character over its degree is an algebraic integer, whenever the size of the conjugacy class of g is coprime to the degree.

Bézout splits χ(g) / χ(1) as an integer combination of the central-character value ωᵪ(K_C) = |C| χ(g) / χ(1) and of χ(g), both of which are algebraic integers. No hypothesis on the characteristic is needed: if the degree happens to vanish in k the quotient is 0, which is an algebraic integer for the trivial reason.

theorem Representation.char_eq_zero_or_norm_char_eq_finrank {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) [ρ.IsIrreducible] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ V)) : ρ.character g = 0 ∨ ‖ρ.character g‖ = ↑(Module.finrank ℂ V)

Burnside's vanishing theorem. If the conjugacy class of g has size coprime to the degree of an irreducible complex representation ρ, then its character either vanishes at g or attains there the maximum absolute value χ(1) that any character value can have.

The average χ(g) / χ(1) is an algebraic integer (Representation.isIntegral_char_div_finrank) and χ(g) is a sum of χ(1) roots of unity, so Kronecker's theorem leaves no other possibility.

theorem Representation.char_eq_zero_or_exists_apply_eq_smul {G : Type u_1} {V : Type u_2} [Group G] [Finite G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) [ρ.IsIrreducible] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ V)) : ρ.character g = 0 ∨ ∃ (μ : ℂ), ρ g = μ • 1

Burnside's vanishing theorem, scalar form (Isaacs, Theorem 3.8). If the conjugacy class of g has size coprime to the degree of an irreducible complex representation ρ, then either its character vanishes at g, or ρ g is a scalar μ • 1, that is, g lies in the centre Z(χ) of the character (Isaacs, Lemma 2.27).

theorem FDRep.isIntegral_char_div_finrank {G : Type u_1} [Group G] [Finite G] {k : Type u_2} [Field k] [IsAlgClosed k] (X : FDRep k G) [Representation.IsIrreducible X.ρ] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank k ↑X.V)) : IsIntegral ℤ (X.character g / ↑(Module.finrank k ↑X.V))

The average of an irreducible character over its degree is an algebraic integer, for a bundled finite-dimensional representation over an algebraically closed field.

theorem FDRep.char_eq_zero_or_norm_char_eq_finrank {G : Type u_1} [Group G] [Finite G] (X : FDRep ℂ G) [Representation.IsIrreducible X.ρ] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ ↑X.V)) : X.character g = 0 ∨ ‖X.character g‖ = ↑(Module.finrank ℂ ↑X.V)

Burnside's vanishing theorem, for a bundled finite-dimensional complex representation.

theorem FDRep.char_eq_zero_or_exists_apply_eq_smul {G : Type u_1} [Group G] [Finite G] (X : FDRep ℂ G) [Representation.IsIrreducible X.ρ] {g : G} (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ ↑X.V)) : X.character g = 0 ∨ ∃ (μ : ℂ), X.ρ g = μ • 1

Burnside's vanishing theorem, scalar form, for a bundled finite-dimensional complex representation.