The arithmetic of character values

If g is an element of finite order n in a group and ρ is a finite-dimensional representation, then ρ g satisfies X ^ n - 1, so every root of its characteristic polynomial is an n-th root of unity. As soon as that characteristic polynomial splits, over an algebraically closed field for instance, the character value ρ.character g is the sum of finrank of these roots of unity.

This file proves that description and reads off its arithmetic consequences: the character value is integral over ℤ, and over ℂ it lies in the ring ℤ[ζ] generated by a primitive n-th root of unity, is bounded in absolute value by the degree χ(1), and is conjugated by inverting the group element, since conjugation inverts roots of unity. The endomorphism ρ g is moreover semisimple as soon as n is invertible in the coefficient field, since X ^ n - 1 is then squarefree.

Integrality needs no splitting hypothesis, because base change to an algebraic closure transports the character value along the field embedding; that reduction is Module.End.isIntegral_trace_of_pow_eq_one. Over ℚ it gives more than integrality over ℤ: a rational algebraic integer is an integer, so a rational character is integer-valued. That is what makes the character table of a group with rational representations, the symmetric group for instance, a matrix of integers.

The facts about ρ g as a bare endomorphism live in TauCeti.LinearAlgebra.End.FiniteOrder.

The conjugation identity conj (χ g) = χ g⁻¹ also holds for a unitary representation of a topological group, where it is ContRepresentation.character_apply_inv and comes from the action of g⁻¹ being the adjoint of the action of g. Here it is proved for an arbitrary complex representation of a group, from the eigenvalues alone, with no invariant inner product in sight.

Main results

• Representation.exists_multiset_rootsOfUnity_char_eq_sum_of_splits: whenever (ρ g).charpoly splits, a character value is a sum of finrank many n-th roots of unity. The variant Representation.exists_multiset_rootsOfUnity_char_eq_sum specializes it to an algebraically closed field.
• Representation.isIntegral_char: character values are algebraic integers, over an arbitrary field. The bundled FDRep form is Mathlib's FDRep.isIntegral_character.
• Representation.char_mem_of_forall_pow_eq_one_mem: whenever (ρ g).charpoly splits, a character value at g with g ^ n = 1 lies in every subring containing the n-th roots of unity.
• Representation.exists_char_eq_intCast and FDRep.exists_char_eq_intCast: a rational character is integer-valued.
• FDRep.intCharacter: the resulting ℤ-valued character of a rational representation of a finite group, taking the degree at the identity, and FDRep.intClassFunction: the same character read as an element of TauCeti.ClassFunction ℤ G.
• FDRep.char_mem_adjoin_of_isPrimitiveRoot: over ℂ they lie in ℤ[ζ_e], for ζ_e a primitive root of unity of order the exponent of the group.
• FDRep.norm_char_le_finrank: over ℂ, ‖χ(g)‖ ≤ χ(1).
• Representation.exists_apply_eq_smul_of_norm_char_eq_finrank and its bundled form FDRep.exists_apply_eq_smul_of_norm_char_eq_finrank: the equality case of that bound, ‖χ(g)‖ = χ(1), which forces ρ g to be a root of unity times the identity.
• FDRep.conj_char: over ℂ, inversion conjugates character values, conj (χ g) = χ g⁻¹. This is what makes the character pairing agree with the Hermitian inner product on complex class functions.
• Representation.isSemisimple_apply and FDRep.isSemisimple_ρ: if the characteristic of k does not divide |G|, then ρ g is a semisimple endomorphism; over ℂ the hypothesis is found by instance search.

The eigenvalues are taken with algebraic multiplicity, as the root multiset of the characteristic polynomial. The set of roots of the minimal polynomial is the same, namely the distinct eigenvalues, but its root multiplicities record maximal Jordan block sizes rather than algebraic multiplicities, so they do not sum to the trace.

Cyclotomic membership and the norm bounds are stated over ℂ; integrality holds over any field.

References

• I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 3.
• J.-P. Serre, Linear Representations of Finite Groups (1977), Section 12.1.

theorem Representation.pow_eq_one_of_mem_roots_charpoly {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) {g : G} {n : ℕ} (hg : g ^ n = 1) {μ : k} (hμ : μ ∈ (ρ g).charpoly.roots) : μ ^ n = 1

If g ^ n = 1 then every eigenvalue of ρ g is an n-th root of unity.

theorem Representation.exists_multiset_rootsOfUnity_char_eq_sum_of_splits {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) {g : G} {n : ℕ} (hsplits : (ρ g).charpoly.Splits) (hg : g ^ n = 1) : ∃ (s : Multiset k), s.card = Module.finrank k V ∧ (∀ μ ∈ s, μ ^ n = 1) ∧ ρ.character g = s.sum

A character value is a sum of roots of unity. If g ^ n = 1 and the characteristic polynomial of ρ g splits, then ρ.character g is the sum of a multiset of finrank k V many n-th roots of unity, namely the eigenvalues of ρ g with algebraic multiplicity.

theorem Representation.exists_multiset_rootsOfUnity_char_eq_sum {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [IsAlgClosed k] (ρ : Representation k G V) {g : G} {n : ℕ} (hg : g ^ n = 1) : ∃ (s : Multiset k), s.card = Module.finrank k V ∧ (∀ μ ∈ s, μ ^ n = 1) ∧ ρ.character g = s.sum

A character value is a sum of roots of unity. Over an algebraically closed field, if g ^ n = 1 then ρ.character g is the sum of a multiset of finrank k V many n-th roots of unity, namely the eigenvalues of ρ g with algebraic multiplicity.

theorem Representation.isSemisimple_of_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {g : G} {n : ℕ} (hn : ↑n ≠ 0) (hg : g ^ n = 1) : Module.End.IsSemisimple (ρ g)

If g ^ n = 1 with n invertible in k, then ρ g is a semisimple endomorphism. This needs no hypothesis on the field beyond invertibility of n. Over a field splitting X ^ n - 1, an algebraically closed one for instance, semisimplicity of ρ g is its diagonalizability, the form in which it underlies the eigenvalue description of character values.

theorem Representation.isIntegral_char {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) : IsIntegral ℤ (ρ.character g)

Character values are algebraic integers: over any field, the value of a character at an element of finite order is integral over ℤ. Once the characteristic polynomial of ρ g splits this is the statement that a sum of roots of unity is an algebraic integer, and the general case follows from that one by base change to an algebraic closure (Module.End.isIntegral_trace_of_pow_eq_one).

theorem Representation.char_mem_of_forall_pow_eq_one_mem {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) {g : G} {n : ℕ} (hsplits : (ρ g).charpoly.Splits) (hg : g ^ n = 1) {A : Subring k} (hA : ∀ (x : k), x ^ n = 1 → x ∈ A) : ρ.character g ∈ A

Character values lie in every subring containing the relevant roots of unity. If the characteristic polynomial of ρ g splits, g ^ n = 1, and the subring A of k contains every n-th root of unity, then ρ.character g ∈ A, being a sum of n-th roots of unity.

theorem Representation.exists_char_eq_intCast {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] (ρ : Representation ℚ G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) : ∃ (m : ℤ), ρ.character g = ↑m

A rational character value is an integer. The character of a representation over ℚ takes at an element of finite order a value that is integral over ℤ, and ℤ is integrally closed in its fraction field ℚ, so that value is the cast of an integer.

theorem Representation.isSemisimple_apply {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (hG : ↑(Nat.card G) ≠ 0) (g : G) : Module.End.IsSemisimple (ρ g)

If the order of G is invertible in k, then every group element acts semisimply. The order of g divides |G|, so it too is invertible, and ρ g is annihilated by the squarefree polynomial X ^ orderOf g - 1. Over a field splitting that polynomial, an algebraically closed one for instance, this is diagonalizability of ρ g.

theorem Representation.char_mem_adjoin_of_isPrimitiveRoot {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} {ζ : ℂ} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) (hg : g ^ n = 1) : ρ.character g ∈ ℤ[ζ]

Character values are cyclotomic integers: over ℂ, if ζ is a primitive n-th root of unity and g ^ n = 1, then ρ.character g lies in the subring ℤ[ζ] of ℂ.

theorem Representation.norm_char_le_finrank {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) : ‖ρ.character g‖ ≤ ↑(Module.finrank ℂ V)

Over ℂ a character value at an element of finite order is bounded in absolute value by the degree of the representation, since it is a sum of finrank ℂ V many roots of unity.

theorem Representation.exists_apply_eq_smul_of_norm_char_eq_finrank {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) (h : ‖ρ.character g‖ = ↑(Module.finrank ℂ V)) : ∃ (μ : ℂ), μ ^ n = 1 ∧ ρ g = μ • 1

The equality case of the bound on a character value. If the absolute value of ρ.character g attains the degree finrank ℂ V, then ρ g is a scalar, the scalar being an n-th root of unity: the character value is a sum of finrank ℂ V many roots of unity, so it can have that absolute value only if they all coincide, and then ρ g is diagonalizable with a single eigenvalue. The bound itself is Representation.norm_char_le_finrank.

theorem Representation.conj_char_eq_char_inv {G : Type v} {V : Type w} [DivisionMonoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) : (starRingEnd ℂ) (ρ.character g) = ρ.character g⁻¹

Over ℂ, inversion conjugates character values: if g ^ n = 1 with n ≠ 0, then conj (χ g) = χ g⁻¹. The eigenvalues of ρ g are n-th roots of unity, so conjugating them inverts them, and ρ g⁻¹ is the inverse of ρ g.

@[simp]

theorem Representation.conj_char {G : Type v} {V : Type w} [Group G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] [Finite G] (ρ : Representation ℂ G V) (g : G) : (starRingEnd ℂ) (ρ.character g) = ρ.character g⁻¹

Over ℂ, inversion conjugates the character values of a finite group.

theorem FDRep.exists_char_eq_intCast {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) (g : G) : ∃ (m : ℤ), V.character g = ↑m

A rational character is integer-valued. For a finite group, every value of the character of a finite-dimensional representation over ℚ is the cast of an integer.

noncomputable def FDRep.intCharacter {G : Type v} [Group G] (V : FDRep ℚ G) (g : G) : ℤ

The integer character of a rational representation of a finite group: the character value V.character g is the cast of an integer (FDRep.exists_char_eq_intCast), and this is that integer, extracted as the numerator of the rational value. Read it only through FDRep.intCharacter_cast, which is what pins it down; the numerator is a way of naming the integer, not extra information.

It lives in the root FDRep namespace, so dot notation on an FDRep ℚ G reaches it: write V.intCharacter g.

Equations

• V.intCharacter g = (V.character g).num

@[simp]

theorem FDRep.intCharacter_cast {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) (g : G) : ↑(V.intCharacter g) = V.character g

The integer character casts back to the character.

theorem FDRep.intCharacter_eq_iff {G : Type v} [Group G] [Finite G] {V W : FDRep ℚ G} {g h : G} : V.intCharacter g = W.intCharacter h ↔ V.character g = W.character h

The integer character carries exactly the information of the rational one: this is the elimination principle for FDRep.intCharacter, an integer equation between its values being the corresponding equation between character values.

@[simp]

theorem FDRep.intCharacter_conj {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) (g h : G) : V.intCharacter (h * g * h⁻¹) = V.intCharacter g

The integer character is a class function.

noncomputable def FDRep.intClassFunction {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) : ↥(TauCeti.ClassFunction ℤ G)

The integer character of a rational representation, as a class function.

Equations

• V.intClassFunction = ⟨V.intCharacter, ⋯⟩

@[simp]

theorem FDRep.intClassFunction_apply {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) (g : G) : ↑V.intClassFunction g = V.intCharacter g

theorem FDRep.intCharacter_eq_of_isConj {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) {g h : G} (hgh : IsConj g h) : V.intCharacter g = V.intCharacter h

Conjugate elements have the same integer character.

@[simp]

theorem FDRep.intCharacter_one {G : Type v} [Group G] [Finite G] (V : FDRep ℚ G) : V.intCharacter 1 = ↑(Module.finrank ℚ ↑V.V)

The integer character at the identity is the degree.

theorem FDRep.char_mem_adjoin_of_isPrimitiveRoot {G : Type v} [Group G] [Finite G] (V : FDRep ℂ G) {ζ : ℂ} (hζ : IsPrimitiveRoot ζ (Monoid.exponent G)) (g : G) : V.character g ∈ ℤ[ζ]

Character values are cyclotomic integers. For a finite group of exponent e and a primitive e-th root of unity ζ, every value of a complex character lies in ℤ[ζ].

theorem FDRep.norm_char_le_finrank {G : Type v} [Group G] [Finite G] (V : FDRep ℂ G) (g : G) : ‖V.character g‖ ≤ ↑(Module.finrank ℂ ↑V.V)

Over ℂ, a character of a finite group is bounded in absolute value by its degree, ‖χ(g)‖ ≤ χ(1).

theorem FDRep.exists_apply_eq_smul_of_norm_char_eq_finrank {G : Type v} [Group G] [Finite G] (V : FDRep ℂ G) {g : G} (h : ‖V.character g‖ = ↑(Module.finrank ℂ ↑V.V)) : ∃ (μ : ℂ), μ ^ orderOf g = 1 ∧ V.ρ g = μ • 1

The equality case of the bound on a character value, for a finite group: if ‖χ(g)‖ attains the degree, then V.ρ g is a scalar, the scalar being a root of unity of order dividing that of g. The bound itself is FDRep.norm_char_le_finrank.

@[simp]

theorem FDRep.conj_char {G : Type v} [Group G] [Finite G] (V : FDRep ℂ G) (g : G) : (starRingEnd ℂ) (V.character g) = V.character g⁻¹

Over ℂ, inversion conjugates the character values of a finite group, so that a complex character is a "unitary" class function: conj (χ g) = χ g⁻¹.

theorem FDRep.isSemisimple_ρ {G : Type v} [Group G] {k : Type u} [Field k] [NeZero ↑(Nat.card G)] (V : FDRep k G) (g : G) : Module.End.IsSemisimple (V.ρ g)

Diagonalizability. If the order of G is invertible in k, which forces G to be finite and which every finite group satisfies in characteristic zero, then V.ρ g is a semisimple endomorphism. Over an algebraically closed field, ℂ for instance, this is its diagonalizability.