The genus-two field y² = x⁵ - 1

Construct the quadratic field given by y² = x⁵ - 1. Its constants are exact in every characteristic. In characteristic other than two and five, it has genus two, and its different is the sum of the distinct zeros of y and its rational place at infinity, with total degree six. Thus the finite branch places contribute degree five whether or not the fifth roots of unity are rational over the constants.

The Weierstrass gaps at a rational place are {1, 3} when the place ramifies over k(x) and {1, 2} when it does not. The place at infinity is of the first kind, so it is a Weierstrass place. An affine point (a, b) with b ≠ 0, such as (0, i) when i² = -1 in k, gives a rational place of the second kind. These are the two gap sequences possible in genus two.

Main results

• TauCeti.GenusTwo.genus_eq_two and TauCeti.GenusTwo.degree_different: the genus is two and the different of F / k(x) has degree six.
• TauCeti.GenusTwo.weierstrassGaps_eq_of_one_lt_ramificationIdx and TauCeti.GenusTwo.weierstrassGaps_eq_of_ramificationIdx_eq_one: the gaps at a rational place are {1, 3} or {1, 2} according as it ramifies over k(x) or not.
• TauCeti.GenusTwo.weierstrassGaps_eq_of_restrict_eq_infty: the place at infinity has gaps {1, 3}.
• TauCeti.GenusTwo.exists_weierstrassGaps_eq_of_sq_eq and TauCeti.GenusTwo.exists_weierstrassGaps_eq_of_sq_eq_neg_one: the rational place of an affine point (a, b) with b ≠ 0, for instance (0, i), has gaps {1, 2}.

References

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 6.2.3, Theorem 1.6.8 and Proposition 6.2.4.

theorem TauCeti.GenusTwo.odd_natDegree (k : Type u_1) [Field k] : Odd (Polynomial.X ^ 5 - Polynomial.C 1).natDegree

The quintic x⁵ - 1 has odd degree over every field.

theorem TauCeti.GenusTwo.squarefree (k : Type u_1) [Field k] (h5 : 5 ≠ 0) : Squarefree (Polynomial.X ^ 5 - Polynomial.C 1)

The quintic x⁵ - 1 is squarefree in characteristic other than five.

noncomputable def TauCeti.GenusTwo.equationPolynomial (k : Type u_1) [Field k] : Polynomial (RatFunc k)

The quadratic equation over k(x) defining y² = x⁵ - 1.

theorem TauCeti.GenusTwo.equationPolynomial_def (k : Type u_1) [Field k] : equationPolynomial k = Polynomial.X ^ 2 - Polynomial.C ((algebraMap (Polynomial k) (RatFunc k)) (Polynomial.X ^ 5 - Polynomial.C 1))

The defining polynomial, for computation without unfolding its body.

@[reducible, inline]

abbrev TauCeti.GenusTwo.FunctionField (k : Type u_1) [Field k] : Type u_1

The function field of the affine equation y² = x⁵ - 1, obtained by adjoining its root to k(x).

instance TauCeti.GenusTwo.instFactIrreduciblePolynomialRatFuncEquationPolynomial (k : Type u_1) [Field k] : Fact (Irreducible (equationPolynomial k))

Irreducibility supplies the field structure on the root algebra.

noncomputable def TauCeti.GenusTwo.genY (k : Type u_1) [Field k] : FunctionField k

The y-coordinate in the quadratic field.

theorem TauCeti.GenusTwo.genY_def (k : Type u_1) [Field k] : genY k = AdjoinRoot.root (equationPolynomial k)

The y-coordinate is the root in the defining root algebra.

noncomputable def TauCeti.GenusTwo.genX (k : Type u_1) [Field k] : FunctionField k

The x-coordinate in the quadratic field: the image of the variable of k(x).

theorem TauCeti.GenusTwo.genX_def (k : Type u_1) [Field k] : genX k = (algebraMap (RatFunc k) (FunctionField k)) RatFunc.X

The x-coordinate is the image of the variable of k(x).

theorem TauCeti.GenusTwo.genY_sq (k : Type u_1) [Field k] : genY k ^ 2 = (algebraMap (RatFunc k) (FunctionField k)) ((algebraMap (Polynomial k) (RatFunc k)) (Polynomial.X ^ 5 - Polynomial.C 1))

The coordinate y satisfies the defining equation.

theorem TauCeti.GenusTwo.adjoin_genY_eq_top (k : Type u_1) [Field k] : (RatFunc k)⟮genY k⟯ = ⊤

The quadratic field is generated by y over k(x).

theorem TauCeti.GenusTwo.finrank_eq_two (k : Type u_1) [Field k] : Module.finrank (RatFunc k) (FunctionField k) = 2

The field extension over k(x) is quadratic.

instance TauCeti.GenusTwo.instFiniteDimensionalRatFuncFunctionField (k : Type u_1) [Field k] : FiniteDimensional (RatFunc k) (FunctionField k)

The model is finite-dimensional over the rational function field.

theorem TauCeti.GenusTwo.isFunctionField (k : Type u_1) [Field k] : IsFunctionField k (FunctionField k)

The constructed field is an algebraic function field over k.

theorem TauCeti.GenusTwo.genus_eq_two (k : Type u_1) [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) : genus k (FunctionField k) = 2

The genus of y² = x⁵ - 1 is two in characteristic other than two and five.

@[simp]

theorem TauCeti.GenusTwo.genY_ne_zero (k : Type u_1) [Field k] : genY k ≠ 0

The y-coordinate is nonzero.

instance TauCeti.GenusTwo.instIsSeparableRatFuncFunctionFieldOfNeZeroOfNat (k : Type u_1) [Field k] [NeZero 2] : Algebra.IsSeparable (RatFunc k) (FunctionField k)

Away from characteristic two the quadratic model is separable over k(x).

theorem TauCeti.GenusTwo.isIntegrallyClosedIn (k : Type u_1) [Field k] : IsIntegrallyClosedIn k (FunctionField k)

The constants of y² = x⁵ - 1 are exactly k in every characteristic.

theorem TauCeti.GenusTwo.degree_different (k : Type u_1) [Field k] [NeZero 2] (h5 : 5 ≠ 0) : Divisor.degree (Divisor.different k (FunctionField k) ⋯) = 6

The different has degree six: Hurwitz reads 2 · 2 - 2 = -2 · 2 + 6.

theorem TauCeti.GenusTwo.exists_different_eq_ofFinset (k : Type u_1) [Field k] [NeZero 2] (h5 : 5 ≠ 0) : ∃ (P : Place k (FunctionField k)), P.degree = 1 ∧ Place.restrict k (RatFunc k) P = Place.infty k ∧ Divisor.different k (FunctionField k) ⋯ = AlgebraicGeometry.WeilDivisor.ofFinset (Divisor.zeros ⋯ (Units.mk0 (genY k) ⋯)).support + AlgebraicGeometry.WeilDivisor.ofPoint P ∧ Divisor.degree (Divisor.zeros ⋯ (Units.mk0 (genY k) ⋯)) = 5

The different consists of the distinct zeros of y and a rational place at infinity. The finite part has degree five, independently of the splitting of x⁵ - 1 over k.

Weierstrass gaps

@[simp]

theorem TauCeti.GenusTwo.genY_sq_eq (k : Type u_1) [Field k] : genY k ^ 2 = genX k ^ 5 - 1

The affine equation in the coordinates x and y: y² = x⁵ - 1.

theorem TauCeti.GenusTwo.transcendental_genX (k : Type u_1) [Field k] : Transcendental k (genX k)

The coordinate x is transcendental over k.

theorem TauCeti.GenusTwo.finrank_adjoin_genX (k : Type u_1) [Field k] : Module.finrank (↥k⟮genX k⟯) (FunctionField k) = 2

The field is quadratic over the subfield k⟮x⟯ generated by x.

instance TauCeti.GenusTwo.instFiniteDimensionalSubtypeFunctionFieldMemIntermediateFieldAdjoinSingletonSetGenX (k : Type u_1) [Field k] : FiniteDimensional (↥k⟮genX k⟯) (FunctionField k)

The field is finite-dimensional over the subfield k⟮x⟯ generated by x.

theorem TauCeti.GenusTwo.weierstrassGaps_eq_of_one_lt_ramificationIdx {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) {P : Place k (FunctionField k)} (hP : P.degree = 1) (hram : 1 < Place.ramificationIdx (RatFunc k) P) : P.weierstrassGaps = {1, 3}

The ramified rational places of y² = x⁵ - 1 have gaps 1, 3: in characteristic other than two and five, a rational place ramified over k(x) has Weierstrass gaps {1, 3}.

theorem TauCeti.GenusTwo.weierstrassGaps_eq_of_ramificationIdx_eq_one {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) {P : Place k (FunctionField k)} (hP : P.degree = 1) (hram : Place.ramificationIdx (RatFunc k) P = 1) : P.weierstrassGaps = {1, 2}

The unramified rational places of y² = x⁵ - 1 have gaps 1, 2: in characteristic other than two and five, a rational place unramified over k(x) has Weierstrass gaps {1, 2}.

theorem TauCeti.GenusTwo.weierstrassGaps_eq_of_restrict_eq_infty {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) {P : Place k (FunctionField k)} (hP : Place.restrict k (RatFunc k) P = Place.infty k) : P.weierstrassGaps = {1, 3}

The place at infinity of y² = x⁵ - 1 is a Weierstrass place: in characteristic other than two and five, the place over the place at infinity of k(x), which is rational, has Weierstrass gaps {1, 3}.

theorem TauCeti.GenusTwo.exists_weierstrassGaps_eq_of_sq_eq {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) {a b : k} (hb : b ≠ 0) (hab : b ^ 2 = a ^ 5 - 1) : ∃ (P : Place k (FunctionField k)), P.degree = 1 ∧ 0 < P.ord (genX k - (algebraMap k (FunctionField k)) a) ∧ 0 < P.ord (genY k - (algebraMap k (FunctionField k)) b) ∧ P.weierstrassGaps = {1, 2}

A rational point off the branch locus gives a rational place with gaps 1, 2: in characteristic other than two and five, if b ≠ 0 and b² = a⁵ - 1, then there is a rational place at which x - a and y - b both vanish, and its Weierstrass gaps are {1, 2}.

theorem TauCeti.GenusTwo.exists_weierstrassGaps_eq_of_sq_eq_neg_one {k : Type u_1} [Field k] (h2 : 2 ≠ 0) (h5 : 5 ≠ 0) {i : k} (hi : i ^ 2 = -1) : ∃ (P : Place k (FunctionField k)), P.degree = 1 ∧ 0 < P.ord (genX k) ∧ 0 < P.ord (genY k - (algebraMap k (FunctionField k)) i) ∧ P.weierstrassGaps = {1, 2}

The rational place of the point (0, i) has gaps 1, 2: in characteristic other than two and five, if i² = -1 in k, then there is a rational place at which x and y - i vanish, and its Weierstrass gaps are {1, 2}.