Finiteness of bounded-degree places

For a finite field K, there are only finitely many finite places of K(X) of bounded degree: a place is represented by its normalized prime polynomial, and a polynomial of bounded degree is determined by finitely many coefficients. A finite place in a finite function-field extension lies over one of these base places, with only finitely many primes in each fiber.

This file proves the corresponding finiteness statements for base finite places, finite places in an extension, and the exhaustive finite-plus-infinity place type. These are the local-finiteness inputs needed to define effective divisor counts and Euler products without assuming zeta rationality.

theorem BGS.HasseWeil.ratFuncFinitePlace_degree_le_finite (K : Type u_1) [Field K] [Finite K] [DecidableEq K] (n : ℕ) : Finite { p : IsDedekindDomain.HeightOneSpectrum (Polynomial K) // CorvajaZannier.ratFuncFinitePlaceDegree p ≤ n }

Finite fields have only finitely many finite rational-function places of degree at most n.

theorem BGS.HasseWeil.finiteExtensionFinitePlace_degree_le_finite (K : Type u_1) (L : Type u_2) [Field K] [Finite K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : Finite { q : CorvajaZannier.FiniteExtensionFinitePlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q) ≤ n }

A finite extension of K(X) has only finitely many finite places of degree at most n.

theorem BGS.HasseWeil.finiteExtensionPlace_degree_le_finite (K : Type u_1) (L : Type u_2) [Field K] [Finite K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : Finite { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ n }

A finite extension of K(X) has only finitely many exhaustive places of degree at most n. The finite branch is the preceding theorem; the branch above the unique base infinity place is finite without a degree restriction.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.finiteExtensionPlaceDegreeLEFintype (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : Fintype { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ n }

A concrete finite type of exhaustive places of degree at most n.

Equations

• BGS.HasseWeil.finiteExtensionPlaceDegreeLEFintype K L n = Fintype.ofFinite { P : BGS.CorvajaZannier.FiniteExtensionPlace K L // BGS.CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ n }