The $x - e$ Kummer map is a homomorphism

Proved

BSD.exists_kummer_hom

by korbonits · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

bsdelliptic-curvesnumber-theory

Let $F$ be a field with $2 \neq 0$ , let $E$ be an elliptic curve over $F$ given by a Weierstrass equation, and let $e \in F$ be a root of the 2-torsion polynomial $\psi_2(x) = 4x^3 + b_2x^2 + 2b_4x + b_6$ (so $T = (e, \ast)$ is a rational 2-torsion point). Then there is a group homomorphism $\delta : E(F) \to F^\times/(F^\times)^2$ such that $\delta(x, y) = (x - e) \bmod (F^\times)^2$ for every affine point with $x \neq e$ .

This is the connecting homomorphism for the 2-isogeny with kernel $\langle T \rangle$ . The key identity is that for three collinear points of $E$ the product of their values of $x - e$ is a square. At $T$ itself, $\delta$ takes the value obtained by continuity, $\psi_2'(e)/4$ .

Preamble

import Mathlib

Formal statement

namespace BSD
theorem exists_kummer_hom {F : Type*} [Field F] [DecidableEq F] (h2 : (2 : F) ≠ 0)
    (W : WeierstrassCurve F) [W.IsElliptic] (e : F) (he : W.twoTorsionPolynomial.toPoly.IsRoot e) :
    ∃ δ : W.toAffine.Point →+ Additive (Fˣ ⧸ (powMonoidHom 2 : Fˣ →* Fˣ).range),
      ∀ (x y : F) (h : W.toAffine.Nonsingular x y) (hx : x - e ≠ 0),
        δ (.some x y h) = Additive.ofMul (QuotientGroup.mk (Units.mk0 (x - e) hx)) := by sorry
end BSD

Source

Silverman, The Arithmetic of Elliptic Curves (2nd ed.), Ch. X, Prop. 1.4 and Ch. VIII, Prop. 1.5–1.6 (proof of the weak Mordell–Weil theorem via the Kummer pairing, full 2-torsion case)

View graph

The x−ex - ex−e Kummer map is a homomorphism

The $x - e$ Kummer map is a homomorphism