Over a finite constant field there are finitely many places of bounded degree

Let F / k be an algebraic function field whose constant field k is finite. Then for every bound r only finitely many places of F / k have degree at most r.

On the rational function field this is a count of polynomials: by the classification of the places of k(x) they are the place at infinity together with the monic irreducible polynomials, and the degree of the place of q is deg q, so a bound on the degree of a place is a bound on the degree of a polynomial over a finite field. In general one chooses a transcendental x, which makes F a finite extension of k(x); a place of F is at least as large as the place of k(x) below it (TauCeti.Place.degree_restrict_le), and each place of k(x) has only finitely many extensions (TauCeti.Place.finite_setOf_restrict_eq), so the bounded-degree places of F sit in finitely many finite fibres.

This is the counting input of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Lemma 5.1.1, on the way to the finiteness of the degree-zero divisor class group; it is not the lemma itself, which counts effective divisors.

Main results

• TauCeti.Place.finite_setOf_degree_le_ratFunc: the bounded-degree places of k(x).
• TauCeti.Place.finite_setOf_degree_le: the bounded-degree places of an arbitrary algebraic function field over a finite constant field.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section V.1.

theorem TauCeti.Place.finite_setOf_degree_le_ratFunc (k : Type u) [Field k] [Finite k] (r : ℕ) : {P : Place k (RatFunc k) | P.degree ≤ r}.Finite

The places of the rational function field of bounded degree are finite in number when the constant field is finite: under the classification of the places of k(x) they are the place at infinity and the monic irreducible polynomials of degree at most r.

theorem TauCeti.Place.finite_setOf_degree_le {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) [Finite k] (r : ℕ) : {P : Place k F | P.degree ≤ r}.Finite

Over a finite constant field an algebraic function field has only finitely many places of degree at most r (Stichtenoth, the counting input of Lemma 5.1.1).