The divisor of the invariant differential

Let W be an elliptic Weierstrass curve over a field F, with function field F(W) and coordinate functions x and y. Its invariant differential ω = dx / (2y + a₁x + a₃) lives in the Kähler differentials Ω[F(W)/F], and the Kähler–Weil comparison determined by the separating element x carries it to a nonzero Weil differential of F(W) / F. This file proves that this Weil differential has divisor zero: ω is regular and nonvanishing at every place of F(W) (Silverman, Proposition III.1.5).

The divisor of dx is -2 (x)_∞ + Diff(F(W) / F(x)), so

(ω) = -div (2y + a₁x + a₃) - 2 (x)_∞ + Diff(F(W) / F(x)).

No different exponent has to be computed exactly. At a place P where x is regular, y is a root of Y² + (a₁x + a₃) Y - (x³ + a₂x² + a₄x + a₆), a monic equation over the valuation ring below P whose derivative at y is 2y + a₁x + a₃; at a pole of x, the function y / x² is a root of the monic equation obtained by dividing by x⁴, whose coefficients are polynomials in 1 / x, and whose derivative at y / x² is (2y + a₁x + a₃) / x². Bounding the different exponent by the order of these derivatives shows that every coefficient of (ω) is at most zero. Since (ω) has degree 2g - 2 = 0, it is zero.

Main results

All in the namespace WeierstrassCurve.Affine:

• kaehlerDifferentialEquivWeilDifferentialOfSeparating_invariantDifferential: the Kähler–Weil comparison sends ω to (2y + a₁x + a₃)⁻¹ · dx.
• weilDifferentialDivisor_invariantDifferential: the invariant differential has divisor zero.

References

• J. Silverman, The Arithmetic of Elliptic Curves, Proposition III.1.5.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.5.10 and Remark 4.3.7.

The local bound

The divisor of the invariant differential

theorem WeierstrassCurve.Affine.kaehlerDifferentialEquivWeilDifferentialOfSeparating_invariantDifferential {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : (TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating ⋯ ⋯ ⋯) W.invariantDifferential = W.invariantDifferentialDenom⁻¹ • TauCeti.weilDifferentialOfSeparating ⋯ ⋯

The invariant differential as a Weil differential: the Kähler–Weil comparison determined by the separating element x sends ω = dx / (2y + a₁x + a₃) to (2y + a₁x + a₃)⁻¹ · dx.

theorem WeierstrassCurve.Affine.kaehlerDifferentialEquivWeilDifferentialOfSeparating_invariantDifferential_ne_zero {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : ↑((TauCeti.kaehlerDifferentialEquivWeilDifferentialOfSeparating ⋯ ⋯ ⋯) W.invariantDifferential) ≠ 0

The Weil differential attached to the invariant differential is nonzero.

@[simp]

theorem WeierstrassCurve.Affine.weilDifferentialDivisor_invariantDifferential {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : TauCeti.weilDifferentialDivisor ⋯ ⋯ ⋯ ⋯ = 0

The invariant differential has divisor zero (Silverman, Proposition III.1.5): under the Kähler–Weil comparison determined by x, the invariant differential ω = dx / (2y + a₁x + a₃) of an elliptic curve is a Weil differential of F(W) / F with neither zeros nor poles.