13.2. Fixed points and factors🔗

The kernel of Q_f - I consists of residue classes satisfying h^p = h. If f = f₁ ··· fᵣ is a product of distinct monic irreducibles, the Chinese remainder theorem identifies that kernel with 𝔽_p^r: a fixed residue is constant on each irreducible factor. Its dimension is therefore the number of irreducible factors.

This gives both a test and a factorization procedure:

• f is irreducible exactly when the kernel contains only constants;

• a nonconstant kernel element h splits a current factor by the greatest common divisors gcd(f, h - c) for c ∈ 𝔽_p;

• repeating these splits over a kernel basis produces the complete factorization.

The executable construction uses exact row reduction over 𝔽_p. The product theorem is proved without Mathlib:

Hex.Berlekamp.prod_berlekampFactor {p : ℕ} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) (hmonic : Hex.DensePoly.Monic f)
  [Hex.ZMod64.PrimeModulus p] :
  (Hex.Berlekamp.berlekampFactor f hmonic).product = f
Hex.Berlekamp.prod_berlekampFactor {p : ℕ}
  [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p)
  (hmonic : Hex.DensePoly.Monic f)
  [Hex.ZMod64.PrimeModulus p] :
  (Hex.Berlekamp.berlekampFactor f
        hmonic).product =
    f

HexBerlekampMathlib transfers the result through the ring equivalence with Polynomial (ZMod p) and proves irreducibility of the returned factors.