Definitions/Def_WeierstrassCurve_VeluOrderTwoShortNF.lean

Throughout, R is a commutative ring and W a Weierstrass curve over R satisfying Mathlib's IsShortNF, i.e. a_1 = a_2 = a_3 = 0, so that W is y^2 = x^3 + a_4 x + a_6. The module specialises the order-two Vélu data of the project to this presentation. Since the general definitions read \mathrm{veluGx}(x,y) = 3x^2 + 2a_2 x + a_4 - a_1 y and \mathrm{veluGy}(x,y) = -(2y + a_1 x + a_3), one obtains \mathrm{veluGx}(x,y) = 3x^2 + a_4 for all x,y and \mathrm{veluGy}(x,0) = 0; and since \mathrm{velu2QuadDisc}(x_0) = b_2^2 - 8 b_2 x_0 - 48 x_0^2 - 32 b_4, with b_2 = 0 and b_4 = 2a_4 this becomes -16\,(3x_0^2 + 4a_4). A further lemma records that a point of the form (e,0) satisfies the affine Weierstrass equation of W exactly when e^3 + a_4 e + a_6 = 0, and an instance records that any curve presented as \langle 0,0,0,a,b\rangle is in short normal form.

The second half treats the curve \mathrm{veluQuotient2}(x_0,y_0), defined in general by keeping a_1, a_2, a_3 and setting a_4' = a_4 - 5\,\mathrm{veluGx}(x_0,y_0), a_6' = a_6 - b_2\,\mathrm{veluGx}(x_0,y_0) - 7 x_0\,\mathrm{veluGx}(x_0,y_0). An instance shows this quotient is again in short normal form, and the coefficients at a point (e,0) are computed: a_4' = -(15e^2 + 4a_4) and a_6' = a_6 - 21e^3 - 7 a_4 e. The final theorem packages these as an equality of Weierstrass curves, \mathrm{veluQuotient2}(e,0) = \langle 0,0,0,\,-(15e^2+4a_4),\;a_6 - 21e^3 - 7a_4 e\rangle . No hypothesis that (e,0) lies on W, or that e is a root of the cubic, is imposed for these identities: they are polynomial identities in e and the coefficients of W.