Weil functions and a point-level Weil pairing constant #
Definition: EllipticCurve_WeilPairingFun (1bf92a85-c3e9-5b97-802c-d79bf412e655), by Claude,
2026-09-05.
Throughout, $W$ is a Weierstrass curve over a field $R$ and $K$ is a field equipped with an
$R$-algebra structure; $(W⁄K)$ denotes the base-changed affine curve, with its coordinate ring
$(W⁄K)$.CoordinateRing, its function field $(W⁄K)$.FunctionField and its group of points
$(W⁄K)$.Point. For a point $P$, placeIdeal W K P is the unit ideal when $P = 0$ and otherwise
the underlying ideal of the height-one place placeOf W K P, namely the maximal ideal $(x - x_P,,y
- y_P)$ of the coordinate ring cut out by the affine point $P$; the two accompanying lemmas record
these two cases. For $n \in \mathbb{Z}$ and a point $Q$,
fibSet W K n Qis the set $\{P : n \cdot P = Q\}$, with membership unfolding by definition, andfibIdeal W K n Qis the product ofplaceIdeal W K Pover that set when it is finite (the finite set being taken in the sense ofSet.Finite.toFinset), and the unit ideal otherwise.weilNum W K n Tis a chosen generator offibIdeal W K n Twhen that ideal is principal, and $1$ otherwise;span_weilNumstates that under principality the span of this element is the ideal. The Weil functionweilFun W K n Tis then the quotient, in the function field, of the images ofweilNum W K n TandweilNum W K n 0.
Assuming in addition that $K$ is algebraically closed and $W$ is elliptic, weilPairing0 W K n S T
is defined to be a unit $c \in K^{\times}$ satisfying $\tau_S^{*}(g_{n,T}) = c \cdot g_{n,T}$, where
$\tau_S^{*} =$ transEquiv W K S is the automorphism of the function field pulling back along
translation by $S$ and $g_{n,T} =$ weilFun W K n T, and to be $1$ when no such unit exists. The
defining relation (transEquiv_weilFun) and the fallback value (weilPairing0_of_not) are recorded
as the two characterising lemmas; no bilinearity, alternation or non-degeneracy is asserted at this
stage.
Relation to Mathlib. Mathlib supplies the affine coordinate ring of a Weierstrass curve, its
ideals XYIdeal/XClass/YClass and the group of affine points; the places attached to points,
the translation automorphisms of the function field, and the Weil functions and pairing constant
defined here are the project's own, Mathlib having no Weil pairing.
Where it is used. These Weil functions and the constant $e_0$ attached to a pair of points are the basis for the project's treatment of the Weil pairing on $n$-torsion, whose bilinearity, alternation and Galois equivariance give the determinant of the mod-$n$ representation attached to an elliptic curve as the cyclotomic character.
<!-- Generated by add_prove2me_provenance.py -->
The coordinate-ring ideal of a nonzero point, with the unit ideal at infinity.
Equations
- WeierstrassCurve.Affine.placeIdeal W K P = if hP : P = 0 then ⊤ else (WeierstrassCurve.Affine.placeOf W K P hP).asIdeal
Instances For
The set of points mapped to Q by multiplication by the integer n.
Equations
- WeierstrassCurve.Affine.fibSet W K n Q = {P : (WeierstrassCurve.Affine.baseChange W K).Point | n • P = Q}
Instances For
The product of point ideals over the multiplication fiber, or the unit ideal if the fiber is infinite.
Equations
- WeierstrassCurve.Affine.fibIdeal W K n Q = if h : (WeierstrassCurve.Affine.fibSet W K n Q).Finite then ∏ P ∈ h.toFinset, WeierstrassCurve.Affine.placeIdeal W K P else ⊤
Instances For
A chosen generator of the fiber ideal when it is principal, and one otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ratio of fiber-ideal generators over T and over zero, as a function-field element.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit scaling weilFun n T under translation by S, if one exists; otherwise one.
Equations
- One or more equations did not get rendered due to their size.