The affine group-law formulae under a change of variables #
An admissible change of variables C : VariableChange R carries a point (x, y) of C • W to
the point (u²x + r, u³y + u²sx + t) of W. This file records what that substitution does to
each formula Mathlib's Affine/Formula.lean defines — negY, addX, negAddY, addY and
slope — to the two partial derivatives polynomialX and polynomialY, and to the two
predicates Equation and Nonsingular that cut the curve out.
Main statements #
WeierstrassCurve.Affine.variableChange_negY,_addX,_negAddY,_addY: each formula transforms by an explicit power ofu, together with the shear and translation the change of variables applies to the coordinate concerned.WeierstrassCurve.Affine.variableChange_evalEval_polynomialX,_polynomialY: the two partial derivatives transform by the matrix![![u⁴, -su³], ![0, u³]]— theY-partial simply scales byu³, while theX-partial scales byu⁴and is sheared by ans-multiple of theY-partial. Invertibility of that matrix is whatvariableChange_nonsingularruns on.WeierstrassCurve.Affine.variableChange_equation,_nonsingular:(x, y)lies onC • W, respectively is a smooth point of it, exactly when its image lies onW. Both are@[simp]. These are what make the change of variables carry points to points.WeierstrassCurve.Affine.variableChange_slope: the slope of the chord or tangent scales byuand translates bys.
Implementation notes #
The file is in two halves, split exactly where division starts. Everything except the slope is a
polynomial identity in the coefficients and the unit u, so it is stated over a commutative ring;
variableChange_slope is a quotient and needs a field.
Mathlib writes the coefficients of C • W with powers of u⁻¹. The five private
u_pow_mul_variableChange_aᵢ lemmas clear those denominators once, as uⁱ * (C • W).aᵢ = …, and
every identity in the first half is then a linear_combination of them which treats (C • W).aᵢ
as an atom and mentions no inverse at all. Multiplying an inverse away where it appears is what
needs a field; multiplying by u to cancel it does not.
The point-group isomorphism these identities are for is
WeierstrassCurve.Affine.Point.equivVariableChange, in Affine/Point/VariableChange.lean. The
split between the two files follows Mathlib's own: the formulae live in Affine/Formula.lean and
the point type in Affine/Point.lean, and nothing here mentions Point.
This is a prerequisite for TauCetiRoadmap/EllipticCurves/README.md §Layer 5's point isomorphism
for the quadratic twist.
Adapted from the FLT project (ImperialCollegeLondon/FLT,
FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean at the roadmap's pin
bc2fe8ff7396, FLT PR #1088, Apache 2.0). That file's own header reads
Authors: Michael Stoll, Claude. Following this repository's convention for adapted material, the
upstream authorship is credited here rather than in the copyright header. FLT states these
identities over a field, as part of the file that builds the point map; stating the polynomial
ones over a commutative ring, and separating them from the point map, is this repository's.
The polynomial identities #
Throughout, the change of variables carries a point (x, y) of C • W to the point
(u²x + r, u³y + u²sx + t) of W.
negY under the change of variables. The negation of the y-coordinate scales by u³
and picks up the same shear and translation the change of variables applies to y.
addX under the change of variables. The x-coordinate of a sum scales by u² and
translates by r, the same law the change of variables applies to any x.
negAddY under the change of variables, scaling by u³ with the shear and translation
of the y-coordinate.
addY under the change of variables, scaling by u³ with the shear and translation of
the y-coordinate, plus the shear applied to addX.
A point (x, y) lies on C • W if and only if (u²x + r, u³y + u²sx + t) lies on W: the
change of variables scales the Weierstrass polynomial by u⁶, and u is a unit.
polynomialY under the change of variables, scaling by u³. The Y-partial derivative
of the Weierstrass polynomial, evaluated at the image point, is u³ times the corresponding
derivative of C • W evaluated at the source point. This is the second row (0, u³) of the
matrix in variableChange_nonsingular below.
polynomialX under the change of variables, scaling by u⁴ and picking up a shear. The
X-partial derivative, evaluated at the image point, is u⁴ times the corresponding derivative
of C • W at the source point, minus s times the u³-scaled Y-partial there. That extra
shear term is the one asymmetry between the two derivative laws, and it makes this the first row
(u⁴, -su³) of the matrix in variableChange_nonsingular below.
Nonsingularity transfers across the change of variables. The two partial derivatives
transform by the matrix ![![u⁴, -su³], ![0, u³]] — the two lemmas just above — which is
invertible because u is, so W_X ≠ 0 ∨ W_Y ≠ 0 holds at the image exactly when it holds at the
source.
This is what lets the point map of Affine/Point/VariableChange.lean avoid [W.IsElliptic]:
equation_iff_nonsingular would supply nonsingularity from the equation, but only for an elliptic
curve, whereas carrying a point to a point needs no such hypothesis.
The slope #
The slope of the chord or tangent is a quotient, so this is the first statement that needs to divide, and the only one here that asks for a field.
The slope under the change of variables, scaling by u and translating by s — the law
the change of variables applies to a slope, as y scales by u³ and x by u². Stated for two
points of C • W on the curve, excluding the degenerate case x₁ = x₂ ∧ y₁ = negY x₂ y₂ —
where the two points are inverse to one another and the chord through them is vertical.