A genus-zero function field that is not rational

Genus zero together with a divisor of degree one forces a function field to be rational (TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one, Stichtenoth, Proposition 1.6.3). Genus zero alone does not. This file records the standard counterexample: the function field of the conic x² + y² + 1 = 0 over a field k in which a² + b² + 1 = 0 has no solution, such as ℝ, ℚ, or any ordered field (Stichtenoth, Remark 1.6.4).

Over such a k, a field containing x and y with x² + y² + 1 = 0 has no place of degree one: the residue field of a rational place P is k, so if x is regular at P the residues of x and y solve a² + b² + 1 = 0, and if x has a pole at P then so does y, and the residue of y / x is a square root of −1. In particular such a field is not isomorphic to k(x).

The function field of the conic is F = k(x, y) with y² = −(x² + 1), an extension y² = f(x) with f squarefree of degree two whenever 2 ≠ 0 in k; so it has genus ⌊(2 − 1) / 2⌋ = 0 and exact constant field k by TauCeti.genus_eq_of_sq_eq. When the conic has no k-point it therefore has no divisor of degree one either.

Main results

• TauCeti.Place.degree_ne_one_of_sq_add_sq_add_one_eq_zero: over such a k, a field containing x and y with x² + y² + 1 = 0 has no place of degree one.
• TauCeti.isEmpty_algEquiv_ratFunc_of_sq_add_sq_add_one_eq_zero: such a field is not rational.
• TauCeti.genus_eq_zero_of_sq_add_sq_add_one_eq_zero: the conic has genus zero when 2 ≠ 0.
• TauCeti.not_exists_divisor_degree_eq_one_of_sq_add_sq_add_one_eq_zero: the conic without k-points has no divisor of degree one.

References

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

theorem TauCeti.Place.degree_ne_one_of_sq_add_sq_add_one_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hk : ∀ (a b : k), a ^ 2 + b ^ 2 + 1 ≠ 0) {x y : F} (hxy : x ^ 2 + y ^ 2 + 1 = 0) (P : Place k F) : P.degree ≠ 1

The conic x² + y² + 1 = 0 has no rational place. If a² + b² + 1 = 0 has no solution in k, then a field F / k containing x and y with x² + y² + 1 = 0 has no place of degree one: at such a place the relation, or its rescaling (y / x)² + (1 / x)² + 1 = 0 at a pole of x, would reduce to a solution in the residue field k.

theorem TauCeti.isEmpty_algEquiv_ratFunc_of_sq_add_sq_add_one_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hk : ∀ (a b : k), a ^ 2 + b ^ 2 + 1 ≠ 0) {x y : F} (hxy : x ^ 2 + y ^ 2 + 1 = 0) : IsEmpty (F ≃ₐ[k] RatFunc k)

A field with a pointless conic is not rational (Stichtenoth, Remark 1.6.4): if a² + b² + 1 = 0 has no solution in k, then a field F / k containing x and y with x² + y² + 1 = 0 admits no k-isomorphism with k(x), since such an isomorphism would transport the rational place at infinity of k(x) to a rational place of F.

theorem TauCeti.isFunctionField_of_sq_add_sq_add_one_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (algebraMap (RatFunc k) F) RatFunc.X ^ 2 + y ^ 2 + 1 = 0) : IsFunctionField k F

The conic is a function field over k, in every characteristic: y is a root of the monic quadratic Y ^ 2 + (x ^ 2 + 1) over k(x).

theorem TauCeti.isIntegrallyClosedIn_of_sq_add_sq_add_one_eq_zero {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) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (algebraMap (RatFunc k) F) RatFunc.X ^ 2 + y ^ 2 + 1 = 0) : IsIntegrallyClosedIn k F

The conic has exact constant field k when 2 ≠ 0 in k.

theorem TauCeti.genus_eq_zero_of_sq_add_sq_add_one_eq_zero {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) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (algebraMap (RatFunc k) F) RatFunc.X ^ 2 + y ^ 2 + 1 = 0) : genus k F = 0

The conic has genus zero when 2 ≠ 0 in k: y ^ 2 = -(x ^ 2 + 1) is an extension y ^ 2 = f(x) with f squarefree of degree two, so its genus is ⌊(2 - 1) / 2⌋ = 0.

theorem TauCeti.not_exists_divisor_degree_eq_one_of_sq_add_sq_add_one_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (hk : ∀ (a b : k), a ^ 2 + b ^ 2 + 1 ≠ 0) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : (algebraMap (RatFunc k) F) RatFunc.X ^ 2 + y ^ 2 + 1 = 0) : ¬∃ (D : Divisor k F), Divisor.degree D = 1

The pointless conic has no divisor of degree one: it has genus zero, and a genus-zero function field with a divisor of degree one has a rational place, which the conic lacks. With TauCeti.genus_eq_zero_of_sq_add_sq_add_one_eq_zero, this records that the degree-one divisor in TauCeti.nonempty_algEquiv_ratFunc_of_genus_eq_zero_of_divisor_degree_eq_one cannot be dropped.