The genus of y ^ 2 = f(x)

Let k be a field of characteristic other than two and F / k(x) an extension generated by an element y with y ^ 2 = f(x), where f ∈ k[X] is squarefree of degree m ≥ 1; then F / k(x) is finite and separable. This file computes the invariants of F / k from the ramification of F / k(x):

• F / k(x) has degree two, and k is the exact field of constants of F;
• the places of k(x) that ramify in F are the zeros of f, together with the place at infinity when m is odd;
• the different of F / k(x) has degree m + (m mod 2), so the Hurwitz genus formula 2g - 2 = -2 · 2 + deg Diff(F / k(x)) gives g = ⌊(m - 1) / 2⌋;
• for m ≥ 5, F / k is a hyperelliptic function field.

The local input is the ramification of the radical extension y ^ 2 = f at a place P of k(x) (TauCeti.Place.ramificationIdx_eq_of_pow_eq_of_prime and TauCeti.Place.differentExponent_eq_of_pow_eq_of_prime): the places above P are ramified, with different exponent one, exactly when ord_P f is odd. Since f is a squarefree polynomial, ord_P f is 0 or 1 at a finite place, and -m at infinity. To add up the different without counting the places above each ramified P, compare it with the conorm of the divisor B of k(x) consisting of the places where ord_P f is odd: every place above B has ramification index two, so Con B = 2 · Diff(F / k(x)), and the conorm multiplies degrees by [F : k(x)] = 2. Hence deg Diff(F / k(x)) = deg B, and deg B = m + (m mod 2) because the zeros of f have total degree m by the product formula.

Exactness of the constants comes from the ramification as well: an extension of prime degree in which some place ramifies is not a constant field extension, so it acquires no new constants (TauCeti.isIntegrallyClosedIn_of_finrank_prime_of_ramificationIdx_ne_one).

Main results

• TauCeti.finrank_ratFunc_eq_two_of_sq_eq and TauCeti.isIntegrallyClosedIn_of_sq_eq: the degree of F / k(x) and exactness of the constant field k.
• TauCeti.Place.one_lt_ramificationIdx_iff_of_sq_eq: the ramified places.
• TauCeti.degree_different_ratFunc_of_sq_eq: deg Diff(F / k(x)) = m + (m mod 2).
• TauCeti.genus_eq_of_sq_eq: the genus of y ^ 2 = f(x) is ⌊(m - 1) / 2⌋.
• TauCeti.isHyperellipticFunctionField_of_sq_eq: for m ≥ 5 the field is hyperelliptic.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Example 3.7.6 and Proposition 6.2.3.

The branch divisor on k(x)

The degree of y ^ 2 = f

theorem TauCeti.finrank_ratFunc_eq_two_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] {f : Polynomial k} (hf : Squarefree f) (hdeg : 0 < f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) : Module.finrank (RatFunc k) F = 2

y ^ 2 = f has degree two over k(x) for a squarefree nonconstant polynomial f. No hypothesis on the characteristic is needed.

Ramification and the different of y ^ 2 = f

theorem TauCeti.Place.one_lt_ramificationIdx_iff_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) (P' : Place k F) : 1 < ramificationIdx (RatFunc k) P' ↔ restrict k (RatFunc k) P' = infty k ∧ Odd f.natDegree ∨ ∃ (q : Polynomial k) (hq : Irreducible q), q ∣ f ∧ restrict k (RatFunc k) P' = adicOfIrreducible hq

The ramified places of y ^ 2 = f (Stichtenoth, Proposition 6.2.3): a place of F is ramified over k(x) exactly when it lies over a zero of f, or over the place at infinity with deg f odd. Its ramification index is then two, by TauCeti.Place.ramificationIdx_eq_of_pow_eq_of_prime.

theorem TauCeti.degree_different_ratFunc_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hdeg : 0 < f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) : Divisor.degree (Divisor.different k F ⋯) = ↑f.natDegree + ↑f.natDegree % 2

The degree of the different of y ^ 2 = f: for a squarefree polynomial f of degree m ≥ 1, the different of F / k(x) has degree m + (m mod 2), the number of branch points counted with their degrees.

The constants and the genus of y ^ 2 = f

theorem TauCeti.isIntegrallyClosedIn_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hdeg : 0 < f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) : IsIntegrallyClosedIn k F

The constant field of y ^ 2 = f is exact: for a squarefree nonconstant polynomial f, k is algebraically closed in F = k(x, y).

theorem TauCeti.genus_eq_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hdeg : 0 < f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) : genus k F = (f.natDegree - 1) / 2

The genus of y ^ 2 = f(x) (Stichtenoth, Example 3.7.6 and Proposition 6.2.3): away from characteristic two, if F = k(x, y) with y ^ 2 = f(x) for a squarefree polynomial f of degree m ≥ 1, then F / k has genus ⌊(m - 1) / 2⌋: (m - 1) / 2 for odd m and (m - 2) / 2 for even m.

theorem TauCeti.isHyperellipticFunctionField_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hdeg : 5 ≤ f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) : IsHyperellipticFunctionField k F

y ^ 2 = f(x) is hyperelliptic when deg f ≥ 5 (Stichtenoth, Proposition 6.2.3): away from characteristic two, if F = k(x, y) with y ^ 2 = f(x) for a squarefree polynomial f of degree at least five, then F / k is a hyperelliptic function field.