mathlib documentation

number_theory.class_number.admissible_card_pow_degree

Admissible absolute values on polynomials #

This file defines an admissible absolute value polynomial.card_pow_degree_is_admissible 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} [field Fq] [fintype Fq] {d m : ā„•} (hm : fintype.card Fq ^ d ā‰¤ m) (b : polynomial Fq) (hb : b.nat_degree ā‰¤ d) (A : fin m.succ ā†’ polynomial Fq) (hA : āˆ€ (i : fin m.succ), (A i).degree < b.degree) :
āˆƒ (iā‚€ iā‚ : fin m.succ), iā‚€ ā‰  iā‚ āˆ§ A iā‚ = A iā‚€

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

theorem polynomial.exists_approx_polynomial_aux {Fq : Type u_1} [field Fq] [fintype 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ā‚€ iā‚ : fin m.succ), iā‚€ ā‰  iā‚ āˆ§ (A iā‚ - A iā‚€).degree < ā†‘(b.nat_degree - d)

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 their difference has small degree.

theorem polynomial.exists_approx_polynomial {Fq : Type u_1} [field Fq] [fintype Fq] {b : polynomial Fq} (hb : b ā‰  0) {Īµ : ā„} (hĪµ : 0 < Īµ) (A : fin (fintype.card Fq ^ āŒˆ-real.log Īµ / real.log ā†‘(fintype.card Fq)āŒ‰ā‚Š).succ ā†’ polynomial Fq) :

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.

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} [field Fq] [fintype 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.card_pow_degree (A iā‚ % b - A iā‚€ % b)) < ā‡‘polynomial.card_pow_degree 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} [field Fq] [fintype 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.card_pow_degree (A iā‚ % b - A iā‚€ % b)) < ā‡‘polynomial.card_pow_degree 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.

Ī» p, fintype.card Fq ^ degree p is an admissible absolute value. We set q ^ degree 0 = 0.

Equations