Burnside's pᵃqᵇ theorem

A finite group whose order has at most two prime divisors is solvable. The proof is the classical character-theoretic one, and it runs through the statement that a conjugacy class of prime-power size larger than one forces a proper nontrivial normal subgroup (TauCeti.not_isSimpleGroup_of_card_carrier_eq_prime_pow), which is where all the representation theory is spent.

The class-size step

Let g have a conjugacy class of size p ^ k with k ≠ 0, and suppose G were simple. Column orthogonality at the classes of g and of 1 reads ∑_χ χ(1) χ(g) = 0, the sum being over the irreducible characters. The trivial character contributes 1. If every other irreducible character either vanished at g or had degree divisible by p, the remaining terms would add up to p times an algebraic integer, making -1/p an algebraic integer; it is rational and not an integer, so some irreducible character χ ≠ 1 has χ(g) ≠ 0 and degree prime to p.

Its degree is then coprime to the class size, so Burnside's vanishing theorem (Representation.char_eq_zero_or_norm_char_eq_finrank) applies and gives ‖χ(g)‖ = χ(1). That is the equality case of the bound on a character value, so the affording representation sends g to a scalar (Representation.exists_apply_eq_smul_of_norm_char_eq_finrank). Its kernel is normal, hence trivial or everything: if it is everything the character is constant and row orthogonality against the trivial character makes its degree 0, which is absurd; and if it is trivial the representation is faithful, so g commutes with everything and its class is a single point, contradicting k ≠ 0.

The induction

TauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow follows by induction on the order. A group with a proper nontrivial normal subgroup is solvable as soon as that subgroup and the quotient are, and both are smaller. A simple group with no q-torsion is a p-group, hence nilpotent. Otherwise the centre of a Sylow q-subgroup Q supplies a nontrivial g whose centralizer contains Q, so its class has size dividing the index of Q, a power of p. A class of size one puts g in the centre, which simplicity then makes all of G, and a larger one contradicts the class-size step.

Main results

• TauCeti.not_isSimpleGroup_of_card_carrier_eq_prime_pow: a conjugacy class of prime-power size larger than one forces a proper nontrivial normal subgroup.
• TauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow: Burnside's pᵃqᵇ theorem, that a finite group of order pᵃqᵇ is solvable, with TauCeti.isSolvable_of_card_dvd_prime_pow_mul_prime_pow the divisibility form that the induction runs in.

References

• W. Burnside, Theory of Groups of Finite Order, 2nd ed. (1911).
• I. M. Isaacs, Character Theory of Finite Groups (1976), Theorem 3.8 and its corollaries.

theorem TauCeti.not_isSimpleGroup_of_card_carrier_eq_prime_pow {G : Type u} [Group G] [Finite G] {g : G} {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (hcard : Nat.card ↑(ConjClasses.mk g).carrier = p ^ k) : ¬IsSimpleGroup G

A conjugacy class of prime-power size larger than one forces a proper normal subgroup. If some element of a finite group has a conjugacy class of size p ^ k with p prime and k ≠ 0, then the group is not simple.

This is the character-theoretic heart of Burnside's pᵃqᵇ theorem: it is what a Sylow argument is fed into.

theorem TauCeti.isSolvable_of_card_dvd_prime_pow_mul_prime_pow {G : Type u} [Group G] [Finite G] {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) {a b : ℕ} (h : Nat.card G ∣ p ^ a * q ^ b) : Group.IsSolvable G

Burnside's pᵃqᵇ theorem, in the form the induction runs in: a finite group whose order divides a product of two prime powers is solvable.

theorem TauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type u} [Group G] [Finite G] {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) {a b : ℕ} (h : Nat.card G = p ^ a * q ^ b) : Group.IsSolvable G

Burnside's pᵃqᵇ theorem: a finite group of order pᵃqᵇ, for primes p and q, is solvable.