The Frobenius orbit of an element algebraic over a finite field

Let F be a finite field with q elements and let E be an algebraic extension of F. Raising to the q-th power is an F-algebra automorphism of E, Mathlib's FiniteField.frobeniusAlgEquivOfAlgebraic, and this file computes the orbit of x : E under the group it generates. That orbit is the root set of the minimal polynomial of x, and

minpoly F x = ∏ β ∈ orbit, (X - β)

once the minimal polynomial is mapped into E[X]. So the minimal polynomial splits in E with simple roots, its degree is the number of elements of the orbit, and two elements of E lie in one orbit exactly when they have the same minimal polynomial.

Neither finiteness of E nor normality of E / F is assumed; an algebraic closure of F is the intended example. Over an infinite algebraic extension the group generated by the Frobenius is a proper subgroup of the full automorphism group, so the statements below are finer than the description of an orbit under the whole group. The two statements that mention no orbit, that x is fixed by the q ^ d-th power map and that its minimal polynomial splits, ask only that x itself be integral over F. The first of those asks even less of E: it holds in any F-algebra that is a domain, commutative or not, since all it needs is that the minimal polynomial be irreducible.

Main results

• TauCeti.FiniteField.orbit_eq_rootSet_minpoly: the orbit is the root set of the minimal polynomial.
• TauCeti.FiniteField.map_minpoly_eq_prod_orbit: the minimal polynomial is the product of X - β over the orbit.
• TauCeti.FiniteField.natCard_orbit_eq_natDegree_minpoly: the orbit has as many elements as the degree of the minimal polynomial.
• TauCeti.FiniteField.mem_orbit_iff_minpoly_eq: the orbits are the fibres of x ↦ minpoly F x.
• TauCeti.FiniteField.mem_orbit_iff_exists_pow_card_pow: the orbit of x consists of the q ^ n-th powers of x.
• TauCeti.FiniteField.pow_card_pow_natDegree_minpoly: x is fixed by the q ^ d-th power map, d the degree of its minimal polynomial; stated for E merely a domain.
• TauCeti.FiniteField.splits_minpoly: the minimal polynomial splits in any field containing the element.

References

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

theorem TauCeti.FiniteField.pow_card_pow_natDegree_minpoly (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Ring E] [IsDomain E] [Algebra F E] {x : E} (hx : IsIntegral F x) : x ^ Fintype.card F ^ (minpoly F x).natDegree = x

An element integral over a finite field with q elements is fixed by the q ^ d-th power map, where d is the degree of its minimal polynomial.

E need only be a domain: irreducibility of the minimal polynomial is all that is used, and the argument never divides, so this also covers noncommutative F-algebras.

theorem TauCeti.FiniteField.finite_orbit (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (x : E) : (MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x).Finite

The Frobenius orbit of an element algebraic over a finite field is finite.

theorem TauCeti.FiniteField.map_minpoly_eq_prod_orbit (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (x : E) : Polynomial.map (algebraMap F E) (minpoly F x) = ∏ β ∈ ⋯.toFinset, (Polynomial.X - Polynomial.C β)

The minimal polynomial over a finite field is the product over the Frobenius orbit: for x algebraic over a finite field F, the minimal polynomial of x, read in E[X], is the product of X - β over the orbit of x.

@[simp]

theorem TauCeti.FiniteField.orbit_eq_rootSet_minpoly (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (x : E) : MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x = (minpoly F x).rootSet E

The Frobenius orbit of x is the root set of its minimal polynomial.

theorem TauCeti.FiniteField.natCard_orbit_eq_natDegree_minpoly (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (x : E) : Nat.card ↑(MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x) = (minpoly F x).natDegree

The Frobenius orbit of x has as many elements as the degree of its minimal polynomial.

theorem TauCeti.FiniteField.mem_orbit_iff_minpoly_eq (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] {x y : E} : y ∈ MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x ↔ minpoly F y = minpoly F x

Two elements lie in one Frobenius orbit exactly when they have the same minimal polynomial.

theorem TauCeti.FiniteField.pow_card_pow_mem_orbit (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (x : E) (n : ℕ) : x ^ Fintype.card F ^ n ∈ MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x

The q ^ n-th power of x lies in the Frobenius orbit of x, where q is the cardinality of the base field.

theorem TauCeti.FiniteField.mem_orbit_iff_exists_pow_card_pow (F : Type u_1) [Field F] [Fintype F] {E : Type u_2} [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] {x y : E} : y ∈ MulAction.orbit (↥(Subgroup.zpowers (FiniteField.frobeniusAlgEquivOfAlgebraic F E))) x ↔ ∃ (n : ℕ), x ^ Fintype.card F ^ n = y

The Frobenius orbit of x consists of the q ^ n-th powers of x, where q is the cardinality of the base field.

theorem TauCeti.FiniteField.splits_minpoly (F : Type u_3) [Field F] [Finite F] {E : Type u_4} [Field E] [Algebra F E] {x : E} (hx : IsIntegral F x) : (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

The minimal polynomial of an element integral over a finite field splits in any field containing that element: its roots are the iterated q-th powers of the element, which lie in the finite subfield generated by it. Equivalently, an algebraic extension of a finite field is normal.