Good Dixon primes

The Burnside--Dixon--Schneider algorithm computes the complex character table of a finite group G by working over a finite prime field ZMod p and lifting the answer back. The prime it works over cannot be arbitrary: it has to make ZMod p behave, for the purposes of the computation, like ℂ, and it has to be large enough that the lift is unambiguous. This file isolates that condition as TauCeti.IsGoodDixonPrime and proves what it buys.

Three arithmetic conditions do the work. That p does not divide |G| makes ZMod p [G] semisimple, by Maschke. That the exponent e of G divides p - 1 makes every element of G act with eigenvalues in ZMod p, because the e-th roots of unity are already there: ZMod p contains a primitive e-th root of unity and X ^ e - 1 splits into distinct linear factors over it. And Dixon's size bound 2⌊√|G|⌋ < p opens a residue window wide enough that an integer of absolute value at most √|G| -- the size of the coefficients the algorithm has to reconstruct -- is determined by its residue modulo p.

Such primes always exist: there are arbitrarily large primes congruent to 1 modulo e (Nat.exists_prime_gt_modEq_one, itself a cyclotomic-polynomial argument), and any of them beyond max |G| (2⌊√|G|⌋) is good. The existence proof is not part of any computation. What the computation does instead is search: TauCeti.DixonPrimeData.candidates tests the numbers e + 1, 2e + 1, 3e + 1, … in turn, keeps the good primes among them, and pairs each with the least primitive e-th root of unity modulo it (TauCeti.ZMod.primitiveRoot?). The existence theorem then says that the search reaches every good prime once it runs far enough (TauCeti.DixonPrimeData.exists_mem_candidates).

Main definitions

• TauCeti.IsGoodDixonPrime: the good-prime predicate.
• TauCeti.DixonPrimeData: a good prime together with a choice of primitive e-th root of unity modulo it, the data the algorithm consumes.
• TauCeti.DixonPrimeData.ofPrime?: the Dixon prime data at a given prime, if it is good.
• TauCeti.DixonPrimeData.candidates: the Dixon prime data at the good primes among the first numbers congruent to 1 modulo the exponent.

Main results

• TauCeti.IsGoodDixonPrime.isSemisimpleRing: the modular group algebra is semisimple.
• TauCeti.IsGoodDixonPrime.exists_isPrimitiveRoot and TauCeti.IsGoodDixonPrime.splits_X_pow_exponent_sub_one: ZMod p splits X ^ e - 1.
• TauCeti.IsGoodDixonPrime.card_nthRootsFinset: that splitting has e distinct roots.
• TauCeti.IsGoodDixonPrime.isSemisimple_apply: every group element acts semisimply in a representation over ZMod p.
• TauCeti.IsGoodDixonPrime.two_mul_natAbs_lt_of_natAbs_le_sqrt, TauCeti.IsGoodDixonPrime.valMinAbs_intCast_of_natAbs_le_sqrt and TauCeti.IsGoodDixonPrime.eq_of_intCast_eq_of_natAbs_le_sqrt: an integer bounded by √|G| is recovered from, and so determined by, its residue modulo p. This is what the size bound is for.
• TauCeti.exists_isGoodDixonPrime: good Dixon primes exist for every finite group.
• TauCeti.DixonPrimeData.isSome_ofPrime?_iff: the data at p is found exactly when p is a good Dixon prime.
• TauCeti.DixonPrimeData.mem_candidates_iff and TauCeti.DixonPrimeData.exists_mem_candidates: the search returns the data at every good prime within its range, and nothing else.

Implementation notes

TauCeti.DixonPrimeData carries the primitive root as a field rather than choosing one with the axiom of choice, because the algorithm that consumes it is meant to run: a noncomputable root would make every downstream def noncomputable. The existence statement is therefore phrased twice, once as the proposition TauCeti.exists_isGoodDixonPrime and once as TauCeti.instNonemptyDixonPrimeData.

References

• J. D. Dixon, High speed computation of group characters, Numerische Mathematik 10 (1967), 446--450.
• G. Schneider, Dixon's character table algorithm revisited, J. Symbolic Comput. 9 (1990), 601--606.
• The roadmap RepresentationTheory/CharacterTheory, Layer 6, "Certified Dixon prime data".

The good-prime predicate

structure TauCeti.IsGoodDixonPrime (G : Type u_1) [Group G] (p : ℕ) : Prop

p is a good Dixon prime for G: it is prime, it does not divide |G|, the exponent of G divides p - 1, and it exceeds Dixon's size bound 2⌊√|G|⌋.

These are exactly the arithmetic hypotheses under which the Burnside--Dixon--Schneider algorithm runs: not_dvd_natCard makes ZMod p [G] semisimple, exponent_dvd puts the e-th roots of unity into ZMod p, and two_mul_sqrt_lt makes the lift back to characteristic zero unique. That the reduced central characters stay pairwise distinct is not part of the definition; it is a consequence, the content of the good-prime structure theorem.

• prime : Nat.Prime p

  p is prime, so that ZMod p is a field.

• not_dvd_natCard : ¬p ∣ Nat.card G

  p does not divide |G|, so that Maschke applies over ZMod p.

• exponent_dvd : Monoid.exponent G ∣ p - 1

  The exponent of G divides p - 1, so that the e-th roots of unity lie in ZMod p.

• two_mul_sqrt_lt : 2 * (Nat.card G).sqrt < p

  Dixon's size bound, which makes the lift back to characteristic zero unique.

theorem TauCeti.IsGoodDixonPrime.fact_prime {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : Fact (Nat.Prime p)

The primality of a good Dixon prime, as the Fact that the field structure on ZMod p is found from.

theorem TauCeti.IsGoodDixonPrime.finite {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : Finite G

A group with a good Dixon prime is finite. Every natural number divides 0, so p ∤ |G| already rules out Nat.card G = 0; finiteness need not be assumed separately.

The exponent condition

theorem TauCeti.IsGoodDixonPrime.exists_isPrimitiveRoot {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : ∃ (ζ : ZMod p), IsPrimitiveRoot ζ (Monoid.exponent G)

ZMod p contains a primitive root of unity of order the exponent of G. This is the exponent condition at work: the exponent divides p - 1, and ZMod p has the roots of unity of every order dividing p - 1, by TauCeti.ZMod.exists_isPrimitiveRoot_of_dvd_sub_one.

The order condition: Maschke

theorem TauCeti.IsGoodDixonPrime.natCast_natCard_ne_zero {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : ↑(Nat.card G) ≠ 0

The order of G is invertible modulo a good Dixon prime.

theorem TauCeti.IsGoodDixonPrime.neZero_natCast_natCard {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : NeZero ↑(Nat.card G)

theorem TauCeti.IsGoodDixonPrime.isSemisimpleRing {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : IsSemisimpleRing (MonoidAlgebra (ZMod p) G)

Maschke's theorem at a good Dixon prime: the modular group algebra ZMod p [G] is a semisimple ring.

Splitting the roots of unity

theorem TauCeti.IsGoodDixonPrime.splits_X_pow_exponent_sub_one {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : (Polynomial.X ^ Monoid.exponent G - 1).Splits

X ^ e - 1 splits over ZMod p, e the exponent of G: this is the sense in which a good Dixon prime makes ZMod p a substitute for ℂ.

theorem TauCeti.IsGoodDixonPrime.card_nthRootsFinset {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] (hp : IsGoodDixonPrime G p) : (Polynomial.nthRootsFinset (Monoid.exponent G) 1).card = Monoid.exponent G

The e-th roots of unity in ZMod p are e in number: X ^ e - 1 splits with distinct roots, which is what makes the elements of G act semisimply.

The Fact instance is redundant with hp.prime, but it cannot be dropped: Polynomial.nthRootsFinset is defined only over an IsDomain, and IsDomain (ZMod p) is found from Fact p.Prime, so without the instance argument the statement fails to elaborate. Deriving it inside the proof is therefore not an option, unlike in TauCeti.IsGoodDixonPrime.splits_X_pow_exponent_sub_one, whose Polynomial.Splits is defined over any commutative ring.

The size condition: the residue window

theorem TauCeti.IsGoodDixonPrime.neZero {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : NeZero p

theorem TauCeti.IsGoodDixonPrime.two_mul_natAbs_lt_of_natAbs_le_sqrt {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) {z : ℤ} (hz : z.natAbs ≤ (Nat.card G).sqrt) : 2 * z.natAbs < p

Dixon's size bound in the shape the residue window asks for. An integer of absolute value at most ⌊√|G|⌋ lies strictly inside the window of half-width p / 2, since 2⌊√|G|⌋ < p.

theorem TauCeti.IsGoodDixonPrime.valMinAbs_intCast_of_natAbs_le_sqrt {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) {z : ℤ} (hz : z.natAbs ≤ (Nat.card G).sqrt) : (↑z).valMinAbs = z

The certified rational-integer lift at a good Dixon prime. Dixon's size bound opens a residue window wide enough that an integer of absolute value at most ⌊√|G|⌋ is returned by ZMod.valMinAbs from its residue. This is the first stage of the cyclotomic lift: a rational character value, reduced modulo p, is recovered exactly.

theorem TauCeti.IsGoodDixonPrime.eq_of_intCast_eq_of_natAbs_le_sqrt {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) {z w : ℤ} (hz : z.natAbs ≤ (Nat.card G).sqrt) (hw : w.natAbs ≤ (Nat.card G).sqrt) (h : ↑z = ↑w) : z = w

Dixon's size bound opens a wide enough residue window. Two integers of absolute value at most ⌊√|G|⌋ that agree modulo p are equal, so an integer of that size is determined by its residue. This is why the lift is unambiguous.

Representations over ZMod p

theorem TauCeti.IsGoodDixonPrime.isSemisimple_apply {G : Type u_1} [Group G] {p : ℕ} {V : Type u_2} [AddCommGroup V] [Module (ZMod p) V] (hp : IsGoodDixonPrime G p) (ρ : Representation (ZMod p) G V) (g : G) : Module.End.IsSemisimple (ρ g)

At a good Dixon prime every group element acts semisimply. This is Representation.isSemisimple_apply at the invertibility of |G| that the good-prime certificate supplies.

Existence

theorem TauCeti.exists_isGoodDixonPrime (G : Type u_1) [Group G] [Finite G] : ∃ (p : ℕ), IsGoodDixonPrime G p

Good Dixon primes exist. Take a prime congruent to 1 modulo the exponent of G and larger than max |G| (2⌊√|G|⌋), the second half being Dixon's size bound; there are arbitrarily large such primes. This is a statement about the algorithm, not a step in it: a concrete group is handed a concrete prime instead.

structure TauCeti.DixonPrimeData (G : Type u_1) [Group G] : Type

The data the Burnside--Dixon--Schneider algorithm runs on: a good Dixon prime p for G together with a chosen primitive e-th root of unity modulo p, e the exponent of G. The root is data rather than a choice made by exists_isPrimitiveRoot, so that the definitions consuming it stay computable.

• p : ℕ

  The prime the algorithm reduces modulo.

• root : ZMod self.p

  The primitive e-th root of unity modulo p, e the exponent of G, that the finite-field computation runs with.

• isGoodDixonPrime : IsGoodDixonPrime G self.p

  The certificate that p is a good Dixon prime.

• isPrimitiveRoot_root : IsPrimitiveRoot self.root (Monoid.exponent G)

  The certificate that root is a primitive e-th root of unity.

theorem TauCeti.DixonPrimeData.ext_iff {G : Type u_1} {inst✝ : Group G} {x y : DixonPrimeData G} : x = y ↔ x.p = y.p ∧ x.root ≍ y.root

theorem TauCeti.DixonPrimeData.ext {G : Type u_1} {inst✝ : Group G} {x y : DixonPrimeData G} (p : x.p = y.p) (root : x.root ≍ y.root) : x = y

instance TauCeti.DixonPrimeData.fact_prime {G : Type u_1} [Group G] (d : DixonPrimeData G) : Fact (Nat.Prime d.p)

The prime is prime, as the Fact the field structure on ZMod d.p is found from. Unlike for the hypothesis IsGoodDixonPrime, this can be an instance, because d is data.

instance TauCeti.DixonPrimeData.neZero {G : Type u_1} [Group G] (d : DixonPrimeData G) : NeZero d.p

@[simp]

theorem TauCeti.DixonPrimeData.orderOf_root {G : Type u_1} [Group G] (d : DixonPrimeData G) : orderOf d.root = Monoid.exponent G

The chosen root has order exactly the exponent of G.

@[simp]

theorem TauCeti.DixonPrimeData.root_pow_exponent_eq_one {G : Type u_1} [Group G] (d : DixonPrimeData G) : d.root ^ Monoid.exponent G = 1

The defining property of the chosen root: it is an e-th root of unity, e the exponent of G.

theorem TauCeti.DixonPrimeData.isUnit_root {G : Type u_1} [Group G] (d : DixonPrimeData G) : IsUnit d.root

The chosen root is a unit, so the finite-field computation may divide by it.

theorem TauCeti.DixonPrimeData.root_ne_zero {G : Type u_1} [Group G] (d : DixonPrimeData G) : d.root ≠ 0

instance TauCeti.instNonemptyDixonPrimeData (G : Type u_1) [Group G] [Finite G] : Nonempty (DixonPrimeData G)

Every finite group admits Dixon prime data. The witness is noncomputable; a computation that needs the data finds it with TauCeti.DixonPrimeData.candidates instead.

Searching for Dixon prime data

The order and the exponent of G enter the search as natural numbers n and e, together with proofs that they are Nat.card G and Monoid.exponent G: Mathlib's Monoid.exponent is noncomputable, and a caller that runs the search supplies the two numbers it already knows.

def TauCeti.DixonPrimeData.ofPrime? {G : Type u_1} [Group G] (e : ℕ) (he : e = Monoid.exponent G) (n : ℕ) (hn : n = Nat.card G) (p : ℕ) : Option (DixonPrimeData G)

The Dixon prime data at p, if p is a good Dixon prime. The four arithmetic conditions of TauCeti.IsGoodDixonPrime are decided on the numbers n and e, and the primitive root is the least one modulo p (TauCeti.ZMod.primitiveRoot?).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DixonPrimeData.p_eq_of_ofPrime?_eq_some {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {p : ℕ} {q : DixonPrimeData G} (h : ofPrime? e he n hn p = some q) : q.p = p

Data returned at p lives at the prime p.

theorem TauCeti.DixonPrimeData.isSome_ofPrime?_iff {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {p : ℕ} : (ofPrime? e he n hn p).isSome = true ↔ IsGoodDixonPrime G p

The data at p is found exactly when p is a good Dixon prime. A good prime has a primitive e-th root of unity, so the root search at it cannot fail.

theorem TauCeti.DixonPrimeData.ofPrime?_eq_some {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {q : DixonPrimeData G} (hroot : Option.map Subtype.val (ZMod.primitiveRoot? q.p e) = some q.root) : ofPrime? e he n hn q.p = some q

The search returns given Dixon prime data at its prime as soon as its root is the one the primitive-root search finds there.

def TauCeti.DixonPrimeData.candidates {G : Type u_1} [Group G] (e : ℕ) (he : e = Monoid.exponent G) (n : ℕ) (hn : n = Nat.card G) (fuel : ℕ) : List (DixonPrimeData G)

The search for Dixon prime data. The numbers e (k + 1) + 1 for k < fuel are tested in increasing order, and the Dixon prime data at each good prime among them is kept. When e ≠ 0 (for instance when G is finite), these are exactly the numbers above 1 and at most e · fuel + 1 congruent to 1 modulo e.

Equations

• TauCeti.DixonPrimeData.candidates e he n hn fuel = List.filterMap (fun (k : ℕ) => TauCeti.DixonPrimeData.ofPrime? e he n hn (e * (k + 1) + 1)) (List.range fuel)

theorem TauCeti.DixonPrimeData.mem_candidates_iff {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {fuel : ℕ} {q : DixonPrimeData G} : q ∈ candidates e he n hn fuel ↔ ofPrime? e he n hn q.p = some q ∧ q.p ≤ e * fuel + 1

The search finds the data at every good prime within its range, and nothing else. The data q is found within fuel steps exactly when it is the data the search computes at its prime and that prime is at most e · fuel + 1.

theorem TauCeti.DixonPrimeData.exists_mem_candidates {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {p fuel : ℕ} (hp : IsGoodDixonPrime G p) (hfuel : p ≤ e * fuel + 1) : ∃ q ∈ candidates e he n hn fuel, q.p = p

Every good Dixon prime is reached by the search once it runs far enough.

theorem TauCeti.DixonPrimeData.candidates_prefix {G : Type u_1} [Group G] {e : ℕ} {he : e = Monoid.exponent G} {n : ℕ} {hn : n = Nat.card G} {fuel fuel' : ℕ} (h : fuel ≤ fuel') : candidates e he n hn fuel <+: candidates e he n hn fuel'

Running the search longer only appends to what it has already found.