Admissible absolute values on polynomials

This file defines an admissible absolute value Polynomial.cardPowDegreeIsAdmissible which we use to show the class number of the ring of integers of a function field is finite.

Main results

• Polynomial.cardPowDegreeIsAdmissible shows cardPowDegree, mapping p : Polynomial 𝔽_q to q ^ degree p, is admissible

theorem Polynomial.exists_eq_polynomial {Fq : Type u_1} [Fintype Fq] [Semiring Fq] {d : ℕ} {m : ℕ} (hm : Fintype.card Fq ^ d ≤ m) (b : Polynomial Fq) (hb : b.natDegree ≤ d) (A : Fin m.succ → Polynomial Fq) (hA : ∀ (i : Fin m.succ), (A i).degree < b.degree) : ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀

If A is a family of enough low-degree polynomials over a finite semiring, there is a pair of equal elements in A.

theorem Polynomial.exists_approx_polynomial_aux {Fq : Type u_1} [Fintype Fq] [Ring Fq] {d : ℕ} {m : ℕ} (hm : Fintype.card Fq ^ d ≤ m) (b : Polynomial Fq) (A : Fin m.succ → Polynomial Fq) (hA : ∀ (i : Fin m.succ), (A i).degree < b.degree) : ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)

If A is a family of enough low-degree polynomials over a finite ring, there is a pair of elements in A (with different indices but not necessarily distinct), such that their difference has small degree.

theorem Polynomial.exists_approx_polynomial {Fq : Type u_1} [Fintype Fq] [Field Fq] {b : Polynomial Fq} (hb : b ≠ 0) {ε : ℝ} (hε : 0 < ε) (A : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ → Polynomial Fq) : ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ) (i₁ : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ), i₀ ≠ i₁ ∧ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε

If A is a family of enough low-degree polynomials over a finite field, there is a pair of elements in A (with different indices but not necessarily distinct), such that the difference of their remainders is close together.

theorem Polynomial.cardPowDegree_anti_archimedean {Fq : Type u_1} [Fintype Fq] [Field Fq] {x : Polynomial Fq} {y : Polynomial Fq} {z : Polynomial Fq} {a : ℤ} (hxy : Polynomial.cardPowDegree (x - y) < a) (hyz : Polynomial.cardPowDegree (y - z) < a) : Polynomial.cardPowDegree (x - z) < a

If x is close to y and y is close to z, then x and z are at least as close.

theorem Polynomial.exists_partition_polynomial_aux {Fq : Type u_1} [Fintype Fq] [Field Fq] (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Polynomial Fq} (hb : b ≠ 0) (A : Fin n → Polynomial Fq) : ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊)), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε

A slightly stronger version of exists_partition on which we perform induction on n: for all ε > 0, we can partition the remainders of any family of polynomials A into equivalence classes, where the equivalence(!) relation is "closer than ε".

theorem Polynomial.exists_partition_polynomial {Fq : Type u_1} [Fintype Fq] [Field Fq] (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Polynomial Fq} (hb : b ≠ 0) (A : Fin n → Polynomial Fq) : ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊)), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε

For all ε > 0, we can partition the remainders of any family of polynomials A into classes, where all remainders in a class are close together.

noncomputable def Polynomial.cardPowDegreeIsAdmissible {Fq : Type u_1} [Fintype Fq] [Field Fq] : Polynomial.cardPowDegree.IsAdmissible

fun p => Fintype.card Fq ^ degree p is an admissible absolute value. We set q ^ degree 0 = 0.

Equations

• Polynomial.cardPowDegreeIsAdmissible = { toIsEuclidean := ⋯, card := fun (ε : ℝ) => Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊, exists_partition' := ⋯ }