Documentation

TauCeti.FieldTheory.FunctionField.RiemannRoch.Genus

Riemann's theorem and the genus #

For a divisor D of an algebraic function field F / k, the quantity deg D - ℓ(D) is bounded above by a constant depending only on F / k. The genus of F / k is the supremum

g := sup {deg D + 1 - ℓ(D) | D a divisor},

truncated to ℕ. Over an exact constant field the truncation changes nothing and g really is the maximum, attained at some divisor; over a non-exact one it is a junk value (see TauCeti.genus). Unwinding the supremum gives Riemann's theorem ℓ(D) ≥ deg D + 1 - g, valid over any constant field; over an exact constant field there is moreover equality as soon as deg D is large. This file is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.4.14 through Definition 1.5.1.

The boundedness argument is the only substantial one. Fix a transcendental x, let B = (x)_∞ be its pole divisor, so that deg B = [F : k(x)] = n by the product formula, and let C be an effective divisor dominating the pole divisors of a k(x)-basis u₁, …, uₙ of F. The n (l + 1) functions uᵢ xʲ with j ≤ l are k-linearly independent and lie in L(l B + C), so ℓ(l B + C) ≥ n (l + 1), whence deg (l B) - ℓ(l B) ≤ deg C - n uniformly in l. Every divisor is linearly equivalent to one below some l B, and both deg and ℓ are linear-equivalence invariants, so the same bound holds for every divisor.

Main definitions #

Main results #

Only the statements that mention the value of the maximum need the constant field to be exact; the bound of Proposition 1.4.14 and Riemann's inequality itself hold with no hypothesis on k beyond IsFunctionField k F.

Provenance #

The mathematics is Stichtenoth's and the Lean development is independent, as in TauCeti.FieldTheory.FunctionField.Place.Zeros. The separate vaca22/riemann-roch-function-fields project (Guanghao Li, Apache-2.0) carries a complete function-field Riemann–Roch development by the same Stichtenoth route; no code is copied or adapted from it here.

References #

The uniform bound on deg D - ℓ(D) #

source
theorem TauCeti.Divisor.bddAbove_range_degree_sub_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) :
BddAbove (Set.range fun (D : Divisor k F) => degree D - ↑D.dim)

Stichtenoth, Proposition 1.4.14: over all divisors of an algebraic function field the quantity deg D - ℓ(D) is bounded above. This finiteness is what makes the genus well-defined; no hypothesis on the constant field is needed.

The genus #

source
noncomputable def TauCeti.genus (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] :
ℕ

The genus of an algebraic function field (Stichtenoth, Definition 1.4.15): g = sup {deg D + 1 - ℓ(D)} after truncation to natural numbers. When IsFunctionField k F, TauCeti.Divisor.bddAbove_range_degree_sub_dim makes this supremum finite; without that hypothesis, an unbounded range gives the junk value 0.

The value is truncated to ℕ. Over an exact constant field this loses nothing, because D = 0 already gives deg 0 + 1 - ℓ(0) = 0; see TauCeti.exists_degree_add_one_sub_dim_eq_genus. Over a non-exact constant field the truncation is a junk value: for ℝ ⊆ ℂ(x) the true maximum is -1, because every ℝ-degree and every ℝ-dimension is twice its ℂ-counterpart.

Equations
Instances For
    source
    theorem TauCeti.genus_def {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
    genus k F = sSup (Set.range fun (D : Divisor k F) => (Divisor.degree D + 1 - ↑D.dim).toNat)

    The genus is the supremum of the nonnegative divisor degree-dimension defects.

    source
    theorem TauCeti.genus_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {c : ℕ} (h : ∀ (D : Divisor k F), Divisor.degree D + 1 - ↑D.dim ≤ ↑c) :
    genus k F ≤ c

    The least-upper-bound half of the universal property defining the genus.

    source
    theorem TauCeti.Divisor.degree_add_one_sub_dim_le_genus {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) :
    degree D + 1 - ↑D.dim ≤ ↑(genus k F)

    Riemann's theorem (Stichtenoth, Theorem 1.4.17), in the form that unwinds the definition of the genus: deg D + 1 - ℓ(D) ≤ g for every divisor D.

    source
    theorem TauCeti.Divisor.degree_add_one_sub_genus_le_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) :
    degree D + 1 - ↑(genus k F) ≤ ↑D.dim

    Riemann's theorem (Stichtenoth, Theorem 1.4.17): ℓ(D) ≥ deg D + 1 - g. No hypothesis on the constant field is needed for the inequality.

    source
    theorem TauCeti.exists_degree_add_one_sub_dim_eq_genus {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) :
    ∃ (D : Divisor k F), Divisor.degree D + 1 - ↑D.dim = ↑(genus k F)

    Stichtenoth, Corollary 1.4.16: over an exact constant field the maximum defining the genus is attained, so g ≥ 0 is the honest bound rather than an artefact of truncation.

    source
    theorem TauCeti.exists_forall_dim_eq_degree_add_one_sub_genus {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) :
    ∃ (c : ℤ), ∀ (D : Divisor k F), c ≤ Divisor.degree D → ↑D.dim = Divisor.degree D + 1 - ↑(genus k F)

    Stichtenoth, Theorem 1.4.17, second half: equality holds in Riemann's theorem for every divisor of sufficiently large degree.

    Functions with a single pole #

    source
    theorem TauCeti.Place.exists_ord_neg_and_forall_ne_ord_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (P : Place k F) :
    ∃ (z : F), P.ord z < 0 ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord z

    Every place is the only pole of some function: for a place P of an algebraic function field there is a function with a pole at P and no pole at any other place.

    Riemann's theorem makes ℓ(n·P) grow without bound, so some step of the ladder L(0) ≤ L(P) ≤ L(2P) ≤ … is strict, and a function in the larger space but not the smaller one has its only pole at P.

    The index of specialty #

    source
    noncomputable def TauCeti.Divisor.indexOfSpecialty {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
    ℤ

    The index of specialty of a divisor (Stichtenoth, Definition 1.5.1): i(D) = ℓ(D) - deg D - 1 + g, the defect in Riemann's theorem.

    Equations
    Instances For
      source
      theorem TauCeti.Divisor.indexOfSpecialty_def {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      D.indexOfSpecialty = ↑D.dim - degree D - 1 + ↑(genus k F)

      Unfolding formula for the index of specialty.

      source
      @[simp]
      theorem TauCeti.Divisor.indexOfSpecialty_sub_principal {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (z : Fˣ) (D : Divisor k F) :
      (D - principal hF z).indexOfSpecialty = D.indexOfSpecialty

      The index of specialty is unchanged by subtracting a principal divisor.

      source
      theorem TauCeti.Divisor.indexOfSpecialty_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) :
      0 ≤ D.indexOfSpecialty

      The index of specialty is nonnegative: this is exactly Riemann's theorem.

      source
      theorem TauCeti.exists_forall_indexOfSpecialty_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) :
      ∃ (c : ℤ), ∀ (D : Divisor k F), c ≤ Divisor.degree D → D.indexOfSpecialty = 0

      The index of specialty vanishes in large degree (Stichtenoth, Definition 1.5.1, following Theorem 1.4.17).