Derivations and the addition law on a Weierstrass curve

Let W be a Weierstrass curve over R, let K be an R-algebra and let D : Derivation R K M be a derivation on K over R. Writing W_X and W_Y for the partial derivatives polynomialX and polynomialY of the Weierstrass polynomial, this file records how D interacts with the points of W⁄K and with the formulae of the addition law.

Main statements

• Equation.evalEval_polynomialX_smul_add_evalEval_polynomialY_smul_eq_zero (in the namespace WeierstrassCurve.Affine): at a point (x, y) of W⁄K, W_X(x, y) • D x + W_Y(x, y) • D y = 0, the differential of the Weierstrass equation, over any commutative ring K.
• WeierstrassCurve.Affine.derivation_evalEval_polynomialX, WeierstrassCurve.Affine.derivation_evalEval_polynomialY and WeierstrassCurve.Affine.derivation_addX: the chain rule for W_X, W_Y and addX.
• WeierstrassCurve.Affine.Equation.derivation_Y_eq_smul_derivation_X: over a field, at a point where W_Y does not vanish, D y = (-W_X(x, y) / W_Y(x, y)) • D x.
• WeierstrassCurve.Affine.derivation_slope_of_X_ne and WeierstrassCurve.Affine.derivation_slope_self_of_Y_ne: the chain rule for the chord and the tangent slope.
• WeierstrassCurve.Affine.derivation_addX_slope: if (x₃, y₃) is the sum of two points (x₁, y₁) and (x₂, y₂) of W⁄K at which W_Y does not vanish (when x₁ ≠ x₂), then D x₃ = W_Y(x₃, y₃) • (W_Y(x₁, y₁)⁻¹ • D x₁ + W_Y(x₂, y₂)⁻¹ • D x₂); when W_Y(x₃, y₃) is nonzero as well, WeierstrassCurve.Affine.inv_smul_derivation_addX_slope divides by it: W_Y(x₃, y₃)⁻¹ • D x₃ = W_Y(x₁, y₁)⁻¹ • D x₁ + W_Y(x₂, y₂)⁻¹ • D x₂.

The last two identities are the additivity of the differential dx / W_Y, with and without the denominator at the sum cleared. On an elliptic curve dx / W_Y is the invariant differential, and the identity is the computation behind the additivity of its pullback along a sum of morphisms (Silverman, The Arithmetic of Elliptic Curves, III.5.2); the version for two points of W⁄K and their sum is in Affine/Point/Derivation.lean. Everything is stated for an arbitrary derivation, so that it applies to the Kähler differentials of a function field without any further hypothesis.

Provenance

The identity for two points with distinct x-coordinates generalises the computation kaehlerD_addPullback_x_eq_one_add_smul_omega of HasseWeil/RouteBGeneral.lean in AINTLIB (commit 513e83879e2f8cbc626eb9e04d660e92be16ccba, Apache 2.0), where the first point is the generic point of the curve and the second its image under an endomorphism, from the Kähler differential to an arbitrary derivation.

Two formulae, and the coefficient identities

The coefficient identities are between elements of the base field: they are the coefficients of D x₁ and D x₂ in the derivation of the sum's x-coordinate, computed by the chain rule from the addition formulae, compared with the coefficients in derivation_addX_slope.

theorem WeierstrassCurve.Affine.sub_negY {K : Type u_1} [CommRing K] (W : Affine K) (x y : K) : y - W.negY x y = Polynomial.evalEval x y W.polynomialY

The difference between a point and its negative is W_Y: y - negY x y = W_Y(x, y).

theorem WeierstrassCurve.Affine.evalEval_polynomialY_ne_zero_of_Y_ne {K : Type u_1} [CommRing K] (W : Affine K) {x y : K} (hy : y ≠ W.negY x y) : Polynomial.evalEval x y W.polynomialY ≠ 0

W_Y does not vanish at a point which is not its own negative.

Derivations at the points of a base change

theorem WeierstrassCurve.Affine.Equation.evalEval_polynomialX_smul_add_evalEval_polynomialY_smul_eq_zero {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) {x y : K} (h : (toAffine (Affine.baseChange W K)).Equation x y) : Polynomial.evalEval x y (toAffine (Affine.baseChange W K)).polynomialX • D x + Polynomial.evalEval x y (toAffine (Affine.baseChange W K)).polynomialY • D y = 0

The differential of the Weierstrass equation. At a point (x, y) of W⁄K, every derivation D on K over R satisfies W_X(x, y) • D x + W_Y(x, y) • D y = 0.

@[simp]

theorem WeierstrassCurve.Affine.derivation_evalEval_polynomialX {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) (x y : K) : D (Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialX) = (toAffine (baseChange W K)).a₁ • D y - (6 * x + 2 * (toAffine (baseChange W K)).a₂) • D x

The chain rule for W_X: D (W_X(x, y)) = a₁ • D y - (6x + 2a₂) • D x.

@[simp]

theorem WeierstrassCurve.Affine.derivation_evalEval_polynomialY {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) (x y : K) : D (Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialY) = 2 • D y + (toAffine (baseChange W K)).a₁ • D x

The chain rule for W_Y: D (W_Y(x, y)) = 2 • D y + a₁ • D x.

theorem WeierstrassCurve.Affine.derivation_addX {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] (W : WeierstrassCurve R) (D : Derivation R K M) (x₁ x₂ ℓ : K) : D ((toAffine (baseChange W K)).addX x₁ x₂ ℓ) = (2 * ℓ + (toAffine (baseChange W K)).a₁) • D ℓ - D x₁ - D x₂

The chain rule for addX: D (addX x₁ x₂ ℓ) = (2ℓ + a₁) • D ℓ - D x₁ - D x₂.

theorem WeierstrassCurve.Affine.Equation.derivation_Y_eq_smul_derivation_X {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) {x y : K} (h : (toAffine (Affine.baseChange W K)).Equation x y) (hu : Polynomial.evalEval x y (toAffine (Affine.baseChange W K)).polynomialY ≠ 0) : D y = (-Polynomial.evalEval x y (toAffine (Affine.baseChange W K)).polynomialX / Polynomial.evalEval x y (toAffine (Affine.baseChange W K)).polynomialY) • D x

The derivation of the y-coordinate is determined by that of the x-coordinate: at a point of W⁄K where W_Y does not vanish, D y = (-W_X(x, y) / W_Y(x, y)) • D x.

theorem WeierstrassCurve.Affine.derivation_slope_of_X_ne {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {x₁ x₂ y₁ y₂ : K} (hx : x₁ ≠ x₂) : D ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂) = (x₁ - x₂)⁻¹ ^ 2 • ((x₁ - x₂) • (D y₁ - D y₂) - (y₁ - y₂) • (D x₁ - D x₂))

The chain rule for the chord slope: for x₁ ≠ x₂, D ℓ = (x₁ - x₂)⁻² • ((x₁ - x₂) • (D y₁ - D y₂) - (y₁ - y₂) • (D x₁ - D x₂)).

theorem WeierstrassCurve.Affine.derivation_slope_self_of_Y_ne {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {x y : K} (hy : y ≠ (toAffine (baseChange W K)).negY x y) : D ((toAffine (baseChange W K)).slope x x y y) = (Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialY)⁻¹ ^ 2 • (Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialY • D (-Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialX) - -Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialX • D (Polynomial.evalEval x y (toAffine (baseChange W K)).polynomialY))

The chain rule for the tangent slope -W_X / W_Y at a point which is not its own negative.

theorem WeierstrassCurve.Affine.derivation_addX_slope {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {x₁ x₂ y₁ y₂ : K} (h₁ : (toAffine (baseChange W K)).Equation x₁ y₁) (h₂ : (toAffine (baseChange W K)).Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (toAffine (baseChange W K)).negY x₂ y₂)) (hu₁ : x₁ ≠ x₂ → Polynomial.evalEval x₁ y₁ (toAffine (baseChange W K)).polynomialY ≠ 0) (hu₂ : x₁ ≠ x₂ → Polynomial.evalEval x₂ y₂ (toAffine (baseChange W K)).polynomialY ≠ 0) : D ((toAffine (baseChange W K)).addX x₁ x₂ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) = Polynomial.evalEval ((toAffine (baseChange W K)).addX x₁ x₂ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) ((toAffine (baseChange W K)).addY x₁ x₂ y₁ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) (toAffine (baseChange W K)).polynomialY • ((Polynomial.evalEval x₁ y₁ (toAffine (baseChange W K)).polynomialY)⁻¹ • D x₁ + (Polynomial.evalEval x₂ y₂ (toAffine (baseChange W K)).polynomialY)⁻¹ • D x₂)

The derivation of the x-coordinate of a sum of points. Let (x₁, y₁) and (x₂, y₂) be points of W⁄K whose sum (x₃, y₃) is affine, at both of which W_Y = 2Y + a₁X + a₃ does not vanish when x₁ ≠ x₂ (in the tangent case x₁ = x₂ it cannot vanish). Then every derivation D on K over R satisfies D x₃ = W_Y(x₃, y₃) • (W_Y(x₁, y₁)⁻¹ • D x₁ + W_Y(x₂, y₂)⁻¹ • D x₂), the additivity of the differential dx / W_Y with the denominator at the sum cleared.

theorem WeierstrassCurve.Affine.inv_smul_derivation_addX_slope {R : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup M] [Module R M] [Module K M] {W : WeierstrassCurve R} (D : Derivation R K M) [DecidableEq K] {x₁ x₂ y₁ y₂ : K} (h₁ : (toAffine (baseChange W K)).Equation x₁ y₁) (h₂ : (toAffine (baseChange W K)).Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (toAffine (baseChange W K)).negY x₂ y₂)) (hu₁ : x₁ ≠ x₂ → Polynomial.evalEval x₁ y₁ (toAffine (baseChange W K)).polynomialY ≠ 0) (hu₂ : x₁ ≠ x₂ → Polynomial.evalEval x₂ y₂ (toAffine (baseChange W K)).polynomialY ≠ 0) (hu₃ : Polynomial.evalEval ((toAffine (baseChange W K)).addX x₁ x₂ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) ((toAffine (baseChange W K)).addY x₁ x₂ y₁ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) (toAffine (baseChange W K)).polynomialY ≠ 0) : (Polynomial.evalEval ((toAffine (baseChange W K)).addX x₁ x₂ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) ((toAffine (baseChange W K)).addY x₁ x₂ y₁ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) (toAffine (baseChange W K)).polynomialY)⁻¹ • D ((toAffine (baseChange W K)).addX x₁ x₂ ((toAffine (baseChange W K)).slope x₁ x₂ y₁ y₂)) = (Polynomial.evalEval x₁ y₁ (toAffine (baseChange W K)).polynomialY)⁻¹ • D x₁ + (Polynomial.evalEval x₂ y₂ (toAffine (baseChange W K)).polynomialY)⁻¹ • D x₂

The differential dx / W_Y is additive: under the hypotheses of derivation_addX_slope, if W_Y does not vanish at the sum either, then W_Y(x₃, y₃)⁻¹ • D x₃ = W_Y(x₁, y₁)⁻¹ • D x₁ + W_Y(x₂, y₂)⁻¹ • D x₂.