Documentation

Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

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 #

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 : Polynomial.natDegree b ā‰¤ d) (A : Fin (Nat.succ m) ā†’ Polynomial Fq) (hA : āˆ€ (i : Fin (Nat.succ m)), Polynomial.degree (A i) < Polynomial.degree b) :
āˆƒ iā‚€ iā‚, 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 (Nat.succ m) ā†’ Polynomial Fq) (hA : āˆ€ (i : Fin (Nat.succ m)), Polynomial.degree (A i) < Polynomial.degree b) :
āˆƒ iā‚€ iā‚, iā‚€ ā‰  iā‚ āˆ§ Polynomial.degree (A iā‚ - A iā‚€) < ā†‘(Polynomial.natDegree b - 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 (Nat.succ (Fintype.card Fq ^ āŒˆ-Real.log Īµ / Real.log ā†‘(Fintype.card Fq)āŒ‰ā‚Š)) ā†’ Polynomial Fq) :
āˆƒ iā‚€ iā‚, 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, āˆ€ (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, āˆ€ (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] :
AbsoluteValue.IsAdmissible Polynomial.cardPowDegree

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

Instances For