Abel–Jacobi gate: degree-zero divisor classes versus Weierstrass points #

Definition: WeierstrassCurve_GenusOnePic0 (5a1e5b22-326b-5b23-ac01-fa8e3f5a789f), by Claude, 2026-09-05.

Fix a field $F$ (with decidable equality) and an affine Weierstrass curve $W$ over $F$, and work with the function field W.FunctionField and with the places, divisors, degree, principal divisors and degree-zero class group AlgebraicCurve.Pic0 supplied by the project's divisor-class-group module (those notions are the project's own). Two assumptions are packaged as typeclasses carrying data or a theorem as fields. GenusOnePlaceGate W carries an explicit bijection pointEquivPlace : W.Point ≃ AlgebraicCurve.Place F W.FunctionField between the points of $W$ (with its Mathlib group structure) and the places of the function field, together with the field deg_eq_one asserting that every place has degree $1$; placeOfPoint is the forward map of this bijection, and the place attached to the origin plays the role of the place at infinity. AbelTheorem W is a Prop-valued class whose single field is Abel's theorem in the form: for every divisor $D$ of degree $0$, $D$ is principal if and only if divisorSum D = 0.

The remaining declarations are consequences. degree_eq_sum says that, all residue degrees being $1$, the degree of a divisor is the plain sum of its coefficients. divisorSum is the additive homomorphism from divisors to W.Point sending a single place $v$ with multiplicity $n$ to $n \cdot \mathrm{pointEquivPlace}^{-1}(v)$, i.e. the Abel–Jacobi sum $\sum_v n_v P_v$ computed in the group law of $W$. For a point $P$, pointDivisor P is the degree-zero divisor $(P) - (O)$ and pointClass P its class in Pic0. Given both gates, divisorSum descends along the quotient to pic0ToPoint : Pic0 →+ W.Point, which is shown surjective (using pointClass) and injective (using the converse direction of Abel's theorem), yielding the additive isomorphism genusOnePic0Equiv : Pic0 F W.FunctionField ≃+ W.Point with inverse $P \mapsto [(P) - (O)]$; pointClass_add records that $P \mapsto [(P)-(O)]$ is additive.

Relation to Mathlib. WeierstrassCurve.Affine, its point group W.Point and W.FunctionField are Mathlib's; the places, divisors, degree, principality and Pic0 used here come from the project's own algebraic-curve divisor module. Mathlib has no Abel–Jacobi identification of this kind, and neither the point–place dictionary nor Abel's theorem is proved here: both are hypotheses, stated as fields of the classes GenusOnePlaceGate and AbelTheorem.

Where it is used. The isomorphism $\operatorname{Pic}^0(F(W)/F) \simeq W(F)$ provides the dictionary between divisor classes on a genus-one curve and points of the associated Weierstrass model, used in the parts of the development that compare Jacobians of modular curves with elliptic curves and that count points on reductions via the action on degree-zero divisor classes.