The character group of a finite group is the dual of its abelianization

A linear character of a group G, a homomorphism G →* Mˣ into the units of a commutative monoid, kills every commutator, so it factors uniquely through the abelianization. Mathlib's Abelianization.lift is that bijection, and Mathlib's CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity counts the characters of a finite commutative group. Composing the two counts the characters of an arbitrary finite group:

Nat.card (G →* Mˣ) = Nat.card (Abelianization G).

The hypothesis is the one Mathlib's counting theorem carries, asked of the abelianization rather than of G: writing n for Monoid.exponent (Abelianization G), HasEnoughRootsOfUnity M n asks that M contain a primitive n-th root of unity and that the n-th roots of unity in M form a cyclic group. An algebraically closed field of characteristic zero satisfies it for every n. It is a sufficient condition, not one shown here to be necessary, but some hypothesis on M is needed: a character group can collapse for want of roots of unity — over ℝ the group ZMod 3 has only the trivial character, while its abelianization is itself — and it can also grow, since over ℝ × ℝ the group ZMod 2 has four characters rather than two.

In particular a finite group has a nontrivial linear character exactly when it is not perfect, and a perfect group has none at all; the count is what turns a computation of the abelianization into a complete list of linear characters.

Main statements

• TauCeti.card_monoidHom_eq_card_abelianization: the linear characters of a finite group are counted by its abelianization.
• CommGroup.card_monoidHom_not_le_ker: for a finite commutative group G and a subgroup H, the characters of G that are nontrivial on H are #G - #(G ⧸ H) in number, since those trivial on H are the characters of G ⧸ H (Mathlib's CommGroup.card_domRestrictHom_ker).
• CommGroup.finsum_domRestrictHom: for a subgroup H of a finite commutative group G, a function of the restriction to H, summed over the characters of G, is #(G ⧸ H) times its sum over the characters of H.

References

• I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Chapter 2, where the linear characters of G are identified with the characters of G / G'.

theorem TauCeti.card_monoidHom_eq_card_abelianization (G : Type u_1) (M : Type u_2) [Group G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent (Abelianization G))] : Nat.card (G →* Mˣ) = Nat.card (Abelianization G)

The linear characters of a finite group are counted by its abelianization. Every homomorphism G →* Mˣ factors uniquely through Abelianization G, and the characters of a finite commutative group with enough roots of unity in M are as many as its elements.

theorem CommGroup.card_monoidHom_not_le_ker {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) : Nat.card { φ : G →* Mˣ // ¬H ≤ φ.ker } = Nat.card G - Nat.card (G ⧸ H)

The characters nontrivial on a subgroup. If M has enough roots of unity, the homomorphisms G →* Mˣ of a finite commutative group that are not trivial on a subgroup H are #G - #(G ⧸ H) in number: those trivial on H are the characters of G ⧸ H.

theorem CommGroup.finsum_domRestrictHom {G : Type u_1} (M : Type u_2) [CommGroup G] [Finite G] [CommMonoid M] [HasEnoughRootsOfUnity M (Monoid.exponent G)] {N : Type u_3} [AddCommMonoid N] (H : Subgroup G) (g : (↥H →* Mˣ) → N) : ∑ᶠ (χ : G →* Mˣ), g ((MonoidHom.domRestrictHom H Mˣ) χ) = Nat.card (G ⧸ H) • ∑ᶠ (ψ : ↥H →* Mˣ), g ψ

Summing over characters through a restriction. If M has enough roots of unity, every character of a subgroup H of a finite commutative group G extends to exactly #(G ⧸ H) characters of G. So a function g of the restriction to H, summed over the characters of G, is #(G ⧸ H) times its sum over the characters of H.