Finite-group representations are determined by their characters

For a finite group over a field of characteristic zero, two finite-dimensional representations with the same character are equivalent. Maschke's theorem makes their group-algebra modules semisimple, while the character pairing identifies the dimension of every intertwiner space. The reconstruction theorem in TauCeti/RingTheory/Semisimple/Multiplicity.lean then shows that the modules are equivalent.

Main results

• Representation.nonempty_equiv_of_character_eq: equal characters determine equivalent finite-dimensional representations.
• FDRep.nonempty_iso_of_character_eq: the bundled FDRep form.
• FDRep.finrank_hom_eq_sum_of_character_eq: an identity χ_X = ∑ᵢ aᵢ • χ_{Yᵢ} with natural-number coefficients gives dim Hom(V, X) = ∑ᵢ aᵢ · dim Hom(V, Yᵢ) for every V.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part I, §§2.3 and 2.5.
• C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §§25 and 30.

This is the object-level input to the injectivity target in Layer 6 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md.

theorem Representation.nonempty_equiv_of_character_eq {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] {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) (hchar : ρ.character = σ.character) : Nonempty (ρ.Equiv σ)

For a finite group over a field of characteristic zero, finite-dimensional representations are determined by their characters.

theorem FDRep.nonempty_iso_of_character_eq {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] (X Y : FDRep k G) (hchar : X.character = Y.character) : Nonempty (X ≅ Y)

For a finite group over a field of characteristic zero, objects of FDRep are determined by their characters.

theorem FDRep.finrank_hom_eq_sum_of_character_eq {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] {ι : Type u_1} [Fintype ι] (V : FDRep k G) {X : FDRep k G} {Y : ι → FDRep k G} {a : ι → ℕ} (hX : X.character = ∑ i : ι, a i • (Y i).character) : Module.finrank k (V ⟶ X) = ∑ i : ι, a i * Module.finrank k (V ⟶ Y i)

A character identity determines multiplicities. For a finite group over a field of characteristic zero, if the character of X is a combination ∑ᵢ aᵢ • χ_{Yᵢ} of characters with natural-number coefficients, then for every V the dimension of Hom(V, X) is ∑ᵢ aᵢ · dim Hom(V, Yᵢ).