Frobenius polynomial identities

This file establishes fundamental identities involving the Frobenius endomorphism for polynomials over finite fields. The main results include factorization identities, Frobenius polynomial identities, and divisibility conditions for irreducible polynomials.

Main Definitions and Theorems

1. Field Vanishing Polynomial Equality:

   • prod_X_sub_C_eq_X_pow_card_sub_X: The identity ∏_{c ∈ Fq} (X - c) = X^q - X in Fq[X]
   • prod_X_sub_C_eq_X_pow_card_sub_X_in_L: Lifted version for field extensions L[X]
   • prod_poly_sub_C_eq_poly_pow_card_sub_poly_in_L: General version ∏_{c ∈ Fq} (p - c) = p^q - p for any polynomial p in L[X]

2. Frobenius Polynomial Identity:

   • frobenius_identity_in_ground_field: (f + g)^q = f^q + g^q in Fq[X] (Freshman's Dream)
   • frobenius_identity_in_algebra: Lifted version for Fq-algebras L[X]
   • aeval_pow_card_eq_aeval_pow_card: (aeval x f)^q = aeval (x^q) f for polynomial evaluation
   • aeval_pow_card_pow_eq_aeval_pow_card_pow: Iterated version (aeval x f)^(q^n) = aeval (x^(q^n)) f

3. Frobenius Polynomial Divisibility:

   • X_pow_sub_one_dvd_X_pow_sub_one_of_dvd: If k ∣ n, then X^k - 1 ∣ X^n - 1
   • X_pow_card_pow_dvd_X_pow_card_pow_of_dvd: If d ∣ n, then X^(q^d) - X ∣ X^(q^n) - X
   • irreducible_dvd_X_pow_card_pow_sub_X: An irreducible polynomial p of degree d divides X^(q^d) - X
   • degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X: If irreducible p divides X^(q^n) - X, then deg(p) ∣ n
   • irreducible_dvd_X_pow_sub_X_iff_natDegree_dvd: Fundamental theorem: p ∣ X^(c^n) - X ↔ deg(p) ∣ n, with the field size as a numeral c together with Fintype.card R = c
   • irreducible_dvd_X_pow_add_X_iff_natDegree_dvd: its characteristic-two form, stated with + X as the binary fields write it

TODOs

• potentially generalize the Frobenius theorems to generic algebras?

theorem instExpCharOfAlgebra {Fq : Type u_1} [Field Fq] {K : Type u_2} [Field K] [Algebra Fq K] {h_ringChar_Fq_pos : ringChar Fq ≠ 0} : ExpChar K (ringChar Fq)

An algebra over a field of positive characteristic inherits its exponential characteristic: if ringChar Fq ≠ 0, then ExpChar K (ringChar Fq) for any Fq-algebra K that is a field. Named as an instance but kept a theorem deliberately — it is introduced locally where a Frobenius argument needs it, rather than added to the instance graph for every algebra.

theorem Polynomial.prod_X_sub_C_eq_X_pow_card_sub_X {Fq : Type u_1} [Field Fq] [Fintype Fq] : ∏ c : Fq, (X - C c) = X ^ Fintype.card Fq - X

The polynomial X^q - X factors into the product of (X - c) ∀ c ∈ Fq, i.e. ∏_{c ∈ Fq} (X - c) = X^q - X.

theorem Polynomial.prod_X_sub_C_eq_X_pow_card_sub_X_in_L {Fq : Type u_1} [Field Fq] [Fintype Fq] {L : Type u_2} [CommRing L] [Algebra Fq L] : ∏ c : Fq, (X - C ((algebraMap Fq L) c)) = X ^ Fintype.card Fq - X

The identity ∏_{c ∈ Fq} (X - c) = X^q - X also holds in the polynomial ring L[X], where L is any field extension of Fq.

theorem Polynomial.prod_poly_sub_C_eq_poly_pow_card_sub_poly_in_L {Fq : Type u_1} [Field Fq] [Fintype Fq] {L : Type u_2} [CommRing L] [Algebra Fq L] (p : Polynomial L) : ∏ c : Fq, (p - C ((algebraMap Fq L) c)) = p ^ Fintype.card Fq - p

The identity ∏_{c ∈ Fq} (X - c) = X^q - X also holds in the polynomial ring L[X], where L is any field extension of Fq.

theorem Polynomial.frobenius_identity_in_ground_field {Fq : Type u_1} [Field Fq] [Fintype Fq] [Fact (Nat.Prime (ringChar Fq))] (f g : Polynomial Fq) : (f + g) ^ Fintype.card Fq = f ^ Fintype.card Fq + g ^ Fintype.card Fq

The Frobenius identity for polynomials in Fq[X]. The q-th power of a sum of polynomials is the sum of their q-th powers.

theorem Polynomial.frobenius_identity_in_algebra {Fq : Type u_1} [Field Fq] [Fintype Fq] {L : Type u_2} [CommRing L] [Algebra Fq L] [Nontrivial L] [Fact (Nat.Prime (ringChar Fq))] (f g : Polynomial L) : (f + g) ^ Fintype.card Fq = f ^ Fintype.card Fq + g ^ Fintype.card Fq

The lifted Frobenius identity for polynomials in L[X], where L is an Fq-algebra. The exponent q is the cardinality of the base field Fq.

theorem Polynomial.linear_map_of_comp_to_linear_map_of_eval {Fq : Type u_1} [Field Fq] {L : Type u_2} [CommRing L] [Algebra Fq L] (f : Polynomial L) (h_f_linear : IsLinearMap Fq fun (inner_p : Polynomial L) => f.comp inner_p) : IsLinearMap Fq fun (x : L) => eval x f

Restricting a linear map on polynomial composition to a linear map on polynomial evaluation.

theorem Polynomial.aeval_pow_card_eq_aeval_pow_card {Fq : Type u_3} {K : Type u_4} [Field Fq] [Fintype Fq] [CommRing K] [Algebra Fq K] [Fact (Nat.Prime (ringChar Fq))] [ExpChar K (ringChar Fq)] (f : Polynomial Fq) (x : K) : (aeval x) f ^ Fintype.card Fq = (aeval (x ^ Fintype.card Fq)) f

Frobenius endomorphism interaction with polynomial evaluation. (aeval x f)^|Fq| = aeval (x^|Fq|) f

theorem Polynomial.aeval_pow_card_pow_eq_aeval_pow_card_pow {Fq : Type u_3} {K : Type u_4} [Field Fq] [Fintype Fq] [CommRing K] [Algebra Fq K] [Fact (Nat.Prime (ringChar Fq))] [ExpChar K (ringChar Fq)] (f : Polynomial Fq) (x : K) (n : ℕ) : (aeval x) f ^ Fintype.card Fq ^ n = (aeval (x ^ Fintype.card Fq ^ n)) f

Iterated Frobenius endomorphism interaction with polynomial evaluation. (aeval x f)^(|Fq|^n) = aeval (x^|Fq|^n) f

theorem Polynomial.X_pow_sub_one_dvd_X_pow_sub_one_of_dvd {Fq : Type u_1} [Field Fq] (k n : ℕ) (h_dvd : k ∣ n) : X ^ k - 1 ∣ X ^ n - 1

Lemma 1: Polynomial Divisibility of Powers If k divides n, then X^k - 1 divides X^n - 1. This is the polynomial version of a | b => x^a - 1 | x^b - 1.

theorem Polynomial.X_pow_card_pow_dvd_X_pow_card_pow_of_dvd {Fq : Type u_1} [Field Fq] [Fintype Fq] (d n : ℕ) (h_dvd : d ∣ n) : have q := Fintype.card Fq; X ^ q ^ d - X ∣ X ^ q ^ n - X

Lemma 2: Frobenius Divisibility Transitivity If d divides n, then X^(q^d) - X divides X^(q^n) - X. This allows us to say: "If a poly divides the small Frobenius, it divides the big one."

theorem Polynomial.irreducible_dvd_X_pow_card_pow_sub_X {Fq : Type u_1} [Field Fq] [Fintype Fq] (p : Polynomial Fq) (hp_irr : Irreducible p) : have q := Fintype.card Fq; have d := p.natDegree; p ∣ X ^ q ^ d - X

Lemma 3: Irreducible Divides Own Frobenius (The Base Case) An irreducible polynomial p of degree d divides X^(q^d) - X. Proof:

1. Consider the extension K = Fq[x]/(p).
2. The group of units K* has order q^d - 1.
3. So every element α satisfies α^(q^d - 1) = 1 (if α ≠ 0).
4. Thus α^(q^d) = α for all α.
5. X^(q^d) - X has root p as a root.
6. Since p is the minimal polynomial of its root, p divides the target.

theorem Polynomial.degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X {Fq : Type u_1} [Field Fq] [Fintype Fq] [Fact (Nat.Prime (ringChar Fq))] (p : Polynomial Fq) (hp_irr : Irreducible p) (n : ℕ) (h_dvd : p ∣ X ^ Fintype.card Fq ^ n - X) : p.natDegree ∣ n

Theorem: The Rabin Condition (One Direction) If p is irreducible, and p divides X^(q^n) - X, then deg(p) divides n.

theorem Polynomial.irreducible_dvd_X_pow_sub_X_iff_natDegree_dvd {R : Type u_2} [Field R] [Fact (Nat.Prime (ringChar R))] [Fintype R] {c : ℕ} (hcard : Fintype.card R = c) (n : ℕ) (q : Polynomial R) (hq_irr : Irreducible q) : q ∣ X ^ c ^ n - X ↔ q.natDegree ∣ n

Fundamental Theorem of Irreducible Polynomials over Finite Fields: For an irreducible polynomial q over a finite field R with c elements: q ∣ X^(c^n) - X ↔ deg q ∣ n.

The field size enters as a numeral c together with hcard : Fintype.card R = c, rather than being read off as Fintype.card R. A concrete field then states the divisibility at its own field-size literal and supplies hcard as ZMod.card _; a caller with no numeral in hand passes rfl and recovers the Fintype.card R statement verbatim. See the section comment in CompPoly/Data/Polynomial/Rabin.lean for why every criterion in the library is shaped this way.

theorem Polynomial.irreducible_dvd_X_pow_add_X_iff_natDegree_dvd {R : Type u_2} [Field R] [Fact (Nat.Prime (ringChar R))] [Fintype R] [CharP R 2] {c : ℕ} (hcard : Fintype.card R = c) (n : ℕ) (q : Polynomial R) (hq_irr : Irreducible q) : q ∣ X ^ c ^ n + X ↔ q.natDegree ∣ n

The characteristic-two form of irreducible_dvd_X_pow_sub_X_iff_natDegree_dvd, stated with + X as a binary field writes it: q ∣ X^(c^n) + X ↔ deg q ∣ n.

Over GF(2) the two spellings are the same polynomial, but only one of them is syntactically what a caller has. Absorbing CharTwo.sub_eq_add here — once, at a statement generic in c and n — means the concrete caller applies this as a term instead of rewriting a hypothesis whose type carries a large exponent such as X ^ 2 ^ 128.