The 2-torsion of the group of points of a Weierstrass curve

Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal form over a field K. In that normal form negation is -(x, y) = (x, -y), so a point is its own negative exactly when y = 0, and the 2-torsion of W(K) is the origin together with the points (x, 0) at the roots of f.

The counting statement card_ker_nsmul_two is what turns a root count into a torsion count. It is one side of the archimedean local-image formula of explicit 2-descent, which reads #(im μ_v) = #E(ℝ)[2] / 2 at a real place.

Main statements

• WeierstrassCurve.Affine.card_ker_nsmul_two: #W(K)[2] is the number of roots of f in K, plus one for the origin.

Provenance

Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/WeakMordellWeil.lean lines 806-868 — the 2-torsion section, which sits after the range that TauCeti/AlgebraicGeometry/EllipticCurve/MordellWeil/XSubT.lean ported.

This advances TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (README:813-820), whose "Explicit 2-descent (core, this layer)" bullet names the local conditions and the rank bound; the archimedean local-image count needs this torsion count.

theorem WeierstrassCurve.Affine.card_ker_nsmul_two {K : Type u_1} [Field K] (W : Affine K) [IsCharNeTwoNF W] [WeierstrassCurve.IsElliptic W] [DecidableEq K] : Nat.card ↥(nsmulAddMonoidHom 2).ker = Nat.card { x : K // Polynomial.eval x W.f = 0 } + 1

The 2-torsion of W(K) has one more element than f has roots in K.

The underlying reason is that the 2-torsion is the origin together with the points (x, 0) at the roots of f; that set equality is established inside the proof, but only the cardinality is exported, because that is all the archimedean local-image count consumes. A caller needing the identification itself should ask for it as its own theorem.