Hyperelliptic function fields

An algebraic function field F / k is hyperelliptic when it has genus at least two and contains a rational subfield k(x) of index two over which it is separable. Separability is part of the definition rather than a consequence of it: over a constant field of characteristic two an index-two subfield can be inseparable, and no standing hypothesis of this development rules that out. Away from characteristic two it is automatic, by TauCeti.Algebra.isSeparable_of_finrank_eq_two.

The content of this file is the intrinsic description of that subfield, which mentions no element of F at all: F is hyperelliptic exactly when its genus is at least two and some divisor of degree two has ℓ(A) ≥ 2. One direction is the pole divisor (x)_∞ of the index-two generator, whose Riemann--Roch space contains 1 and x. The other moves A inside its class to an effective divisor B, picks a function x ∈ L(B) outside the constants — which positivity of ℓ(B) over the line of constants provides — and reads [F : k(x)] = deg (x)_∞ off the product formula: the pole divisor of x is dominated by B, so the degree is at most two, and it is not one because a rational function field has genus zero.

In genus two the canonical divisor is such an A, since deg W = 2g - 2 = 2 and ℓ(W) = g = 2; so every function field of genus two has an index-two rational subfield, and away from characteristic two every function field of genus two is hyperelliptic.

Main definitions

• TauCeti.IsHyperellipticFunctionField: genus at least two together with a separable rational subfield of index two.

Main results

• TauCeti.exists_transcendental_finrank_adjoin_eq_two_of_degree_eq_two: a divisor of degree two with ℓ ≥ 2 produces a rational subfield of index two; no hypothesis on the characteristic.
• TauCeti.isHyperellipticFunctionField_iff_two_le_genus_and_exists_degree_eq_two_and_two_le_dim: the intrinsic characterization, away from characteristic two.
• TauCeti.exists_transcendental_finrank_adjoin_eq_two_of_genus_eq_two and TauCeti.isHyperellipticFunctionField_of_genus_eq_two: genus two gives an index-two rational subfield, and away from characteristic two makes F hyperelliptic.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section VI.2: Definition 6.2.1 and Lemma 6.2.2.

structure TauCeti.IsHyperellipticFunctionField (k : Type u_3) (F : Type u_4) [Field k] [Field F] [Algebra k F] : Prop

A hyperelliptic function field (Stichtenoth, Definition 6.2.1, with separability of the index-two subextension made part of the definition): genus at least two together with an element x transcendental over k such that F / k(x) is separable of degree two.

Being an algebraic function field is not part of the predicate: the hypothesis TauCeti.IsFunctionField, like the exactness of the constant field, is kept as a separate hypothesis on the statements that need it, as everywhere in this development.

In characteristic two an index-two subextension can be purely inseparable, and such an F is deliberately outside this model class; away from characteristic two the separability clause is automatic, so there the predicate agrees with Stichtenoth's index-two definition.

• two_le_genus : 2 ≤ genus k F

  A hyperelliptic function field has genus at least two.

• exists_separable_finrank_adjoin_eq_two : ∃ (x : F), Transcendental k x ∧ Module.finrank (↥k⟮x⟯) F = 2 ∧ Algebra.IsSeparable (↥k⟮x⟯) F

  A hyperelliptic function field has a separable rational subfield of index two.

From the index-two subfield to a divisor of degree two

theorem TauCeti.IsHyperellipticFunctionField.exists_degree_eq_two_and_two_le_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hhyp : IsHyperellipticFunctionField k F) : ∃ (A : Divisor k F), Divisor.degree A = 2 ∧ 2 ≤ A.dim

A hyperelliptic function field has a divisor of degree two whose Riemann--Roch space has dimension at least two. This is the forward half of the intrinsic characterization TauCeti.isHyperellipticFunctionField_iff_two_le_genus_and_exists_degree_eq_two_and_two_le_dim, and it needs no hypothesis on the characteristic.

From a divisor of degree two to the index-two subfield

theorem TauCeti.exists_transcendental_finrank_adjoin_eq_two_of_degree_eq_two {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) {A : Divisor k F} (hA : Divisor.degree A = 2) (hdim : 2 ≤ A.dim) : ∃ (x : F), Transcendental k x ∧ Module.finrank (↥k⟮x⟯) F = 2

A divisor of degree two whose Riemann--Roch space has dimension at least two produces a rational subfield of index two, as soon as the genus is positive.

No hypothesis on the characteristic is made, and no separability is claimed: this is the part of Stichtenoth's Section VI.2 dictionary that holds over an arbitrary constant field. The genus hypothesis cannot be dropped: over a rational function field the subfield produced would be all of F.

theorem TauCeti.isHyperellipticFunctionField_iff_two_le_genus_and_exists_degree_eq_two_and_two_le_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h2 : 2 ≠ 0) : IsHyperellipticFunctionField k F ↔ 2 ≤ genus k F ∧ ∃ (A : Divisor k F), Divisor.degree A = 2 ∧ 2 ≤ A.dim

The intrinsic characterization of hyperelliptic function fields away from characteristic two (Stichtenoth, Section VI.2): F is hyperelliptic exactly when its genus is at least two and some divisor of degree two has a Riemann--Roch space of dimension at least two.

The characteristic hypothesis is used only to make the index-two subextension separable, so the forward implication TauCeti.IsHyperellipticFunctionField.exists_degree_eq_two_and_two_le_dim and the subfield half of the converse hold without it.

Genus two

theorem TauCeti.exists_degree_eq_two_and_dim_eq_two_of_genus_eq_two {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 = 2) : ∃ (A : Divisor k F), Divisor.degree A = 2 ∧ A.dim = 2

A function field of genus two has a divisor of degree two whose Riemann--Roch space has dimension exactly two. It supplies the divisor hypotheses of TauCeti.exists_transcendental_finrank_adjoin_eq_two_of_degree_eq_two in genus two.

theorem TauCeti.exists_transcendental_finrank_adjoin_eq_two_of_genus_eq_two {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 = 2) : ∃ (x : F), Transcendental k x ∧ Module.finrank (↥k⟮x⟯) F = 2

Every function field of genus two has a rational subfield of index two (Stichtenoth, Lemma 6.2.2), over an arbitrary constant field. Separability of that subextension is not claimed here; away from characteristic two it is automatic, see TauCeti.isHyperellipticFunctionField_of_genus_eq_two.

theorem TauCeti.isHyperellipticFunctionField_of_genus_eq_two {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (h2 : 2 ≠ 0) (hg : genus k F = 2) : IsHyperellipticFunctionField k F

Every function field of genus two away from characteristic two is hyperelliptic (Stichtenoth, Lemma 6.2.2).