Documentation

TauCeti.FieldTheory.FunctionField.Place.Zeros

The zeros of a function of an algebraic function field are few #

A nonzero element x of a function field F / k has, at every place P, an order ord_P x, and the places where that order is nonzero are the zeros and the poles of x. This file proves that a function has only finitely many of each, and quantifies the statement: the zeros of x, counted with multiplicity ord_P x and weighted by the residue degree deg P, number at most [F : k(x)]. This is Stichtenoth, Algebraic Function Fields and Codes, 2nd ed. (GTM 254), Proposition 1.3.3 and Corollary 1.3.4.

The finiteness statement is what makes the divisor theory possible at all: without it the principal divisor div x = ∑_P ord_P x · P of a function is not a finitely supported formal sum and does not lie in Place k F →₀ ℤ.

Main results #

Implementation notes #

Proposition 1.3.3 is proved exactly as in Stichtenoth, by exhibiting ∑ P ∈ S, ord_P x · deg P elements of F that are linearly independent over k(x). For each place P of S choose

the family is then u_{P,j} · t_P ^ a for 0 ≤ a < ord_P x. Both choices are weak approximation, and both are what make the places of S interact: a relation among the family is grouped by place, and the group belonging to one place P₀ is seen to have order exactly a₀ < ord_{P₀} x at P₀, where a₀ is the least exponent surviving the clearing of a common factor x, while every other group has order at least ord_{P₀} x there. The two are incompatible, so no relation exists.

As in TauCeti.FieldTheory.FunctionField.Place.Degree, the relation is taken over the polynomial subalgebra k[x] = Algebra.adjoin k {x} and upgraded by LinearIndependent.iff_fractionRing; the common power of x is cleared by TauCeti.Polynomial.exists_common_X_pow_factor. Orders are compared in the multiplicative form P.valuation, which is free of the junk value ord_P 0 = 0, so no term of a sum has to be proved nonzero.

Provenance #

The mathematics is Stichtenoth's and the Lean development is independent. 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. In particular, this file uses Tau Ceti's normalized-ℤᵐ⁰-valuation TauCeti.Place API.

References #

The order of a two-parameter polynomial combination at a single place #

The two lemmas of this section are the local computations of Stichtenoth's Proposition 1.3.3: the value of P on ∑ a, ∑ j, p_{a,j}(x) · u_j · t ^ a when P is the place the family belongs to, and when it is one of the others.

Proposition 1.3.3 #

source
theorem TauCeti.Place.sum_ord_mul_degree_le_finrank {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} [FiniteDimensional (↥k⟮x⟯) F] {S : Finset (Place k F)} (hS : ∀ P ∈ S, 0 < P.ord x) :
∑ P ∈ S, P.ord x * ↑P.degree ≤ ↑(Module.finrank (↥k⟮x⟯) F)

Stichtenoth, Proposition 1.3.3: the zeros of x, counted with multiplicity and weighted by their residue degrees, number at most [F : k(x)]. The statement is for an arbitrary finite set S of zeros of x; that there are only finitely many of them is the corollary TauCeti.Place.finite_setOf_ord_pos.

source
theorem TauCeti.Place.card_le_finrank_of_forall_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} [FiniteDimensional (↥k⟮x⟯) F] {S : Finset (Place k F)} (hS : ∀ P ∈ S, 0 < P.ord x) :
S.card ≤ Module.finrank (↥k⟮x⟯) F

A function of a function field has at most [F : k(x)] zeros: the degree-weighted count of TauCeti.Place.sum_ord_mul_degree_le_finrank, read with every weight replaced by 1.

Corollary 1.3.4: the zeros and the poles are finite in number #

source
theorem TauCeti.Place.finite_setOf_ord_pos_of_finiteDimensional {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {x : F} [FiniteDimensional (↥k⟮x⟯) F] :
{P : Place k F | 0 < P.ord x}.Finite

The places at which x has positive order are finite in number whenever F / k(x) is finite-dimensional. For x ≠ 0 these places are the zeros of x; at x = 0 the set is empty, by the junk value ord_P 0 = 0.

source
theorem TauCeti.Place.finite_setOf_ord_pos {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : F) :
{P : Place k F | 0 < P.ord x}.Finite

Stichtenoth, Corollary 1.3.4: an element of an algebraic function field has only finitely many zeros. The set is the support of the totalized order function ord_P on the positive side, so the statement holds for every x : F; it is Corollary 1.3.4 for x ≠ 0, while at x = 0 the junk value ord_P 0 = 0 empties it, the zero function having in truth a zero at every place.

source
theorem TauCeti.Place.finite_setOf_ord_neg {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : F) :
{P : Place k F | P.ord x < 0}.Finite

Stichtenoth, Corollary 1.3.4: an element of an algebraic function field has only finitely many poles. A pole of x is a zero of x⁻¹. As for the zeros, the set is a side of the support of the totalized ord_P and the statement is Corollary 1.3.4 for x ≠ 0; at x = 0, where ord_P 0 = 0, it is empty, as the zero function indeed has no pole.

source
theorem TauCeti.Place.finite_setOf_ord_ne_zero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (x : F) :
{P : Place k F | P.ord x ≠ 0}.Finite

Stichtenoth, Corollary 1.3.4: the places at which an element of an algebraic function field has nonzero order are finite in number. This is the finiteness that makes the principal divisor div x = ∑_P ord_P x · P of a nonzero x a finitely supported formal sum; 0 has no principal divisor, and the statement at x = 0 is the degenerate one that the junk value ord_P 0 = 0 has empty support.