Function field of a Weierstrass curve over F(x) #
Definition: WeierstrassCurve_FunctionFieldQuadratic (4002f263-afc3-568e-bdcd-dc58468b3d3a), by
Claude, 2026-09-05.
Fix a field $F$ and an affine Weierstrass curve $W : y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6$
over $F$, with its coordinate ring W.CoordinateRing $= F[x,y]/(W)$ and function field
W.FunctionField, the fraction field of that ring. The module sets up the tower $F \subset F(x) \subset F(W)$ and exhibits $F(W)$ as generated by a root of a monic quadratic over $F(x)$. First,
polyToFunctionField W : F[X] →+* W.FunctionField is the composite of the structure maps $F[X] \to$
W.CoordinateRing $\to$ W.FunctionField; it is shown to be injective (using that the coordinate
ring is free over $F[X]$ on the basis $\{1, y\}$), to send a constant $C c$ to the image of $c$, to
send nonzero polynomials to nonzero elements, and to agree with the canonical algebra map $F[X] \to$
W.FunctionField; auxiliary lemmas compute the images of $p \cdot 1$ and $p \cdot 1 + q\,y$ in
terms of it, and record that the image of $y$ is nonzero. Since $F[X] \to F(W)$ is injective and
$F(x) =$ RatFunc F is the fraction field of $F[X]$, it extends to ratFuncToFunctionField W : RatFunc F →+* W.FunctionField, which is installed as an $F(x)$-algebra structure on $F(W)$
compatible with the $F[X]$- and $F$-algebra structures. Next, yCoord W is the image of $y$ in
$F(W)$, and weierstrassQuadratic W is the polynomial $T^2 + \bigl((a_1x+a_3)T - (x^3+a_2x^2+a_4x+a_6)\bigr)$ over $F(x)$, whose coefficients are images of polynomials in $x$. The
remaining results show that the non-leading part has degree $< 2$, hence that this quadratic is
monic, that yCoord W satisfies the Weierstrass relation $y^2 = (x^3+a_2x^2+a_4x+a_6) - (a_1x+a_3)y$ in $F(W)$, that it is therefore a root of weierstrassQuadratic W, and consequently
that yCoord W is integral over $F(x)$.
Relation to Mathlib. Everything is built directly on Mathlib's
WeierstrassCurve.Affine.CoordinateRing and WeierstrassCurve.Affine.FunctionField, including the
$F[X]$-basis $\{1, y\}$ of the coordinate ring. The $F(x)$-algebra structure on the function field,
the associated scalar-tower instances, and the coordinate function yCoord with its quadratic
equation over $F(x)$ are additions to that Mathlib material.
Where it is used. These definitions are the basic dictionary for working with rational functions on a Weierstrass curve: they present $F(W)$ as a degree-two extension of the rational function field $F(x)$ generated by $y$. Downstream they support the study of principal divisors on $F(W)$, the place at infinity, and function-field comparisons between curves linked by isogenies, within the elliptic-curve input to the proof.
<!-- Generated by add_prove2me_provenance.py -->
The map from polynomials in the x-coordinate to the curve's function field.
Equations
- W.polyToFunctionField = (algebraMap W.CoordinateRing W.FunctionField).comp (algebraMap (Polynomial F) W.CoordinateRing)
Instances For
The embedding of rational functions in the x-coordinate into the curve's function field.
Equations
Instances For
The image of the y-coordinate in the curve's function field.
Equations
Instances For
The monic quadratic in the y-coordinate over the rational function field obtained from the Weierstrass equation.
Equations
- One or more equations did not get rendered due to their size.