Factor degrees over a finite field are Frobenius orbit sizes

Let g be a polynomial over a finite field F with q elements and let E be an algebraic extension of F in which g splits. Two groups act on the roots of g in E: the Galois group Polynomial.Gal g, whose orbits are matched with the monic irreducible factors of g in TauCeti/FieldTheory/GaloisGroups/Orbits.lean, and the group generated by the q-th power map, whose orbits are computed in TauCeti/FieldTheory/Finite/MinpolyOrbit.lean. Over a finite base field the two agree, because both orbits of a root are the root set of its minimal polynomial.

Consequently the monic irreducible factors of g correspond to the orbits of the q-th power map on the roots of g, the degree of a factor being the number of elements of the matching orbit. This is the form in which the factorization of a polynomial over a finite field is compared with the cycle type of a permutation of the roots; for a squarefree polynomial the comparison is an equality between the full cycle type and the multiset of factor degrees.

Main results

• TauCeti.FiniteField.image_val_orbit_gal_eq_orbit: over a finite base field the Galois orbit of a root is its Frobenius orbit.
• TauCeti.FiniteField.natCard_orbit_eq_natDegree_factor: along the bijection between orbits and monic irreducible factors, the size of an orbit is the degree of the factor.
• TauCeti.FiniteField.exists_orbit_eq_rootSet_factor: every monic irreducible factor of g is the minimal polynomial of a root, its root set is a single Frobenius orbit, and that orbit has as many elements as the degree of the factor.
• TauCeti.FiniteField.fullCycleType_eq_map_natDegree_normalizedFactors: for squarefree g, a permutation of the roots acting as the q-th power map has full cycle type the multiset of degrees of the monic irreducible factors of g.

References

• [S. Lang, Algebra][serge_lang_algebra], Chapter V, §5.

theorem TauCeti.FiniteField.image_val_orbit_gal_eq_orbit {F : Type u_1} [Field F] [Fintype F] {g : Polynomial F} (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [Fact (Polynomial.map (algebraMap F E) g).Splits] (x : ↑(g.rootSet E)) : Subtype.val '' MulAction.orbit g.Gal x = MulAction.orbit ↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E)) ↑x

Over a finite base field the Galois orbit of a root is its Frobenius orbit: both consist of the roots of its minimal polynomial.

theorem TauCeti.FiniteField.natCard_orbit_eq_natDegree_factor {F : Type u_1} [Field F] [Fintype F] {g : Polynomial F} (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [Fact (Polynomial.map (algebraMap F E) g).Splits] (x : ↑(g.rootSet E)) : Nat.card ↑(MulAction.orbit ↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E)) ↑x) = (↑((orbitQuotientEquivFactors g E ⋯) ⟦x⟧)).natDegree

The size of a Frobenius orbit on the roots of g is the degree of the matching monic irreducible factor of g, along the bijection TauCeti.orbitQuotientEquivFactors between orbits and factors.

theorem TauCeti.FiniteField.exists_orbit_eq_rootSet_factor {F : Type u_1} [Field F] [Fintype F] {g : Polynomial F} (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [Fact (Polynomial.map (algebraMap F E) g).Splits] (hg : g ≠ 0) (q : g.Factors) : ∃ (x : ↑(g.rootSet E)), MulAction.orbit ↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E)) ↑x = (↑q).rootSet E ∧ Nat.card ↑(MulAction.orbit ↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E)) ↑x) = (↑q).natDegree

Every monic irreducible factor of g has a root in E, whose Frobenius orbit is the root set of that factor and has as many elements as its degree.

theorem TauCeti.FiniteField.fullCycleType_eq_map_natDegree_normalizedFactors {F : Type u_1} [Field F] [Fintype F] {g : Polynomial F} (E : Type u_2) [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [Fact (Polynomial.map (algebraMap F E) g).Splits] (hg : Squarefree g) (π : Equiv.Perm ↑(g.rootSet E)) (hπ : ∀ (x : ↑(g.rootSet E)), ↑(π x) = ↑x ^ Fintype.card F) : π.fullCycleType = Multiset.map Polynomial.natDegree (UniqueFactorizationMonoid.normalizedFactors g)

The cycle type of the Frobenius on the roots of a squarefree polynomial is its factorization type. Let g be a squarefree polynomial over a finite field F with q elements, split in an algebraic extension E. A permutation of the roots of g in E that acts as the q-th power map has, counting fixed points, cycle lengths the degrees of the monic irreducible factors of g.