The regular differentials of a function field with a rational subfield of index two

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. The divisor (g - 1) · (x)_∞ is canonical (TauCeti.divisorClass_sub_one_zsmul_poles_eq_canonicalClass), so it is the divisor of a Weil differential ω₀. By the duality theorem the regular differentials Ω_F(0) are the multiples z · ω₀ with z ∈ L((g - 1) · (x)_∞), and that space is spanned by 1, x, …, x^{g-1}. Hence ω₀, x ω₀, …, x^{g-1} ω₀ is a k-basis of Ω_F(0), and the quotient of two regular differentials always lies in k(x). For g ≥ 2 the quotient of x ω₀ by ω₀ is x itself, so these quotients generate k(x): the regular differentials single out the rational subfield of index two.

For the model y ^ 2 = f(x) with f squarefree of degree m ≥ 1, away from characteristic two, the differential ω₀ is explicit: dx / y has divisor (g - 1) · (x)_∞. Indeed (dx) = -2 (x)_∞ + Diff(F / k(x)), and at a place Q above a place P of k(x) with ramification index e the three terms contribute as follows.

• Above a zero of f: e = 2, the different exponent is 1 and ord_Q y = 1.
• Above any other finite place: e = 1 and both the different exponent and ord_Q y vanish.
• Above infinity, for m odd: e = 2, the different exponent is 1, ord_Q y = -m and ord_Q x = -2, so the coefficient is m - 3 = 2 (g - 1).
• Above infinity, for m even: e = 1, the different exponent is 0, ord_Q y = -m / 2 and ord_Q x = -1, so the coefficient is m / 2 - 2 = g - 1.

So the regular differentials of y ^ 2 = f(x) are exactly p(x) dx / y with deg p < g.

Main results

• TauCeti.weilDifferentialFiltration_zero_eq_span_pow: if (ω₀) = (g - 1) · (x)_∞, then Ω_F(0) is spanned by x ^ i · ω₀ for i < g; these are linearly independent by TauCeti.linearIndependent_repartitionDualMul_pow.
• TauCeti.mem_adjoin_of_repartitionDualMul_eq: the quotient of two regular differentials lies in k(x).
• TauCeti.adjoin_setOf_repartitionDualMul_eq_adjoin: for g ≥ 2, these quotients generate k(x).
• TauCeti.weilDifferentialDivisor_repartitionDualMul_inv_weilDifferentialCotrace_of_sq_eq: for y ^ 2 = f(x), the differential dx / y has divisor (g - 1) · (x)_∞.
• TauCeti.weilDifferentialFiltration_zero_eq_span_of_sq_eq: the regular differentials of y ^ 2 = f(x) are spanned by x ^ i dx / y for i < g.

References

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

A rational subfield of index two

theorem TauCeti.weilDifferentialFiltration_zero_eq_span_pow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) {ω : Module.Dual k ↥(repartitionSpace k F)} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} ((↑(genus k F) - 1) • Divisor.poles hF (Units.mk0 x ⋯))) : weilDifferentialFiltration 0 = Submodule.span k (Set.range fun (i : Fin (genus k F)) => ((repartitionDualMul hF) (x ^ ↑i)) ω)

The regular differentials over a rational subfield of index two: if [F : k(x)] = 2 and the Weil differential ω has divisor (g - 1) · (x)_∞, then the regular differentials are spanned by ω, x ω, …, x^{g-1} ω. These are linearly independent (TauCeti.linearIndependent_repartitionDualMul_pow), so they form a basis of Ω_F(0).

theorem TauCeti.mem_adjoin_of_repartitionDualMul_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) {ω η : Module.Dual k ↥(repartitionSpace k F)} (hωmem : ω ∈ weilDifferentialFiltration 0) (hηmem : η ∈ weilDifferentialFiltration 0) (hη : η ≠ 0) {z : F} (hz : ((repartitionDualMul hF) z) η = ω) : z ∈ k⟮x⟯

Quotients of regular differentials lie in the rational subfield of index two: if [F : k(x)] = 2 and z · η = ω for regular Weil differentials ω and η ≠ 0, then z ∈ k(x).

theorem TauCeti.adjoin_setOf_repartitionDualMul_eq_adjoin {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hx : Transcendental k x) (hdeg : Module.finrank (↥k⟮x⟯) F = 2) (hg : 2 ≤ genus k F) : IntermediateField.adjoin k {z : F | ∃ ω ∈ weilDifferentialFiltration 0, ∃ η ∈ weilDifferentialFiltration 0, η ≠ 0 ∧ ((repartitionDualMul hF) z) η = ω} = k⟮x⟯

Quotients of regular differentials generate the rational subfield of index two: if [F : k(x)] = 2 and g ≥ 2, then the quotients z of regular Weil differentials, z · η = ω with η ≠ 0, generate k(x). Each such quotient lies in k(x) (TauCeti.mem_adjoin_of_repartitionDualMul_eq), and x is the quotient of x ω₀ by ω₀.

The model y ^ 2 = f(x)

theorem TauCeti.weilDifferentialDivisor_repartitionDualMul_inv_weilDifferentialCotrace_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc 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)) : weilDifferentialDivisor ⋯ ⋯ ⋯ ⋯ = (↑(genus k F) - 1) • Divisor.poles ⋯ ((Units.map ↑(algebraMap (RatFunc k) F)) (Units.mk0 RatFunc.X ⋯))

The divisor of dx / y: away from characteristic two, if F = k(x, y) with y ^ 2 = f(x) for a squarefree polynomial f of degree m ≥ 1, then the Weil differential dx / y has divisor (g - 1) · (x)_∞, where g = ⌊(m - 1) / 2⌋ is the genus of F and dx is the cotrace of the normalized differential of k(x).

theorem TauCeti.weilDifferentialFiltration_zero_eq_span_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc 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)) : weilDifferentialFiltration 0 = Submodule.span k (Set.range fun (i : Fin (genus k F)) => ((repartitionDualMul ⋯) ((algebraMap (RatFunc k) F) RatFunc.X ^ ↑i / ↑y)) ↑((weilDifferentialCotrace k F ⋯ ⋯) ⟨ratFuncWeilDifferential k, ⋯⟩))

The regular differentials of y ^ 2 = f(x): away from characteristic two, if F = k(x, y) with y ^ 2 = f(x) for a squarefree polynomial f of degree m ≥ 1, then the regular Weil differentials of F are spanned by x ^ i dx / y for i < g, where g = ⌊(m - 1) / 2⌋ is the genus of F and dx is the cotrace of the normalized differential of k(x). They are linearly independent (TauCeti.linearIndependent_repartitionDualMul_pow applied to dx / y), so they form a basis of Ω_F(0).