The Weierstrass partial derivatives are derivatives

Mathlib defines the two partial derivatives WeierstrassCurve.Affine.polynomialX and WeierstrassCurve.Affine.polynomialY of the Weierstrass polynomial W(X, Y) by explicit formulae, and marks both definitions with the comment TODO: define this in terms of Polynomial.derivative. This file identifies each of them with the derivative it is named after.

Main statements

• WeierstrassCurve.Affine.derivative_polynomial: W_Y is Polynomial.derivative W(X, Y), an identity of bivariate polynomials. No evaluation is involved: R[X][Y] is a polynomial ring in Y over R[X], so Polynomial.derivative already differentiates in Y.
• WeierstrassCurve.Affine.equivPolynomial_mapCoeffs_polynomial: W_X is the coefficientwise derivative of W(X, Y), again an identity of bivariate polynomials with no evaluation involved.
• WeierstrassCurve.Affine.derivative_eval_polynomial: the chain rule along a substitution Y := p, which expresses derivative (W(X, p)) through both partials. For a constant p = C y the Y-term drops out and this reads W_X(X, y).
• WeierstrassCurve.Affine.polynomialY_eq_zero_iff: W_Y vanishes exactly when 2 = 0 and a₁ = a₃ = 0, the criterion behind polynomialY_ne_zero.
• WeierstrassCurve.Affine.polynomialY_ne_zero: W_Y is a nonzero polynomial once Δ ≠ 0. This is what makes the Weierstrass equation separable in Y, and so the function field a separable extension of the rational functions in x; in characteristic two the leading term of W_Y vanishes and the discriminant is what rules out a₁ = a₃ = 0.

Every statement here holds over an arbitrary commutative ring; only polynomialY_ne_zero carries a further hypothesis, Δ ≠ 0.

Implementation notes

Polynomial.derivative on R[X][Y] differentiates in Y, so derivative_polynomial is an identity of bivariate polynomials with no evaluation anywhere. Differentiating in X instead means differentiating the coefficients, which Derivation.mapCoeffs does; reading the result back in R[X][Y] along PolynomialModule.equivPolynomial gives the shape standing on the right of Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, so no MvPolynomial transport is needed to state that partial either.

Each partial is therefore stated bare and one at a time, and the chain rule is derived from the two rather than taken as primitive: derivative_eval_polynomial follows from equivPolynomial_mapCoeffs_polynomial and derivative_polynomial through Derivation.apply_eval_eq. The substituted form remains the one most consumers meet, so it is kept, but it is now a corollary of the bare identities rather than the only statement of them.

Provenance

Two of the three identities come from the proof of WeierstrassCurve.Affine.Point.nonsingular_of_isUnit_XYIdeal in Affine/Point/ToClass.lean, which is itself ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, by Chris Birkbeck), where they were local haves over a field, stated after evaluating at a point.

They are restated here to different degrees, and only one of them is a straight extraction. derivative_polynomial is the identity the have already had, moved ahead of the evaluation and over a commutative ring. derivative_eval_polynomial goes beyond its have: that one covered only the constant substitution p = C y, for which the Y-term drops out, so the chain rule for an arbitrary p : R[X] is a generalisation of it rather than an extraction of it. The constant case is what the call site in ToClass.lean recovers.

equivPolynomial_mapCoeffs_polynomial has no counterpart in the source: the haves worked with the substituted form throughout, and the bare X-partial is stated here for the first time.

@[simp]

theorem WeierstrassCurve.Affine.derivative_polynomial {R : Type u_1} [CommRing R] {W : Affine R} : Polynomial.derivative W.polynomial = W.polynomialY

The Y-partial derivative of W(X, Y) is a Polynomial.derivative. Viewing R[X][Y] as a polynomial ring in Y over R[X], differentiating W(X, Y) in Y gives W_Y(X, Y) on the nose.

@[simp]

theorem WeierstrassCurve.Affine.equivPolynomial_mapCoeffs_polynomial {R : Type u_1} [CommRing R] {W : Affine R} : PolynomialModule.equivPolynomial (Polynomial.derivative'.mapCoeffs W.polynomial) = W.polynomialX

The X-partial derivative of W(X, Y) is a coefficientwise derivative. Differentiating W(X, Y) in X means differentiating its coefficients, which Derivation.mapCoeffs does; reading the result back in R[X][Y] gives W_X(X, Y) on the nose.

@[simp]

theorem WeierstrassCurve.Affine.derivative_eval_polynomial {R : Type u_1} [CommRing R] {W : Affine R} (p : Polynomial R) : Polynomial.derivative (Polynomial.eval p W.polynomial) = Polynomial.eval p W.polynomialX + Polynomial.eval p W.polynomialY * Polynomial.derivative p

The chain rule for W(X, Y) along a substitution Y := p. Differentiating the one-variable polynomial W(X, p) splits into the two partials of W, the Y-one weighted by p'. Substituting a constant p = C y kills the second term and leaves W_X(X, y).

@[simp]

theorem WeierstrassCurve.Affine.polynomialY_eq_zero_iff {R : Type u_1} [CommRing R] {W : Affine R} : W.polynomialY = 0 ↔ 2 = 0 ∧ W.a₁ = 0 ∧ W.a₃ = 0

W_Y = 2Y + a₁X + a₃ vanishes exactly when 2 = 0 and a₁ = a₃ = 0. So W_Y is a nonzero polynomial wherever 2 ≠ 0, and where 2 = 0 it is nonzero exactly when a₁ ≠ 0 or a₃ ≠ 0; polynomialY_ne_zero draws the latter from Δ ≠ 0.

theorem WeierstrassCurve.Affine.polynomialY_ne_zero {R : Type u_1} [CommRing R] {W : Affine R} (hΔ : Δ W ≠ 0) : W.polynomialY ≠ 0

The partial derivative W_Y = 2Y + a₁X + a₃ of the Weierstrass polynomial is a nonzero polynomial whenever the discriminant is nonzero. In characteristic two the first term vanishes, and it is Δ ≠ 0 that rules out a₁ = a₃ = 0; the criterion carrying no hypothesis on Δ is polynomialY_eq_zero_iff.