Documentation

TauCeti.RepresentationTheory.CharacterTable.Degree

The degree of an irreducible character divides the group order #

For an irreducible representation ρ of a finite group G over an algebraically closed field of characteristic zero, the degree χ(1) = dim V divides |G|.

The proof is the classical one. First orthogonality gives ∑_g χ(g) χ(g⁻¹) = |G|. Collecting that sum one conjugacy class at a time and substituting the class-sum identity ωᵪ(K_C) · χ(1) = |C| · χ(g_C) for the central character turns it into

χ(1) · ∑_C ωᵪ(K_C) χ(g_C⁻¹) = |G|.

Every factor of the remaining sum is an algebraic integer -- the values of a central character on the class sums because the class sums are integral over ℤ, the character values because they are sums of roots of unity -- so |G| / χ(1) is an algebraic integer. It is also rational, and a rational algebraic integer is an integer, so χ(1) divides |G|.

Main statements #

Implementation notes #

The character value at the inverse, g ↦ χ(g⁻¹), is the character of the dual representation (Representation.char_dual), so the sum over conjugacy classes is indexed through TauCeti.ClassFunction.toConjClasses of that character rather than through a choice of class representatives. The corresponding representative form is TauCeti.Representation.centralCharacter_classSumCenter_mul_character_one.

References #

This proves the "degree divides the order" item of Layer 4 of the character theory roadmap. See I. M. Isaacs, Character Theory of Finite Groups, Theorem 3.11, or J.-P. Serre, Linear Representations of Finite Groups, Section 6.5.

source
theorem TauCeti.Representation.finrank_mul_sum_centralCharacter_eq_card {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] [Fintype G] [DecidableEq G] [IsAlgClosed k] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] [Invertible ↑(Nat.card G)] :
↑(Module.finrank k V) * ∑ C : ConjClasses G, (centralCharacter ρ) (classSumCenter C) * ClassFunction.toConjClasses (ClassFunction.ofCharacter ρ.dual) C = ↑(Nat.card G)

The degree times an algebraic integer is the group order.

Collecting first orthogonality one conjugacy class at a time and substituting ωᵪ(K_C) · χ(1) = |C| · χ(g_C) gives χ(1) · ∑_C ωᵪ(K_C) χ(g_C⁻¹) = |G|, where g_C is any element of the class C and the value χ(g_C⁻¹) is read off the character of the dual representation. Both factors of each summand are algebraic integers, which is what makes this the divisibility statement TauCeti.Representation.finrank_dvd_card.

source
theorem TauCeti.Representation.finrank_dvd_card {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] [Finite G] [IsAlgClosed k] [CharZero k] [FiniteDimensional k V] (ρ : Representation k G V) [ρ.IsIrreducible] :
Module.finrank k V ∣ Nat.card G

The degree of an irreducible character divides the order of the group.

Over an algebraically closed field of characteristic zero, the dimension of an irreducible representation of a finite group G divides |G|.

source
theorem FDRep.finrank_dvd_card {k : Type u_1} {G : Type u_2} [Field k] [IsAlgClosed k] [CharZero k] [Group G] [Finite G] (X : FDRep k G) [Representation.IsIrreducible X.ρ] :
Module.finrank k ↑X.V ∣ Nat.card G

The degree of an irreducible character divides the order of the group, for a bundled finite-dimensional representation.