The polynomial coprimality theorem over finite fields

Over a finite field with q elements, the number of m-tuples of monic polynomials of degrees n₁, …, n_m ≥ 1 with no non-unit common divisor is q^N − q^(N − m + 1), N = Σ nᵢ; with equal degrees, the proportion of tuples with a non-trivial common factor is 1/q^(m−1) (Theorem of the Day). Proof: every tuple factors uniquely as d · (g₁, …, g_m) with d the monic gcd and the gᵢ coprime, so q^N = Σ_k q^k · C(n − k), and strong induction on min nᵢ solves for C.

Main results

• PolynomialCoprimality.card_monic_natDegree: there are q^n monic polynomials of degree n
• PolynomialCoprimality.card_coprime_tuples: coprime m-tuples of monic polynomials of degrees nᵢ ≥ 1: q^N − q^(N−m+1)
• PolynomialCoprimality.card_not_coprime_equal_degree: equal degrees: q^(mn − m + 1) tuples share a non-trivial factor (proportion 1/q^(m−1))

References

• R. Whitty, Theorem of the Day, «The Polynomial Coprimality Theorem» (CombinatorialTheory/Coprimality).
• S. Corteel, C. D. Savage, H. S. Wilf, D. Zeilberger, A pentagonal number sieve, J. Combin. Theory Ser. A 82 (1998).
• A. T. Benjamin, C. D. Bennett, The probability of relatively prime polynomials, Math. Mag. 80 (2007).

@[reducible, inline]

abbrev PolynomialCoprimality.MonicDeg (K : Type u_1) [Field K] (n : ℕ) : Type u_1

Monic polynomials of natural degree n.

Equations

• PolynomialCoprimality.MonicDeg K n = { f : Polynomial K // f.Monic ∧ f.natDegree = n }

noncomputable def PolynomialCoprimality.monicEquiv (K : Type u_1) [Field K] (n : ℕ) : MonicDeg K n ≃ ↥(Polynomial.degreeLT K n)

Equations

• One or more equations did not get rendered due to their size.

theorem PolynomialCoprimality.card_monic_natDegree (K : Type u_1) [Field K] [Fintype K] (n : ℕ) : Nat.card { f : Polynomial K // f.Monic ∧ f.natDegree = n } = Fintype.card K ^ n

instance PolynomialCoprimality.finMonicDeg (K : Type u_1) [Field K] [Finite K] (n : ℕ) : Finite (MonicDeg K n)

@[reducible, inline]

abbrev PolynomialCoprimality.TupDeg (K : Type u_1) [Field K] (m : ℕ) (n : Fin m → ℕ) : Type u_1

Tuples of monic polynomials with prescribed degrees.

Equations

• PolynomialCoprimality.TupDeg K m n = { t : Fin m → Polynomial K // ∀ (i : Fin m), (t i).Monic ∧ (t i).natDegree = n i }

@[reducible, inline]

abbrev PolynomialCoprimality.CopDeg (K : Type u_1) [Field K] (m : ℕ) (n : Fin m → ℕ) : Type u_1

Such tuples with no non-unit common divisor.

Equations

• PolynomialCoprimality.CopDeg K m n = { t : Fin m → Polynomial K // (∀ (i : Fin m), (t i).Monic ∧ (t i).natDegree = n i) ∧ ∀ (d : Polynomial K), (∀ (i : Fin m), d ∣ t i) → IsUnit d }

noncomputable def PolynomialCoprimality.tupEquiv {K : Type u_1} [Field K] {m : ℕ} (n : Fin m → ℕ) : TupDeg K m n ≃ ((i : Fin m) → MonicDeg K (n i))

Equations

• PolynomialCoprimality.tupEquiv n = Equiv.subtypePiEquivPi

instance PolynomialCoprimality.finTup {K : Type u_1} [Field K] [Finite K] {m : ℕ} (n : Fin m → ℕ) : Finite (TupDeg K m n)

instance PolynomialCoprimality.finCop {K : Type u_1} [Field K] [Finite K] {m : ℕ} (n : Fin m → ℕ) : Finite (CopDeg K m n)

theorem PolynomialCoprimality.card_tup {K : Type u_1} [Field K] [Fintype K] {m : ℕ} (n : Fin m → ℕ) : Nat.card (TupDeg K m n) = Fintype.card K ^ ∑ i : Fin m, n i

@[instance_reducible]

noncomputable def PolynomialCoprimality.instNGCD {K : Type u_1} [Field K] [DecidableEq K] : NormalizedGCDMonoid (Polynomial K)

A normalized gcd on K[X], local to this file (Mathlib has no global instance for a bare field).

Equations

• PolynomialCoprimality.instNGCD = UniqueFactorizationMonoid.toNormalizedGCDMonoid (Polynomial K)

theorem PolynomialCoprimality.gcd_mul_cop {K : Type u_1} [Field K] [DecidableEq K] {m : ℕ} (d : Polynomial K) (hd : d.Monic) (g : Fin m → Polynomial K) (hg : ∀ (c : Polynomial K), (∀ (i : Fin m), c ∣ g i) → IsUnit c) : (Finset.univ.gcd fun (i : Fin m) => d * g i) = d

theorem PolynomialCoprimality.exists_decomp {K : Type u_1} [Field K] [DecidableEq K] {m : ℕ} (hm : 0 < m) (t : Fin m → Polynomial K) (ht : ∀ (i : Fin m), (t i).Monic) : ∃ (d : Polynomial K) (s : Fin m → Polynomial K), d.Monic ∧ (∀ (i : Fin m), (s i).Monic) ∧ (∀ (i : Fin m), t i = d * s i) ∧ ∀ (c : Polynomial K), (∀ (i : Fin m), c ∣ s i) → IsUnit c

@[reducible, inline]

abbrev PolynomialCoprimality.Dec (K : Type u_2) [Field K] (m : ℕ) (n : Fin m → ℕ) (L : ℕ) : Type u_2

Decomposition data: a monic d of degree k ≤ L and a coprime tuple of degrees nᵢ - k.

Equations

• PolynomialCoprimality.Dec K m n L = ((k : Fin (L + 1)) × PolynomialCoprimality.MonicDeg K ↑k × PolynomialCoprimality.CopDeg K m fun (i : Fin m) => n i - ↑k)

theorem PolynomialCoprimality.decMap_prop {K : Type u_1} [Field K] {m : ℕ} (n : Fin m → ℕ) (L : ℕ) (hL : ∀ (i : Fin m), L ≤ n i) (x : Dec K m n L) (i : Fin m) : (↑x.snd.1 * ↑x.snd.2 i).Monic ∧ (↑x.snd.1 * ↑x.snd.2 i).natDegree = n i

noncomputable def PolynomialCoprimality.decMap {K : Type u_1} [Field K] {m : ℕ} (n : Fin m → ℕ) (L : ℕ) (hL : ∀ (i : Fin m), L ≤ n i) : Dec K m n L → TupDeg K m n

The multiplication map (d, g) ↦ d • g.

Equations

• PolynomialCoprimality.decMap n L hL x = ⟨fun (i : Fin m) => ↑x.snd.1 * ↑x.snd.2 i, ⋯⟩

theorem PolynomialCoprimality.decMap_bijective {K : Type u_1} [Field K] [DecidableEq K] {m : ℕ} (hm : 0 < m) (n : Fin m → ℕ) (L : ℕ) (hL : ∀ (i : Fin m), L ≤ n i) (hL' : ∃ (i : Fin m), n i = L) : Function.Bijective (decMap n L hL)

theorem PolynomialCoprimality.card_decomp {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m : ℕ} (hm : 0 < m) (n : Fin m → ℕ) (L : ℕ) (hL : ∀ (i : Fin m), L ≤ n i) (hL' : ∃ (i : Fin m), n i = L) : Fintype.card K ^ ∑ i : Fin m, n i = ∑ k ∈ Finset.range (L + 1), Fintype.card K ^ k * Nat.card (CopDeg K m fun (i : Fin m) => n i - k)

q ^ N = ∑_{k ≤ L} q ^ k * C(n - k).

theorem PolynomialCoprimality.telescope (f a : ℕ → ℕ) (L : ℕ) (hL : 1 ≤ L) (h1 : ∀ (j : ℕ), 1 ≤ j → j < L → f j + a (j + 1) = a j) (h2 : f L = a L) : ∑ k ∈ Finset.range L, f (k + 1) = a 1

Pure telescoping step.

theorem PolynomialCoprimality.count_ind {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {m : ℕ} (hm : 0 < m) (N : ℕ) (n : Fin m → ℕ) : ∑ i : Fin m, n i = N → ((∃ (i : Fin m), n i = 0) → Nat.card (CopDeg K m n) = Fintype.card K ^ N) ∧ ((∀ (i : Fin m), 1 ≤ n i) → Nat.card (CopDeg K m n) + Fintype.card K ^ (N - m + 1) = Fintype.card K ^ N)

theorem PolynomialCoprimality.card_coprime_tuples (K : Type u_2) [Field K] [Fintype K] (m : ℕ) (hm : 1 ≤ m) (n : Fin m → ℕ) (hn : ∀ (i : Fin m), 1 ≤ n i) : Nat.card { t : Fin m → Polynomial K // (∀ (i : Fin m), (t i).Monic ∧ (t i).natDegree = n i) ∧ ∀ (d : Polynomial K), (∀ (i : Fin m), d ∣ t i) → IsUnit d } = Fintype.card K ^ ∑ i : Fin m, n i - Fintype.card K ^ (∑ i : Fin m, n i - m + 1)

The polynomial coprimality theorem (general degrees).

theorem PolynomialCoprimality.card_not_coprime_equal_degree (K : Type u_2) [Field K] [Fintype K] (m : ℕ) (hm : 1 ≤ m) (n : ℕ) (hn : 1 ≤ n) : Nat.card { t : Fin m → Polynomial K // (∀ (i : Fin m), (t i).Monic ∧ (t i).natDegree = n) ∧ ∃ (d : Polynomial K), (∀ (i : Fin m), d ∣ t i) ∧ ¬IsUnit d } = Fintype.card K ^ (m * n - m + 1)

Equal degrees: q ^ (m * n - m + 1) tuples of monic polynomials of degree n share a non-trivial common factor.