Irreducible characters are linearly independent

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 for TauCeti.ClassFunction.characterPairing, by Mathlib's first orthogonality relation. A family that is orthogonal for a bilinear form and has nonzero self-pairings is linearly independent, so those characters are linearly independent over k, both as class functions and as functions on G.

Two consequences follow at once. An irreducible representation is determined by its character: two irreducibles with the same character are equivalent, since otherwise a self pairing of 1 would also have to be the cross pairing 0. And a family of pairwise inequivalent irreducibles has at most as many members as G has conjugacy classes, because the class functions have exactly that dimension.

That last bound is in fact an equality, and the equality upgrades the linear independence proved here to a basis of the class functions. Its other half runs through Wedderburn: the blocks of a presentation of k[G] are as many as the conjugacy classes, and each carries an irreducible representation, distinct blocks carrying inequivalent ones (TauCeti/RepresentationTheory/CharacterTable/BlockRepresentation.lean). Completeness, the resulting basis and the second orthogonality relation are proved in TauCeti/RepresentationTheory/CharacterTable/Completeness.lean, downstream of this file; nothing below uses them.

Main results

• TauCeti.ClassFunction.linearIndependent_ofCharacter and TauCeti.ClassFunction.linearIndependent_character: the characters of pairwise inequivalent irreducible representations are linearly independent, as class functions and as functions on G; TauCeti.ClassFunction.linearIndependent_ofFDRep and TauCeti.ClassFunction.linearIndependent_character_fdRep are the FDRep mirrors.
• Representation.nonempty_equiv_of_character_eq_of_isIrreducible and FDRep.nonempty_iso_of_character_eq_of_simple: an irreducible representation is determined by its character.
• TauCeti.ClassFunction.card_le_card_conjClasses and TauCeti.ClassFunction.card_le_card_conjClasses_fdRep: there are at most as many pairwise inequivalent irreducibles as there are conjugacy classes.
• TauCeti.Representation.nonempty_equiv_iff_eq: inside a pairwise inequivalent family, two members are equivalent exactly when they are the same member. This one needs neither irreducibility nor any hypothesis on k and G; it is the form in which the pairwise-inequivalence hypothesis is used downstream.

Implementation notes

The pairing enters only through the split orthonormality lemmas of TauCeti/RepresentationTheory/CharacterTable/Pairing.lean, so these statements ask for Finite G and produce the Fintype inside their proofs.

References

• Character theory roadmap. Everything here is proved from Layer 0's characterPairing and its orthonormality, which are on main, together with Mathlib's char_orthonormal; no Layer 1, Layer 2 or Layer 3 material is used, and none is presupposed. What the file supplies is prerequisite material for the later layers: that a character determines its irreducible is the injectivity of the map character : Irreps k G → ClassFunction k G that Layer 2.5 asks for, and the cardinality bound is the ≤ half of Layer 2's count Nat.card (Irreps k G) = Nat.card (ConjClasses G), obtained without Wedderburn. Layer 3's completeness item, the spanning statement and the orthonormal basis, is proved downstream in TauCeti/RepresentationTheory/CharacterTable/Completeness.lean from the linear independence proved here and the ≥ half of the count.
• I. M. Isaacs, Character Theory of Finite Groups (1976), Theorem 2.8 and Corollary 2.9.

Linear independence

theorem TauCeti.ClassFunction.linearIndependent_ofCharacter {k : Type u} {G : Type v} [Field k] [Group G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] [Finite G] {ι : Type u_1} {V : ι → Type w} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h : Pairwise fun (i j : ι) => IsEmpty ((ρ i).Equiv (ρ j))) : LinearIndependent k fun (i : ι) => ofCharacter (ρ i)

The characters of pairwise inequivalent irreducible representations are linearly independent as class functions: they are orthogonal for the character pairing, and each pairs to 1 with itself.

theorem TauCeti.ClassFunction.linearIndependent_character {k : Type u} {G : Type v} [Field k] [Group G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] [Finite G] {ι : Type u_1} {V : ι → Type w} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h : Pairwise fun (i j : ι) => IsEmpty ((ρ i).Equiv (ρ j))) : LinearIndependent k fun (i : ι) => (ρ i).character

The characters of pairwise inequivalent irreducible representations are linearly independent as functions on G.

theorem TauCeti.ClassFunction.linearIndependent_ofFDRep {k : Type u} {G : Type v} [Field k] [Group G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] [Finite G] {ι : Type u_1} (X : ι → FDRep k G) [∀ (i : ι), CategoryTheory.Simple (X i)] (h : Pairwise fun (i j : ι) => IsEmpty (X i ≅ X j)) : LinearIndependent k fun (i : ι) => ofFDRep (X i)

The characters of pairwise non-isomorphic simple objects of FDRep k G are linearly independent as class functions.

theorem TauCeti.ClassFunction.linearIndependent_character_fdRep {k : Type u} {G : Type v} [Field k] [Group G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] [Finite G] {ι : Type u_1} (X : ι → FDRep k G) [∀ (i : ι), CategoryTheory.Simple (X i)] (h : Pairwise fun (i j : ι) => IsEmpty (X i ≅ X j)) : LinearIndependent k fun (i : ι) => (X i).character

The characters of pairwise non-isomorphic simple objects of FDRep k G are linearly independent as functions on G.

An irreducible representation is determined by its character

theorem Representation.nonempty_equiv_of_character_eq_of_isIrreducible {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {V W : Type w} [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) [ρ.IsIrreducible] [σ.IsIrreducible] (h : ρ.character = σ.character) : Nonempty (σ.Equiv ρ)

An irreducible representation is determined by its character: two irreducible representations with the same character are equivalent.

Members of a pairwise inequivalent family

@[simp]

theorem TauCeti.Representation.nonempty_equiv_iff_eq {k : Type u} {G : Type v} [Semiring k] [Monoid G] {ι : Type u_1} {V : ι → Type w} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] (ρ : (i : ι) → Representation k G (V i)) (hind : Pairwise fun (i j : ι) => IsEmpty ((ρ i).Equiv (ρ j))) {i j : ι} : Nonempty ((ρ i).Equiv (ρ j)) ↔ i = j

Inside a family of pairwise inequivalent representations, two members are equivalent exactly when they are the same member.

theorem FDRep.nonempty_iso_of_character_eq_of_simple {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (X Y : FDRep k G) [CategoryTheory.Simple X] [CategoryTheory.Simple Y] (h : X.character = Y.character) : Nonempty (X ≅ Y)

A simple object of FDRep k G is determined by its character: two simple objects with the same character are isomorphic.

Counting irreducibles against conjugacy classes

theorem TauCeti.ClassFunction.card_le_card_conjClasses {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type u_1} [Fintype ι] {V : ι → Type w} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) [∀ (i : ι), (ρ i).IsIrreducible] (h : Pairwise fun (i j : ι) => IsEmpty ((ρ i).Equiv (ρ j))) : Fintype.card ι ≤ Nat.card (ConjClasses G)

There are at most as many pairwise inequivalent irreducible representations as there are conjugacy classes: their characters are linearly independent in the space of class functions, whose dimension is the number of conjugacy classes.

theorem TauCeti.ClassFunction.card_le_card_conjClasses_fdRep {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type u_1} [Fintype ι] (X : ι → FDRep k G) [∀ (i : ι), CategoryTheory.Simple (X i)] (h : Pairwise fun (i j : ι) => IsEmpty (X i ≅ X j)) : Fintype.card ι ≤ Nat.card (ConjClasses G)

There are at most as many pairwise non-isomorphic simple objects of FDRep k G as there are conjugacy classes of G.