The character table of a finite group #
Let G be a finite group and k an algebraically closed field in which |G| is invertible. The
characters of the irreducible representations of G over k form a finite set
TauCeti.irreducibleCharacters k G of functions G → k, of size the number of conjugacy classes of
G: they are linearly independent, they span the class functions, and every irreducible
representation is equivalent to one that occurs in the complete family produced by the Wedderburn
decomposition of k[G].
Choosing an enumeration of that set by Fin r, r = |ConjClasses G|, turns the irreducible
characters into the rows of a square matrix, the character table
TauCeti.characterTable k G : Matrix (Fin r) (ConjClasses G) k, whose (i, C) entry is the value
of the i-th irreducible character on the class C. Its columns are labelled by the actual
conjugacy classes of G; only the rows depend on the enumeration, and any two enumerations differ
by a permutation of them.
The two orthogonality relations become statements about the table: its rows are orthonormal for the
character pairing, and its columns are orthogonal with the class sizes as weights. Over ℂ both
take their familiar Hermitian form, because inversion conjugates character values
(Representation.conj_char).
Main definitions #
TauCeti.irreducibleCharacters: the set of irreducible characters ofGoverk.TauCeti.irreducibleCharacter: thei-th irreducible character, for an enumeration of that set byFin (Nat.card (ConjClasses G)), together withTauCeti.irreducibleRepresentation, an irreducible representation affording it, andTauCeti.characterDegree, its degree.TauCeti.characterTable: the character table ofG.TauCeti.basisIrreducibleCharacter: its rows, as a basis of the class functions, so thatTauCeti.linearIndependent_irreducibleCharacterholds inG → k.
Main results #
TauCeti.card_irreducibleCharacters:Ghas as many irreducible characters as conjugacy classes, so the table is square;TauCeti.character_mem_irreducibleCharactersis the statement that no irreducible character is missing from it.TauCeti.characterTable_apply: the entries of the table are the irreducible character values.TauCeti.card_inv_mul_sum_characterTable_mul_characterTable_invandTauCeti.card_inv_mul_sum_characterTable_mul_conj: first (row) orthogonality, overkand in its Hermitian form overℂ;TauCeti.card_inv_mul_sum_card_conjClass_mul_characterTable_mul_conjis the latter summed one column at a time, the form in which the roadmap's specification of a character table asks for it;TauCeti.characterPairing_ofCharacter_irreducibleRepresentation_orthonormalis the same relation phrased as orthonormality for the character pairing.TauCeti.exists_irreducibleCharacter_eq_one: the trivial character is a row of the table, and in characteristic zero every other row is nonconstant (TauCeti.exists_irreducibleCharacter_ne_characterDegree).TauCeti.card_conjClass_mul_sum_characterTable_mul_characterTable_invandTauCeti.sum_characterTable_mul_conj: second (column) orthogonality, overkand in its Hermitian form overℂ.TauCeti.irreducibleCharacter_apply_mem_of_forall_pow_eq_one_mem: the entries lie in every subring containing the|G|-th roots of unity.TauCeti.characterTable_one: the identity-class column of the table lists the degrees, which are positive (TauCeti.characterDegree_pos) and have squares summing to|G|(TauCeti.sum_characterDegree_sq_eq_card); in characteristic zero they moreover divide|G|(TauCeti.characterDegree_dvd_card).
Implementation notes #
TauCeti.irreducibleCharacters is defined by the representations on the coordinate spaces
Fin n → k, the shape in which the Wedderburn blocks of k[G] produce them; this also keeps the
set free of a universe parameter beyond those of k and G. Nothing is lost:
TauCeti.character_mem_irreducibleCharacters puts the character of an irreducible representation on
any finite-dimensional space in the set, since it is equivalent to one of the coordinate ones.
The rows are indexed by Fin (Nat.card (ConjClasses G)) rather than by a bare Fin r, so that the
squareness of the table is visible in its type.
The roadmap pins the character table over ℂ. Everything holds over any algebraically closed field
in which |G| is invertible except the Hermitian refinements, which are stated over ℂ, and the
divisibility of the degrees by |G|, which additionally assumes CharZero k. So the table is
defined over such a k, and TauCeti.characterTable ℂ G is the pinned object.
References #
This is Layer 3 of the
character theory roadmap:
the character table as an object, with its second orthogonality relation
(char_column_orthogonality in that roadmap's Suggested.lean) and the degrees in its
identity-class column.
See I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 2, or J.-P. Serre, Linear
Representations of Finite Groups (1977), Section 2.5.
The irreducible characters of G over k: the set of characters of the irreducible
representations of G on the coordinate spaces Fin n → k.
Restricting to coordinate spaces costs nothing: by TauCeti.character_mem_irreducibleCharacters the
character of an irreducible representation on any finite-dimensional space belongs to this set.
Equations
- TauCeti.irreducibleCharacters k G = {f : G → k | ∃ (n : ℕ) (ρ : Representation k G (Fin n → k)), ρ.IsIrreducible ∧ ρ.character = f}
Instances For
Membership in TauCeti.irreducibleCharacters unfolded. This is deliberately not @[simp]:
unfolding membership to the existential would put the left-hand side of the @[simp] lemma
TauCeti.irreducibleCharacter_mem out of simp normal form, and simp cannot discharge the
existential it produces.
The character of an irreducible representation is an irreducible character: the character
of an irreducible representation on an arbitrary finite-dimensional space lies in
TauCeti.irreducibleCharacters, because a basis transports it to an equivalent representation on a
coordinate space.
The character of a simple object of FDRep k G is an irreducible character, the bundled
form of TauCeti.character_mem_irreducibleCharacters.
The irreducible characters of G correspond to its conjugacy classes. A complete family of
pairwise inequivalent irreducible representations is indexed by ConjClasses G, its characters are
distinct because they are linearly independent, and every irreducible character is one of them.
A finite group has as many irreducible characters as conjugacy classes.
An enumeration of the irreducible characters of G by Fin (Nat.card (ConjClasses G)), chosen
once and for all; it indexes the rows of the character table.
Equations
Instances For
The i-th irreducible character of G.
Equations
- TauCeti.irreducibleCharacter k i = ↑((TauCeti.finEquivIrreducibleCharacters k G) i)
Instances For
The i-th member of the chosen enumeration is the i-th irreducible character.
Every enumerated character is an irreducible character.
Distinct rows of the character table are distinct characters.
Every irreducible character is enumerated.
The trivial character is a row of the character table: some enumerated irreducible
character of G is the constant function 1, the character of the trivial one-dimensional
representation.
The degree of the i-th irreducible character, the dimension of a representation affording
it.
Equations
Instances For
An irreducible representation affording the i-th irreducible character.
Equations
Instances For
The representations affording the rows of the character table are pairwise inequivalent, their characters being distinct.
An irreducible character takes its degree as its value at the identity.
The values of the irreducible characters lie in every subring of k containing the
|G|-th roots of unity, each value being a sum of such roots.
The degree of an irreducible character is positive: an irreducible representation is nonzero, so the space affording the character has positive dimension.
The sum of the squares of the degrees is the order of the group, as an identity of natural
numbers. The representations affording the enumerated characters are pairwise inequivalent
irreducibles, and there are as many of them as G has conjugacy classes, so they are the blocks of
a Wedderburn presentation of k[G] up to a relabelling of the blocks; the squares of the block
dimensions add up to the dimension |G| of k[G].
The degree of an irreducible character divides the order of the group.
The character table of G: the square matrix whose (i, C) entry is the value of the
i-th irreducible character of G on the conjugacy class C.
The rows are indexed by the chosen enumeration TauCeti.finEquivIrreducibleCharacters of the
irreducible characters and the columns by the conjugacy classes themselves, so the table is labelled
on its columns and determined up to a permutation of its rows.
Equations
Instances For
The entries of the character table are the values of the irreducible characters: the entry
in row i and the column of the class of g is the i-th irreducible character at g.
The identity-class column of the character table lists the degrees of the irreducible characters.
This is not a simp lemma: TauCeti.characterTable_apply already rewrites the left-hand side to
TauCeti.irreducibleCharacter k i 1, which TauCeti.irreducibleCharacter_one then evaluates.
The rows of the character table are a basis of the class functions. There are as many of
them as G has conjugacy classes, which is the dimension of the space of class functions, and they
are linearly independent.
Equations
Instances For
The irreducible characters are linearly independent as functions G → k: they are the
basis TauCeti.basisIrreducibleCharacter of the class functions, read in the ambient space.
The rows of the character table are orthonormal, read as class functions: the character
pairing of the representations affording the i-th and j-th irreducible characters is 1 when
i = j and 0 otherwise. This is the orthonormality of the irreducible characters
(TauCeti.ClassFunction.characterPairing_ofCharacter_self and
TauCeti.ClassFunction.characterPairing_ofCharacter_eq_zero) transported along the enumeration.
First (row) orthogonality on the character table: distinct rows pair to 0 and each row
pairs to 1 with itself.
A nontrivial irreducible character is not constant. Over an algebraically closed field of
characteristic zero, if i₀ indexes the trivial character, the constant function 1, and
i ≠ i₀, then the i-th irreducible character takes somewhere a value other than its degree,
which is its value χᵢ(1) at the identity (TauCeti.irreducibleCharacter_one).
TauCeti.exists_irreducibleCharacter_eq_one supplies such an index i₀.
Second (column) orthogonality on the character table, in a form free of division: the
columns at g and at h, weighted by the size of the class of g, sum to |G| when g and h
are conjugate and to 0 otherwise.
Second (column) orthogonality on the character table, in its quotient form.
Second (column) orthogonality at a class and its inverse, indexed by the conjugacy classes
themselves: the column at C against the column at C⁻¹, weighted by the class size |C|,
is |G|.
This is TauCeti.card_conjClass_mul_sum_characterTable_mul_characterTable_inv at a pair of
conjugate elements, restated without a choice of representative.
Second (column) orthogonality at two distinct classes, indexed by the conjugacy classes
themselves: for C ≠ D the column at C pairs with the column at D⁻¹ to 0.
The weight |C| of
TauCeti.card_carrier_mul_sum_characterTable_mul_characterTable_inv cancels here, being nonzero
in k: it divides the invertible |G|.
Complex conjugation of an irreducible character value inverts the group element.
Complex conjugation of a character-table entry inverts the class.
This is not a simp lemma: TauCeti.characterTable_apply already rewrites the left-hand side to
(starRingEnd ℂ) (TauCeti.irreducibleCharacter ℂ i g), which TauCeti.conj_irreducibleCharacter
then normalizes.
Complex conjugation of a character-table entry inverts the class, in the class-indexed
form: TauCeti.conj_characterTable_apply is the same statement about a representative.
First (row) orthogonality over ℂ, in its Hermitian form: the rows of the complex character
table are orthonormal for the Hermitian inner product on class functions.
First (row) orthogonality over ℂ, summed one column at a time: the Hermitian pairing of
two rows of the complex character table, collected over the conjugacy classes with the class sizes
as weights. This is the shape in which the roadmap's specification of a character table asks for row
orthonormality; TauCeti.card_inv_mul_sum_characterTable_mul_conj is the same statement summed over
the group.
The enumeration of the conjugacy classes is an explicit Fintype argument rather than a classical
one, so that the statement is about whichever enumeration the caller has in hand; a caller with
[DecidableEq G] has one, and a classical instance would not be defeq to it.
Second (column) orthogonality over ℂ, in its Hermitian form: two columns of the complex
character table are orthogonal unless they are the same class, in which case they pair to
|G| / |C|.