Denominator-free affine doubling coordinates

For a Weierstrass curve over ℚ, this file records compact homogeneous numerators for the abscissa and completed ordinate of an affine double. The formulas are proved directly from the chord-and-tangent law and are designed for composition with explicit rational maps.

def MazurTorsion.Doubling.completedCubic (W : WeierstrassCurve ℚ) (x : ℚ) : ℚ

The completed-square cubic, equal on the curve to (2y + a₁x + a₃)².

Equations

• MazurTorsion.Doubling.completedCubic W x = 4 * x ^ 3 + W.b₂ * x ^ 2 + 2 * W.b₄ * x + W.b₆

def MazurTorsion.Doubling.xNumerator (W : WeierstrassCurve ℚ) (x : ℚ) : ℚ

The numerator of the affine doubling abscissa over completedCubic.

Equations

• MazurTorsion.Doubling.xNumerator W x = x ^ 4 - W.b₄ * x ^ 2 - 2 * W.b₆ * x - W.b₈

def MazurTorsion.Doubling.completedYNumerator (W : WeierstrassCurve ℚ) (x : ℚ) : ℚ

The numerator of the completed ordinate of the affine double over the cube of the source completed ordinate.

Equations

• One or more equations did not get rendered due to their size.

def MazurTorsion.Doubling.xNumeratorHomogeneous {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (u v : R) : R

Homogenization of xNumerator to degree four.

Equations

• MazurTorsion.Doubling.xNumeratorHomogeneous W u v = u ^ 4 - W.b₄ * u ^ 2 * v ^ 2 - 2 * W.b₆ * u * v ^ 3 - W.b₈ * v ^ 4

def MazurTorsion.Doubling.completedYNumeratorHomogeneous {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (u v : R) : R

Homogenization of completedYNumerator to degree six.

Equations

• One or more equations did not get rendered due to their size.

def MazurTorsion.Doubling.completedCubicHomogeneous {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (u v : R) : R

Homogenization of completedCubic to degree three.

Equations

• MazurTorsion.Doubling.completedCubicHomogeneous W u v = 4 * u ^ 3 + W.b₂ * u ^ 2 * v + 2 * W.b₄ * u * v ^ 2 + W.b₆ * v ^ 3

def MazurTorsion.Doubling.completedCubicHomogeneousDirectional (W : WeierstrassCurve ℚ) (u v du dv : ℚ) : ℚ

Directional derivative of completedCubicHomogeneous at (u, v) in the direction (du, dv).

Equations

• MazurTorsion.Doubling.completedCubicHomogeneousDirectional W u v du dv = (12 * u ^ 2 + 2 * W.b₂ * u * v + 2 * W.b₄ * v ^ 2) * du + (W.b₂ * u ^ 2 + 4 * W.b₄ * u * v + 3 * W.b₆ * v ^ 2) * dv

def MazurTorsion.Doubling.xNumeratorHomogeneousDirectional (W : WeierstrassCurve ℚ) (u v du dv : ℚ) : ℚ

Directional derivative of xNumeratorHomogeneous at (u, v) in the direction (du, dv).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MazurTorsion.Doubling.xNumeratorHomogeneous_at_one (W : WeierstrassCurve ℚ) (x : ℚ) : xNumeratorHomogeneous W x 1 = xNumerator W x

@[simp]

theorem MazurTorsion.Doubling.completedYNumeratorHomogeneous_at_one (W : WeierstrassCurve ℚ) (x : ℚ) : completedYNumeratorHomogeneous W x 1 = completedYNumerator W x

@[simp]

theorem MazurTorsion.Doubling.completedCubicHomogeneous_at_one (W : WeierstrassCurve ℚ) (x : ℚ) : completedCubicHomogeneous W x 1 = completedCubic W x

theorem MazurTorsion.Doubling.xNumeratorHomogeneous_directional (W : WeierstrassCurve ℚ) (u v du dv : ℚ) : xNumeratorHomogeneousDirectional W u v du dv * v * completedCubicHomogeneous W u v - xNumeratorHomogeneous W u v * (dv * completedCubicHomogeneous W u v + v * completedCubicHomogeneousDirectional W u v du dv) = 2 * completedYNumeratorHomogeneous W u v * (du * v - u * dv)

The directional numerator identity for tangent doubling. Equivalently, the derivative of xNumeratorHomogeneous / (v * completedCubicHomogeneous) has numerator 2 * completedYNumeratorHomogeneous.

theorem MazurTorsion.Doubling.completedCubic_eq_completedY_sq (W : WeierstrassCurve ℚ) {x y : ℚ} (h : W.toAffine.Equation x y) : completedCubic W x = (2 * y + W.a₁ * x + W.a₃) ^ 2

The completed-square cubic equals the square of the completed ordinate on the affine curve.

theorem MazurTorsion.Doubling.addX_self_mul_completedCubic (W : WeierstrassCurve ℚ) {x y : ℚ} (h : W.toAffine.Equation x y) (hv : 2 * y + W.a₁ * x + W.a₃ ≠ 0) : W.toAffine.addX x x (W.toAffine.slope x x y y) * completedCubic W x = xNumerator W x

The tangent-law doubling abscissa times the completed-square cubic is the denominator-free numerator xNumerator.

theorem MazurTorsion.Doubling.completedY_add_self (W : WeierstrassCurve ℚ) {x y : ℚ} (h : W.toAffine.Equation x y) (hv : 2 * y + W.a₁ * x + W.a₃ ≠ 0) : (2 * y + W.a₁ * x + W.a₃) ^ 3 * (2 * W.toAffine.addY x x y (W.toAffine.slope x x y y) + W.a₁ * W.toAffine.addX x x (W.toAffine.slope x x y y) + W.a₃) = completedYNumerator W x

The completed ordinate of an affine double, multiplied by the cube of the source completed ordinate, is completedYNumerator.