Weierstrass gaps at the rational places of a double cover of the line

Let F / k be a function field with exact constant field k and genus g, and let x ∈ F be transcendental with [F : k(x)] = 2; for g ≥ 2 this is a hyperelliptic function field. The Weierstrass gaps at a rational place P of F are decided by whether P ramifies over k(x):

• if P is ramified, its gaps are the odd numbers 1, 3, …, 2g - 1;
• if P is unramified, its gaps are 1, 2, …, g.

For g ≥ 2 the two gap sequences differ, so a rational place has 2 as a pole number exactly when it ramifies over k(x): the rational places whose gap sequence is not 1, …, g are exactly the ramified ones. In terms of Weierstrass weights, the ramified rational places have the maximal weight g (g - 1) / 2 and the unramified ones have weight 0. Conversely, away from characteristic two or over a perfect field, a function field of genus g ≥ 2 with a rational place at which 2 is a pole number, that is, a rational place of maximal weight, is hyperelliptic.

Main results

• TauCeti.Place.ramificationIdx_mul_relativeDegree_eq_two_of_isPoleNumber: a positive pole number m at P with m · deg P ≤ g makes P the only place over its restriction to k(x).
• TauCeti.Place.isPoleNumber_two_of_one_lt_ramificationIdx: 2 is a pole number at a ramified rational place.
• TauCeti.Place.weierstrassGaps_eq_image_range_of_one_lt_ramificationIdx: the gaps at a ramified rational place are 1, 3, …, 2g - 1.
• TauCeti.Place.weierstrassGaps_eq_Icc_of_ramificationIdx_eq_one: the gaps at an unramified rational place are 1, …, g.
• TauCeti.Place.isPoleNumber_two_iff_one_lt_ramificationIdx: for g ≥ 2, 2 is a pole number at a rational place exactly when the place ramifies over k(x).
• TauCeti.Place.weierstrassWeight_eq_genus_choose_two_iff_one_lt_ramificationIdx and TauCeti.Place.weierstrassWeight_eq_zero_of_ramificationIdx_eq_one: ramified rational places have weight g (g - 1) / 2, unramified ones weight 0.
• TauCeti.weierstrassWeight_eq_genus_choose_two_of_isHyperellipticFunctionField: the rational Weierstrass points of a hyperelliptic function field all have weight g (g - 1) / 2.
• TauCeti.isHyperellipticFunctionField_of_isPoleNumber_two and TauCeti.isHyperellipticFunctionField_of_isPoleNumber_two_of_perfectField: a rational place at which 2 is a pole number makes a function field of genus at least two hyperelliptic, away from characteristic two or over a perfect field.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.6.8 and Proposition 6.2.4.
• H. M. Farkas and I. Kra, Riemann Surfaces, 2nd ed., GTM 71, Springer, 1992, Section III.7, for the gap sequences of a hyperelliptic Riemann surface.

theorem TauCeti.Place.ramificationIdx_mul_relativeDegree_eq_two_of_isPoleNumber {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} {m : ℕ} (hP : P.IsPoleNumber m) (hm : 0 < m) (hmg : m * P.degree ≤ genus k F) : ramificationIdx (↥k⟮x⟯) P * relativeDegree k (↥k⟮x⟯) P = 2

A positive pole number m with m · deg P ≤ g forces e f = 2 over k(x). If [F : k(x)] = 2, then e(P ∣ P₀) f(P ∣ P₀) = 2 for the restriction P₀ of P to k(x). This uses Stichtenoth, Proposition 6.2.4(a).

theorem TauCeti.Place.isPoleNumber_two_of_one_lt_ramificationIdx {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (hram : 1 < ramificationIdx (↥k⟮x⟯) P) : P.IsPoleNumber 2

2 is a pole number at a rational place ramified over k(x).

theorem TauCeti.Place.weierstrassGaps_eq_image_range_of_one_lt_ramificationIdx {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (hram : 1 < ramificationIdx (↥k⟮x⟯) P) : P.weierstrassGaps = Finset.image (fun (i : ℕ) => 2 * i + 1) (Finset.range (genus k F))

The Weierstrass gaps at a ramified rational place are 1, 3, …, 2g - 1.

theorem TauCeti.Place.isGap_of_ramificationIdx_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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (hram : ramificationIdx (↥k⟮x⟯) P = 1) {m : ℕ} (hm : 0 < m) (hmg : m ≤ genus k F) : P.IsGap m

No number up to the genus is a pole number at an unramified rational place.

theorem TauCeti.Place.weierstrassGaps_eq_Icc_of_ramificationIdx_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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (hram : ramificationIdx (↥k⟮x⟯) P = 1) : P.weierstrassGaps = Finset.Icc 1 (genus k F)

The Weierstrass gaps at an unramified rational place are 1, …, g.

theorem TauCeti.Place.isPoleNumber_two_iff_one_lt_ramificationIdx {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] (hg : 2 ≤ genus k F) {P : Place k F} (hP : P.degree = 1) : P.IsPoleNumber 2 ↔ 1 < ramificationIdx (↥k⟮x⟯) P

For g ≥ 2, 2 is a pole number at a rational place exactly when the place ramifies over k(x). In particular the rational places whose gap sequence is not 1, …, g are exactly the ramified ones.

theorem TauCeti.Place.weierstrassWeight_eq_genus_choose_two_iff_one_lt_ramificationIdx {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] (hg : 2 ≤ genus k F) {P : Place k F} (hP : P.degree = 1) : P.weierstrassWeight = (genus k F).choose 2 ↔ 1 < ramificationIdx (↥k⟮x⟯) P

A rational place has the maximal Weierstrass weight g (g - 1) / 2 exactly when it ramifies over k(x), for g ≥ 2: the branch places of the double cover are its places of maximal weight.

theorem TauCeti.Place.weierstrassWeight_eq_zero_of_ramificationIdx_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) {x : F} (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) [FiniteDimensional (↥k⟮x⟯) F] {P : Place k F} (hP : P.degree = 1) (hram : ramificationIdx (↥k⟮x⟯) P = 1) : P.weierstrassWeight = 0

A rational place unramified over k(x) has Weierstrass weight zero.

theorem TauCeti.weierstrassWeight_eq_genus_choose_two_of_isHyperellipticFunctionField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hhyp : IsHyperellipticFunctionField k F) {P : Place k F} (hP₁ : P.degree = 1) (hP : P.weierstrassWeight ≠ 0) : P.weierstrassWeight = (genus k F).choose 2

Every rational Weierstrass point of a hyperelliptic function field has the maximal weight g (g - 1) / 2: a rational place ramified over the index-two rational subfield has that weight, and an unramified one has weight zero.

theorem TauCeti.isHyperellipticFunctionField_of_isPoleNumber_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 : 2 ≤ genus k F) {P : Place k F} (hP : P.degree = 1) (hpole : P.IsPoleNumber 2) : IsHyperellipticFunctionField k F

A rational place at which 2 is a pole number makes a function field of genus g ≥ 2 hyperelliptic, away from characteristic two: the divisor 2P has degree two and ℓ(2P) ≥ 2. By TauCeti.Place.weierstrassWeight_eq_genus_choose_two_iff, these are the rational places of maximal Weierstrass weight g (g - 1) / 2, so a function field that is not hyperelliptic has none. Over a perfect field the characteristic hypothesis can be dropped, see TauCeti.isHyperellipticFunctionField_of_isPoleNumber_two_of_perfectField.

theorem TauCeti.isHyperellipticFunctionField_of_isPoleNumber_two_of_perfectField {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [PerfectField k] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hg : 2 ≤ genus k F) {P : Place k F} (hP : P.degree = 1) (hpole : P.IsPoleNumber 2) : IsHyperellipticFunctionField k F

Over a perfect field, a rational place at which 2 is a pole number makes a function field of genus g ≥ 2 hyperelliptic, in every characteristic: the divisor 2P of degree two with ℓ(2P) ≥ 2 gives a rational subfield of index two. Over a perfect field the positive genus rules out a purely inseparable index-two extension, so F is separable over this subfield, see TauCeti.isHyperellipticFunctionField_iff_two_le_genus_and_exists_finrank_adjoin_eq_two.