The good-prime structure theorem

The Burnside--Dixon--Schneider algorithm computes over ZMod p instead of over ℂ, and the theorem that licenses the substitution is this one: at a good Dixon prime the centre of ZMod p [G] looks exactly like the centre of ℂ[G], namely a product of r copies of the coefficient field, r the number of conjugacy classes.

Two of the three arithmetic conditions in TauCeti.IsGoodDixonPrime are what make this work: p ∤ |G| and Monoid.exponent G ∣ p - 1. The first makes |G| invertible modulo p; the second says g ^ p = g for every g : G, so that ZMod p already contains the eigenvalues of every group element. Dixon's size bound plays no part here -- it is about the lift back to characteristic zero, not about the modular computation.

Everything is inherited from TauCeti/RepresentationTheory/CharacterTable/FiniteField.lean, which proves the statement for an arbitrary finite coefficient field satisfying those two conditions; ZMod p has p elements, so g ^ Fintype.card (ZMod p) = g is exactly the exponent condition.

Main results

• TauCeti.IsGoodDixonPrime.pow_prime_eq_self: g ^ p = g at a good Dixon prime.
• TauCeti.IsGoodDixonPrime.center_pow_prime: the modular centre is fixed by the Frobenius.
• TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_conjClasses and TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_pi: the good-prime structure theorem, Z(ZMod p [G]) ≃ₐ[ZMod p] (ConjClasses G → ZMod p), indexed by the conjugacy classes and by Fin r respectively.

References

• J. D. Dixon, High speed computation of group characters, Numerische Mathematik 10 (1967), 446--450.
• The roadmap RepresentationTheory/CharacterTheory, Layer 6, "The good-prime structure theorem".

theorem TauCeti.IsGoodDixonPrime.pow_prime_eq_self {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) (g : G) : g ^ p = g

Every group element is fixed by the p-th power map at a good Dixon prime. The exponent of G divides p - 1, so g ^ (p - 1) = 1. This is the group-side form of the condition that ZMod p contains the e-th roots of unity.

theorem TauCeti.IsGoodDixonPrime.center_pow_prime {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) {y : MonoidAlgebra (ZMod p) G} (hy : y ∈ Subalgebra.center (ZMod p) (MonoidAlgebra (ZMod p) G)) : y ^ p = y

The modular centre is fixed by the Frobenius. Every central element y of ZMod p [G] satisfies y ^ p = y; equivalently, the central characters take values in the prime field rather than in a proper extension of it. This is the mechanism behind the structure theorem.

theorem TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_conjClasses {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : Nonempty (↥(Subalgebra.center (ZMod p) (MonoidAlgebra (ZMod p) G)) ≃ₐ[ZMod p] ConjClasses G → ZMod p)

The good-prime structure theorem. At a good Dixon prime the centre of ZMod p [G] is the algebra of ZMod p-valued functions on the conjugacy classes of G.

This is what guarantees that the class-multiplication matrices are simultaneously diagonalizable over ZMod p with exactly r distinct common eigenrows, so that the eigenvector search of the Burnside--Dixon--Schneider algorithm terminates in one-dimensional common eigenspaces, with no bad-prime merging of distinct central characters.

theorem TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_pi {G : Type u_1} [Group G] {p : ℕ} (hp : IsGoodDixonPrime G p) : Nonempty (↥(Subalgebra.center (ZMod p) (MonoidAlgebra (ZMod p) G)) ≃ₐ[ZMod p] Fin (Nat.card (ConjClasses G)) → ZMod p)

The good-prime structure theorem with the factors indexed by Fin r rather than by the conjugacy classes themselves: the shape in which the finite-field linear algebra of the Burnside--Dixon--Schneider algorithm consumes it.