The class number of a function field with a finite constant field #

Let F / k be an algebraic function field. Riemann's theorem produces, from a divisor B and an n with n · deg B ≥ g, an effective representative of degree n · deg B in the class of D + n·B for every degree-zero divisor D (TauCeti.Divisor.exists_isEffective_linearlyEquivalent_add_nsmul): so the class of a degree-zero divisor is the class of A - n·B with A effective of one fixed degree. Taking B to be a place makes deg B positive, so such an n exists.

When the constant field k is finite there are only finitely many effective divisors of a given degree — the places of bounded degree are finite in number (TauCeti.Place.finite_setOf_degree_le) and an effective divisor of degree at most n is supported on places of degree at most n with coefficients in [0, n]. Combining the two gives the finiteness of the degree-zero divisor class group Cl⁰(F) = ker (deg : Cl(F) → ℤ), whose cardinality is the class number h_F.

This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Lemma 5.1.1 and Proposition 5.1.3, the zeta-free half of his Section V.1: no zeta function, no functional equation, and no exactness hypothesis on the constant field.

⚠ TauCeti.Divisor.classNumber is not Mathlib's FunctionField.classNumber (Mathlib/NumberTheory/ClassNumber/FunctionField.lean), which is #ClassGroup (FunctionField.ringOfIntegers Fq F): the class number of the finite chart of one chosen model, defined only for a chosen embedding of Fq(X) and under separability of F / Fq(X). The two differ by the places at infinity of that model: ClassGroup R_x is a quotient of the full divisor class group Cl(F), with kernel generated by the classes of the places over ∞, and Cl⁰(F) already surjects onto it as soon as one of those places is rational. The comparison is the affine class-group bridge of TauCeti.FieldTheory.FunctionField.RiemannRoch.AffineClassNumber, which transfers the finiteness proved here to the ideal class group of an arbitrary affine model.

Main definitions #

TauCeti.Divisor.classNumber: h_F = #Cl⁰(F), the cardinality of the degree-zero divisor class group.

Main results #

TauCeti.Divisor.finite_setOf_isEffective_degree_le: over a finite constant field there are finitely many effective divisors of bounded degree (Lemma 5.1.1).
TauCeti.Divisor.exists_isEffective_linearlyEquivalent_add_nsmul: the effective representative of fixed degree in a degree-zero class, from Riemann's theorem.
TauCeti.Divisor.finite_ker_degreeClass: Cl⁰(F) is finite (Proposition 5.1.3), with TauCeti.Divisor.classNumber_pos recording that the class number is then positive.
TauCeti.Divisor.finite_preimage_degreeClass: whenever Cl⁰(F) is finite, only finitely many divisor classes have degree in a given finite set of integers.

References #

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

Counting effective divisors #

source

theorem TauCeti.Divisor.finite_setOf_isEffective_degree_le {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) [Finite k] (n : ℕ) :

{D : Divisor k F | AlgebraicGeometry.WeilDivisor.IsEffective D ∧ degree D ≤ ↑n}.Finite

Over a finite constant field there are only finitely many effective divisors of degree at most n (Stichtenoth, Lemma 5.1.1): such a divisor is supported on the finitely many places of degree at most n, and its coefficients lie in [0, n].

The effective representative of a degree-zero class #

source

theorem TauCeti.Divisor.exists_isEffective_linearlyEquivalent_add_nsmul {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {B D : Divisor k F} {n : ℕ} (hn : ↑(genus k F) ≤ ↑n * degree B) (hD : degree D = 0) :

∃ (A : Divisor k F), AlgebraicGeometry.WeilDivisor.IsEffective A ∧ degree A = ↑n * degree B ∧ (Place.orderSystem hF).LinearlyEquivalent A (D + n • B)

Every degree-zero divisor class contains a divisor of the form A - n·B, with A effective of degree n · deg B — for any divisor B and any n with n · deg B at least the genus (Stichtenoth, the representative step in the proof of Proposition 5.1.3). Riemann's theorem makes L(D + n·B) nonzero, and a nonzero function in it moves D + n·B to an effective divisor of the same degree.

The class number #

source

theorem TauCeti.Divisor.finite_ker_degreeClass {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) [Finite k] :

Finite ↥(degreeClass hF).ker

The degree-zero divisor class group Cl⁰(F) of an algebraic function field with a finite constant field is finite (Stichtenoth, Proposition 5.1.3): every degree-zero class is the class of A - n·B for a fixed divisor B and an effective A of one fixed degree, and there are only finitely many such A.

source

theorem TauCeti.Divisor.finite_preimage_degreeClass_singleton {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hker : Finite ↥(degreeClass hF).ker) (n : ℤ) :

(⇑(degreeClass hF) ⁻¹' {n}).Finite

A fibre of the degree map on divisor classes is empty or a coset of Cl⁰(F), so it is finite as soon as Cl⁰(F) is — over a finite constant field always, by TauCeti.Divisor.finite_ker_degreeClass.

source

theorem TauCeti.Divisor.finite_preimage_degreeClass {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hker : Finite ↥(degreeClass hF).ker) {s : Set ℤ} (hs : s.Finite) :

(⇑(degreeClass hF) ⁻¹' s).Finite

Only finitely many divisor classes have degree in a given finite set of integers, as soon as Cl⁰(F) is finite: each degree fibre is empty or a coset of it.

source

noncomputable def TauCeti.Divisor.classNumber {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) :

ℕ

The class number h_F = #Cl⁰(F) of an algebraic function field: the cardinality of its degree-zero divisor class group. Over a finite constant field this is a positive integer (TauCeti.Divisor.classNumber_pos); in general Nat.card returns the junk value 0 for an infinite group.

Equations