Injectivity of the character map on the representation ring

Let G be a finite group and k a field of characteristic zero. This file proves that the character homomorphism from the representation ring of G is injective. Thus a virtual representation is determined by its character.

For the representation ring itself, every element of split K₀ is a difference [V] - [W]. A difference in the kernel has V.character = W.character, so the object-level theorem makes V and W isomorphic and their difference vanishes. The object-level input is FDRep.nonempty_iso_of_character_eq, proved in TauCeti/RepresentationTheory/CharacterTable/Determined.lean from Maschke decompositions and the character pairing.

Main results

• TauCeti.repRingCharacter_injective: the character homomorphism on the representation ring is injective.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part II, §9.1.

This is the injectivity target in Layer 6 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md.

theorem TauCeti.repRingCharacter_injective {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] : Function.Injective ⇑(repRingCharacter k G)

For a finite group over a field of characteristic zero, the character homomorphism is injective. Thus every virtual representation is determined by its character.