The nonsingular points of a singular Weierstrass curve

Let W be a Weierstrass curve over a field F with a singular point (x₀, y₀) ∈ F². Its nonsingular points still form a group, Mathlib's W.toAffine.Point, and this file identifies that group with the additive or the multiplicative group of F (Silverman III.2.5).

Expanded at the singular point, the equation of W reads

(y - y₀)² + a₁ (x - x₀) (y - y₀) = (x - x₀)³ + (3 x₀ + a₂) (x - x₀)²

(WeierstrassCurve.Affine.equation_iff_of_isSingular), so the two tangent lines at (x₀, y₀) have slopes the roots of the tangent quadratic T² + a₁ T - (3 x₀ + a₂). Suppose that α ∈ F is a root; the other root is β = -a₁ - α, which is also in F.

• At a cusp, α = β, that is 2 α + a₁ = 0, and the equation reads u² = (x - x₀)³ with u = y - y₀ - α (x - x₀). The map (x, y) ↦ (x - x₀) / u, sending the point at infinity to 0, is an isomorphism W.toAffine.Point ≃+ F (WeierstrassCurve.Affine.Point.cuspAddEquiv).
• At a split node, α ≠ β, and the equation reads u w = (x - x₀)³ with w = y - y₀ - β (x - x₀). The map (x, y) ↦ u / w, sending the point at infinity to 1, is an isomorphism W.toAffine.Point ≃+ Additive Fˣ (WeierstrassCurve.Affine.Point.nodeAddEquiv).

In both cases three points add to zero exactly when they lie on a line, and the line u = m (x - x₀) + c meets the curve where the parameter t = (x - x₀) / u, respectively s = u / w, satisfies a cubic whose roots sum to 0, respectively multiply to 1. The proofs below verify this on Mathlib's chord-and-tangent formulas after moving the singular point to the origin by a change of variables.

When the tangent quadratic has no root in F, the singular point is a nonsplit node, or, over an imperfect field of characteristic 2, a cusp whose tangent is not defined over F. The group of nonsingular points is then a twisted form of Fˣ or of F, and these cases are not treated here.

As a consequence, for n invertible in F the number of n-torsion points among the nonsingular points divides n (WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_isSingular), since F has no such torsion and the n-th roots of unity in Fˣ form a cyclic group of order dividing n. Passing to an algebraic closure, where every singular point has rational tangent slopes, this holds for every Weierstrass curve with vanishing discriminant over any field (WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_Δ_eq_zero). In the proof of the criterion of Néron, Ogg and Shafarevich (Silverman VII.7.1) this bound, applied to the reduced curve, excludes bad reduction when the torsion of order prime to the residue characteristic is unramified. When moreover c₄ = 0, the singular point is a cusp, since c₄ = (2 α + a₁) ^ 4 for a tangent slope α (WeierstrassCurve.Affine.c₄_eq_of_isSingular), and there is no such torsion at all (WeierstrassCurve.Affine.Point.torsionBy_eq_bot_of_Δ_eq_zero_of_c₄_eq_zero). Applied to the reduced curve, this is what makes the points with nonsingular reduction at additive reduction free of torsion prime to the residue characteristic.

Main definitions

• WeierstrassCurve.Affine.Point.cuspAddEquiv: at a cusp with tangent slope α ∈ F, the isomorphism W.toAffine.Point ≃+ F.
• WeierstrassCurve.Affine.Point.nodeAddEquiv: at a node with tangent slopes in F, the isomorphism W.toAffine.Point ≃+ Additive Fˣ.

Main results

• WeierstrassCurve.Affine.Point.cuspAddEquiv_some and WeierstrassCurve.Affine.Point.val_toMul_nodeAddEquiv_some: the coordinate formulas.
• WeierstrassCurve.Affine.Point.cuspAddEquiv_symm_of_ne_zero and WeierstrassCurve.Affine.Point.nodeAddEquiv_symm_of_ne_one: the points with a given parameter.
• WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_isSingular: when the tangent slopes at a singular point lie in F, the number of n-torsion points divides n, for n invertible in F.
• WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_Δ_eq_zero: the same divisibility over any field whenever Δ = 0.
• WeierstrassCurve.Affine.Point.torsionBy_eq_bot_of_Δ_eq_zero_of_c₄_eq_zero: over any field, if Δ = 0 and c₄ = 0 then the n-torsion is trivial, for n invertible in F.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.2.5 and VII.7.1.

Models singular at the origin

The cusp

The split node

An arbitrary singular point

def WeierstrassCurve.Affine.Point.cuspAddEquiv {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hc : 2 * α + W.a₁ = 0) : W.toAffine.Point ≃+ F

The nonsingular points at a cusp form the additive group (Silverman III.2.5). If (x₀, y₀) is a singular point of W whose tangent quadratic T² + a₁ T - (3 x₀ + a₂) has the double root α ∈ F, so that 2 α + a₁ = 0, then (x, y) ↦ (x - x₀) / (y - y₀ - α (x - x₀)), with the point at infinity sent to 0, is a group isomorphism W.toAffine.Point ≃+ F.

@[simp]

theorem WeierstrassCurve.Affine.Point.cuspAddEquiv_some {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hc : 2 * α + W.a₁ = 0) {x y : F} (hxy : W.toAffine.Nonsingular x y) : (cuspAddEquiv h hα hc) (some x y hxy) = (x - x₀) / (y - y₀ - α * (x - x₀))

The coordinate formula for cuspAddEquiv.

@[simp]

theorem WeierstrassCurve.Affine.Point.cuspAddEquiv_symm_of_ne_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hc : 2 * α + W.a₁ = 0) {t : F} (ht : t ≠ 0) : (cuspAddEquiv h hα hc).symm t = some (x₀ + 1 / t ^ 2) (y₀ + (1 / t ^ 3 + α / t ^ 2)) ⋯

The inverse of cuspAddEquiv sends a parameter t ≠ 0 to the point (x₀ + 1 / t², y₀ + (1 / t³ + α / t²)).

def WeierstrassCurve.Affine.Point.nodeAddEquiv {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hn : 2 * α + W.a₁ ≠ 0) : W.toAffine.Point ≃+ Additive Fˣ

The nonsingular points at a split node form the multiplicative group (Silverman III.2.5). If (x₀, y₀) is a singular point of W whose tangent quadratic T² + a₁ T - (3 x₀ + a₂) has the two distinct roots α and -a₁ - α in F, so that 2 α + a₁ ≠ 0, then (x, y) ↦ (y - y₀ - α (x - x₀)) / (y - y₀ + (a₁ + α) (x - x₀)), with the point at infinity sent to 1, is a group isomorphism W.toAffine.Point ≃+ Additive Fˣ.

@[simp]

theorem WeierstrassCurve.Affine.Point.val_toMul_nodeAddEquiv_some {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hn : 2 * α + W.a₁ ≠ 0) {x y : F} (hxy : W.toAffine.Nonsingular x y) : ↑(Additive.toMul ((nodeAddEquiv h hα hn) (some x y hxy))) = (y - y₀ - α * (x - x₀)) / (y - y₀ + (W.a₁ + α) * (x - x₀))

The coordinate formula for nodeAddEquiv.

@[simp]

theorem WeierstrassCurve.Affine.Point.nodeAddEquiv_symm_of_ne_one {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) (hn : 2 * α + W.a₁ ≠ 0) {s : Additive Fˣ} (hs : ↑(Additive.toMul s) ≠ 1) : (nodeAddEquiv h hα hn).symm s = some (x₀ + (2 * α + W.a₁) ^ 2 * ↑(Additive.toMul s) / (↑(Additive.toMul s) - 1) ^ 2) (y₀ + (-(2 * α + W.a₁) ^ 3 * ↑(Additive.toMul s) ^ 2 / (↑(Additive.toMul s) - 1) ^ 3 + α * ((2 * α + W.a₁) ^ 2 * ↑(Additive.toMul s) / (↑(Additive.toMul s) - 1) ^ 2))) ⋯

The inverse of nodeAddEquiv sends a parameter s ≠ 1 to the point (x₀ + D² s / (s - 1)², y₀ + (-D³ s² / (s - 1)³ + α D² s / (s - 1)²)), where D = 2 α + a₁.

theorem WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_isSingular {F : Type u_1} [Field F] {W : WeierstrassCurve F} {α x₀ y₀ : F} [DecidableEq F] (h : W.toAffine.IsSingular x₀ y₀) (hα : α ^ 2 + W.a₁ * α - (3 * x₀ + W.a₂) = 0) {n : ℕ} (hn : ↑n ≠ 0) : Nat.card ↥(AddSubgroup.torsionBy W.toAffine.Point ↑n) ∣ n

Torsion at a singular point with rational tangents. If (x₀, y₀) is a singular point of W at which the tangent slopes lie in F, then for n invertible in F the number of n-torsion points divides n: the n-torsion is trivial at a cusp, and a subgroup of the n-th roots of unity at a split node.

theorem WeierstrassCurve.Affine.Point.natCard_torsionBy_dvd_of_Δ_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [DecidableEq F] (hΔ : W.Δ = 0) {n : ℕ} (hn : ↑n ≠ 0) : Nat.card ↥(AddSubgroup.torsionBy W.toAffine.Point ↑n) ∣ n

Torsion of a singular cubic. If Δ = 0, then for n invertible in F the number of n-torsion points among the nonsingular points divides n. In particular the n-torsion is not (ℤ / n)² for n > 1, unlike the n-torsion of an elliptic curve.

theorem WeierstrassCurve.Affine.Point.torsionBy_eq_bot_of_Δ_eq_zero_of_c₄_eq_zero {F : Type u_1} [Field F] {W : WeierstrassCurve F} [DecidableEq F] (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) {n : ℕ} (hn : ↑n ≠ 0) : AddSubgroup.torsionBy W.toAffine.Point ↑n = ⊥

A cuspidal cubic has no torsion prime to the characteristic. If Δ = 0 and c₄ = 0, the singular point is a cusp, and for n invertible in F the only nonsingular point killed by n is the point at infinity. Over an algebraic closure the nonsingular points of a cusp form the additive group of the field (Silverman III.2.5), which has no n-torsion.