Genus-zero function fields with a divisor of degree one

Let F / k be an algebraic function field with exact constant field. If F has genus zero and admits a divisor of degree one, then F is a rational function field over k. This is the nontrivial implication of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Proposition 1.6.3.

The degree-one hypothesis is deliberately stated for an arbitrary divisor, not for a rational place. Riemann--Roch gives a nonzero section of that divisor. Translating the section by its principal divisor produces an effective divisor of degree one, whose support contains a rational place. At that place, the genus-zero prescribed-pole theorem produces a function with one simple pole. The product formula identifies the degree of the resulting rational subfield with one, so Mathlib's RatFunc.algEquivOfTranscendental extends to the required equivalence.

This module proves the forward implication without weakening the degree-one-divisor hypothesis to the existence of a rational place. The converse, that a function field generated by a single transcendental element has genus zero, is proved here too, by the growth estimate for the powers of that element against Riemann--Roch in large degree.

Main results

• TauCeti.exists_place_degree_eq_one_of_genus_eq_zero_of_divisor_degree_eq_one: genus zero and a degree-one divisor produce a rational place.
• TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one: genus zero and a degree-one divisor make the function field rational.
• TauCeti.genus_eq_zero_of_adjoin_eq_top: conversely, a function field generated by one transcendental element has genus zero.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.6.3 and Remark 1.6.4.

theorem TauCeti.exists_place_degree_eq_one_of_genus_eq_zero_of_divisor_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : genus k F = 0) (hdegree : ∃ (D : Divisor k F), Divisor.degree D = 1) : ∃ (P : Place k F), P.degree = 1

A genus-zero function field with a divisor of degree one has a rational place.

Riemann--Roch gives dimension two for the degree-one divisor. A nonzero section translates it to a linearly equivalent effective divisor, still of degree one, and such a divisor contains a rational place.

theorem TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : genus k F = 0) (hdegree : ∃ (D : Divisor k F), Divisor.degree D = 1) : Nonempty (F ≃ₐ[k] RatFunc k)

Genus zero plus a divisor of degree one implies rationality (the nontrivial direction of Stichtenoth, Proposition 1.6.3).

The conclusion is an equivalence of k-algebras F ≃ₐ[k] RatFunc k. No perfectness, separability, or rational-place hypothesis is added: exactness of the constant field is the only extra hypothesis required by Riemann--Roch.

theorem TauCeti.genus_eq_zero_of_adjoin_eq_top {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) (htop : k⟮x⟯ = ⊤) : genus k F = 0

A rational function field has genus zero (Stichtenoth, Example 1.4.18), stated for a function field that is generated by one transcendental element rather than for RatFunc k itself.

Neither the function field hypothesis nor the exactness of the field of constants has to be assumed: both follow from hx and htop. Together with TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one this makes genus zero with a degree-one divisor the exact characterization of rationality.

theorem TauCeti.genus_adjoin_simple_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : genus k ↥k⟮x⟯ = 0

k(x) has genus zero for every transcendental x, as a function field in its own right.