The division-polynomial Wronskian at the generic point

Multiplication by n scales the invariant differential, [n]*ω = n ω (Silverman III.5.3). Read through ω = dx / u with u = 2y + a₁x + a₃, and through [n]*x = Φₙ / ΨSqₙ, that single differential identity becomes an identity between division polynomials: the quotient rule turns d([n]*x) into the Wronskian Φₙ' ΨSqₙ - Φₙ ΨSqₙ' over ΨSqₙ², and comparing coefficients of dx gives

(Φₙ' ΨSqₙ - Φₙ ΨSqₙ') u = n ΨSqₙ² ([n]*u)

at the generic point. The other half rewrites ΨSqₙ² ([n]*u) as preΨ_{2n} u, through the two identities ψc is defined by, and the two together give the classical polynomial identity

Φₙ' ΨSqₙ - Φₙ ΨSqₙ' = n · preΨ_{2n} in F[X],

by cancelling u and descending along the injective algebraMap F[X] → F(W).

The identity is an input to the multiplicity-one step in the unramifiedness of [n] (Silverman III.4.10(c)), not that step itself. There the fibre polynomial Φₙ - x_Q · ΨSqₙ is differentiated at the x-coordinate of a preimage P, and the identity evaluates that derivative as n · preΨ_{2n}(x_P) / ΨSqₙ(x_P). Concluding a simple root needs that quantity to be nonzero, which the identity alone does not give. It requires (n : F) ≠ 0 — so the characteristic must not divide n — together with the numerator condition preΨ_{2n}(x_P) ≠ 0 and the denominator condition ΨSqₙ(x_P) ≠ 0. Those two are not the same as P ∉ ker [2n]: since ψ_{2n} = preΨ_{2n} ψ₂, a 2-torsion P, where ψ₂(P) = 0, can lie in ker [2n] with both of the factors above nonzero.

Main results

• TauCeti.Isogeny.wronskian_Φ_ΨSq_mul_invariantDifferentialDenom: the identity above.
• TauCeti.Isogeny.two_mul_omega_add_eq_psic and TauCeti.Isogeny.psi_mul_psic: the two identities characterising psicFunctionField — 2 ωₙ + a₁ φₙ ψₙ + a₃ ψₙ³ = ψcₙ and ψₙ ψcₙ = ψ_{2n} — at the generic point.
• TauCeti.Isogeny.psiFunctionField_cube_mul_fieldPullback_invariantDifferentialDenom: ψₙ³ ([n]*u) = ψcₙ, the first half of the preΨ bridge, and TauCeti.Isogeny.aeval_ΨSq_sq_mul_fieldPullback_invariantDifferentialDenom: ΨSqₙ² ([n]*u) = preΨ_{2n} u, the bridge itself.
• TauCeti.Isogeny.wronskian_Φ_ΨSq: the classical polynomial identity Φₙ' ΨSqₙ - Φₙ ΨSqₙ' = n · preΨ_{2n}, for every Weierstrass curve over every commutative ring and every integer n — the function-field proof needs a field and an elliptic curve, but the statement does not, and the universal curve discharges both once and for all.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.5.3.

Provenance

AINTLIB (Chris Birkbeck), Apache-2.0, at commit a302aeacd86053f9d5f991fbbf664e1cc1051d08, proves the same identity as divPoly_wronskian_identity_of_omega, at projects/HasseWeil/HasseWeil/Foundation/OmegaPullbackCoeff.lean:776. There it is stated over a packaging of the scaling factor as omegaPullbackCoeff, and takes a_{[n]} = n as a hypothesis; TauCeti already proves the scaling identity itself (pullbackDifferential_mulByIntIsogeny_invariantDifferential), so no packaging is needed and the hypothesis is discharged. Only the quotient-rule computation is carried over.

theorem TauCeti.Isogeny.wronskian_Φ_ΨSq_mul_invariantDifferentialDenom {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : ((Polynomial.aeval W.genericX) (Polynomial.derivative (WeierstrassCurve.Φ W n)) * (Polynomial.aeval W.genericX) (WeierstrassCurve.ΨSq W n) - (Polynomial.aeval W.genericX) (WeierstrassCurve.Φ W n) * (Polynomial.aeval W.genericX) (Polynomial.derivative (WeierstrassCurve.ΨSq W n))) * W.invariantDifferentialDenom = ↑n * (Polynomial.aeval W.genericX) (WeierstrassCurve.ΨSq W n) ^ 2 * (mulByIntIsogeny W hn).fieldPullback W.invariantDifferentialDenom

The division-polynomial Wronskian at the generic point:

(Φₙ' ΨSqₙ - Φₙ ΨSqₙ') u = n ΨSqₙ² ([n]*u),

where u = 2y + a₁x + a₃ is the denominator of the invariant differential. This is the function-field form of the Wronskian; the polynomial identity wronskian_Φ_ΨSq follows from it and the preΨ bridge below.

The ψc bridge

[n]*u is u read at the image point (Φₙ/ΨSqₙ, ωₙ/ψₙ³), so clearing ψₙ³ turns it into the left-hand side of ω_spec, the identity ψc is defined by.

theorem TauCeti.Isogeny.two_mul_omega_add_eq_psic {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : 2 * omegaFunctionField W n + (algebraMap F W.FunctionField) W.a₁ * phiFunctionField W n * psiFunctionField W n + (algebraMap F W.FunctionField) W.a₃ * psiFunctionField W n ^ 3 = psicFunctionField W n

The defining identity for ψc at the generic point: 2 ωₙ + a₁ φₙ ψₙ + a₃ ψₙ³ = ψcₙ.

theorem TauCeti.Isogeny.psiFunctionField_cube_mul_fieldPullback_invariantDifferentialDenom {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : psiFunctionField W n ^ 3 * (mulByIntIsogeny W hn).fieldPullback W.invariantDifferentialDenom = psicFunctionField W n

ψₙ³ · ([n]*u) = ψcₙ, where u = 2y + a₁x + a₃.

The first half of the bridge from [n]*u to the division polynomials; with psi_mul_psic it gives aeval_ΨSq_sq_mul_fieldPullback_invariantDifferentialDenom.

theorem TauCeti.Isogeny.psi_mul_psic {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (n : ℤ) : psiFunctionField W n * psicFunctionField W n = psiFunctionField W (2 * n)

ψₙ ψcₙ = ψ_{2n} at the generic point, the complement identity ψc is named for.

theorem TauCeti.Isogeny.aeval_ΨSq_sq_mul_fieldPullback_invariantDifferentialDenom {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (Polynomial.aeval W.genericX) (WeierstrassCurve.ΨSq W n) ^ 2 * (mulByIntIsogeny W hn).fieldPullback W.invariantDifferentialDenom = (algebraMap (Polynomial F) W.FunctionField) (WeierstrassCurve.preΨ W (2 * n)) * W.invariantDifferentialDenom

The preΨ bridge: ΨSqₙ² ([n]*u) = preΨ_{2n} u.

With the Wronskian at the generic point this gives the polynomial identity wronskian_Φ_ΨSq.

Off the elliptic hypothesis, by the universal curve

theorem TauCeti.Isogeny.wronskian_Φ_ΨSq {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial.derivative (W.Φ n) * W.ΨSq n - W.Φ n * Polynomial.derivative (W.ΨSq n) = Polynomial.C ↑n * W.preΨ (2 * n)

The division-polynomial Wronskian, in its classical polynomial form:

Φₙ' ΨSqₙ - Φₙ ΨSqₙ' = n · preΨ_{2n} in R[X],

for every Weierstrass curve over every commutative ring and every integer n. It is a polynomial identity in the coefficients, so neither a field nor nonsingularity is needed: those are hypotheses of the proof, discharged once over the universal curve.