Completeness of the irreducible characters, and the second orthogonality relation #
Let G be a finite group and k an algebraically closed field in which |G| is invertible. The
characters of pairwise inequivalent irreducible representations of G are orthonormal, hence
linearly independent, and there are at most as many of them as G has conjugacy classes
(TauCeti/RepresentationTheory/CharacterTable/Independence.lean). This file supplies the matching
lower bound and everything it unlocks.
The lower bound comes from the Wedderburn presentation of k[G]: its blocks are indexed by the
conjugacy classes and each carries an irreducible representation, pairwise inequivalent
(TauCeti.exists_irreducible_family_conjClasses). A family of that size therefore has linearly
independent characters in a space of exactly that dimension, so the characters are a basis of the
class functions: this is completeness, and TauCeti.ClassFunction.le_span_irreducibleCharacters
is the spanning statement it amounts to.
Expanding a class function in that basis is easy because the basis is orthonormal for
TauCeti.ClassFunction.characterPairing: the coefficient of χᵢ in f is ⟨χᵢ, f⟩, so a class
function is determined by its pairings with the χᵢ. Applying the expansion to the indicator
function of a conjugacy class, whose pairings are computed by
TauCeti.ClassFunction.characterPairing_classIndicator_inv, gives the second (column)
orthogonality relation |C_g| · ∑ᵢ χᵢ(g) χᵢ(h⁻¹) = |G| or 0 according as g and h are
conjugate or not.
Main statements #
TauCeti.ClassFunction.basisOfIrreducibleCharacters: the characters of a family of pairwise inequivalent irreducible representations indexed by as many indices asGhas conjugacy classes form a basis of the class functions, withTauCeti.ClassFunction.exists_basis_ofCharacterthe statement that such a family exists.TauCeti.ClassFunction.le_span_irreducibleCharacters: completeness, in the form that every class function lies in the span of the irreducible characters.TauCeti.ClassFunction.sum_characterPairing_smul_ofCharacter: the expansion of a class function in that basis, with coefficients the pairings against the irreducible characters, andTauCeti.ClassFunction.eq_of_forall_characterPairing_ofCharacter_eqthe consequence that a class function is determined by those pairings.TauCeti.ClassFunction.exists_nonempty_equiv: such a family is a complete list of the irreducibles, every irreducible representation being equivalent to one of its members.TauCeti.ClassFunction.card_conjClass_mul_sum_char_mul_char_inv: the second orthogonality relation, in a form free of division, andTauCeti.ClassFunction.sum_char_mul_char_invin the quotient form|G| / |C_g|.
Implementation notes #
The irreducibles are produced on the coordinate spaces Fin n → k rather than as simple objects of
FDRep k G, because a Wedderburn block is a matrix algebra acting on its column space, and because
FDRep k G carries only representations on types in the universe of k. The
Representation-level statements are the ones the rest of the theory uses; a consumer holding a
simple object of FDRep k G reaches them through FDRep.simple_iff_isIrreducible.
References #
This implements the completeness and second-orthogonality items of Layer 3 of the
character theory roadmap,
at the Representation level. Its Suggested.lean pins them as irreducibleCharacters_span, over
the simple objects of FDRep k G, and char_column_orthogonality, over the ℂ-valued character
table; the statements below are the prerequisites those two are read off from, and neither roadmap
name is claimed here. Reading irreducibleCharacters_span off from
TauCeti.ClassFunction.le_span_irreducibleCharacters needs two further steps: the dictionary
FDRep.simple_iff_isIrreducible between CategoryTheory.Simple in FDRep k G and
Representation.IsIrreducible, which lives in TauCeti.RepresentationTheory.Simple.Basic and which
this file does not import, and a comparison of the two spanning sets, which is not done here.
See I. M. Isaacs, Character Theory of Finite Groups (1976), Theorem 2.18 and Corollary 2.14, or
J.-P. Serre, Linear Representations of Finite Groups, Sections 2.5 and 6.4.
The irreducible characters are a basis of the class functions. The characters of a family of
pairwise inequivalent irreducible representations are linearly independent, and if the family is
indexed by as many indices as G has conjugacy classes then there are as many of them as the
dimension of the class functions.
Equations
- TauCeti.ClassFunction.basisOfIrreducibleCharacters ρ hind hcard = basisOfLinearIndependentOfCardEqFinrank' (fun (i : ι) => TauCeti.ClassFunction.ofCharacter (ρ i)) ⋯ ⋯
Instances For
Completeness: the irreducible characters span the class functions.
The expansion of a class function in the basis of irreducible characters. The basis is
orthonormal for the character pairing, so the coefficient of χᵢ is the pairing ⟨χᵢ, f⟩.
A class function is determined by its pairings with the irreducible characters: two class functions with the same pairing against every character of a complete family of pairwise inequivalent irreducible representations are equal.
The pointwise form of the expansion of a class function in the irreducible characters.
The second (column) orthogonality relation, in a form free of division: the columns of the
character table 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.
The second (column) orthogonality relation in its quotient form: the columns of the
character table at g and at h sum to |G| / |C_g| when g and h are conjugate, and to 0
otherwise.
A complete family exhausts the irreducibles: every finite-dimensional irreducible
representation of G is equivalent to a member of the family. Were it equivalent to none of them,
its character would be orthogonal to a basis of the class functions, hence zero; but an irreducible
character pairs to 1 with itself.
The irreducible characters of a finite group are a basis of its class functions. There is a
family of pairwise inequivalent irreducible representations of G indexed by the conjugacy classes
of G, and its characters are a basis of the class functions.
The count is sharp in both directions: no larger family of pairwise inequivalent irreducibles exists
by TauCeti.ClassFunction.card_le_card_conjClasses.
Completeness: every class function is a linear combination of irreducible characters.
Only this inclusion is stated: every character is itself a class function, so the span is contained
in TauCeti.ClassFunction k G for free, and the irreducible characters do not span all of G → k
unless G is abelian.
This is the Representation-level form, spanning by the characters of the irreducible
representations on the coordinate spaces Fin n → k that the Wedderburn blocks produce. It is a
prerequisite for, and not the same statement as, the roadmap's irreducibleCharacters_span, which
spans by the characters of the simple objects of FDRep k G: passing between the two needs
FDRep.simple_iff_isIrreducible and a comparison of the two spanning sets, which is not
done here.