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^(q^n) - X ↔ deg(p) ∣ n

TODOs

• potentially generalize the Frobenius theorems to generic algebras?

instance 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)

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] (n : ℕ) (q : Polynomial R) (hq_irr : Irreducible q) : q ∣ X ^ Fintype.card R ^ n - X ↔ q.natDegree ∣ n

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