The addition theorem for `℘` and the group law on `ℂ / Λ` #

This file proves the addition theorem for the Weierstrass ℘-function of a period lattice Λ: for z, w ∉ Λ with ℘(z) ≠ ℘(w),

℘(z + w) = ((℘'(z) - ℘'(w)) / (℘(z) - ℘(w)))² / 4 - ℘(z) - ℘(w),

together with the companion formula for ℘'(z + w). In terms of the point map P(z) = (℘(z), ℘'(z) / 2) to the Weierstrass curve y² = x³ - (g₂ / 4) x - g₃ / 4 (PeriodPair.weierstrassPoint), these say that P(z + w) is the chord-and-tangent sum of P(z) and P(w). Hence P is a group homomorphism from ℂ to the points of the curve with kernel Λ: this is the injectivity half of the complex uniformization ℂ / Λ ≃ E(ℂ). Together with the surjectivity of P (PeriodPair.weierstrassPoint_surjective), it gives the group isomorphism ℂ / Λ ≃+ E(ℂ) (PeriodPair.weierstrassPointEquiv).

Main results #

PeriodPair.hasDerivAt_derivWeierstrassP: ℘'' = 6 ℘² - g₂ / 2 off the lattice.
PeriodPair.weierstrassP_add, PeriodPair.derivWeierstrassP_add: the addition theorems for ℘ and ℘'.
PeriodPair.weierstrassPoint_add: P(z + w) = P(z) + P(w).
PeriodPair.weierstrassPointHom: the point map as a group homomorphism ℂ →+ E(ℂ), and PeriodPair.ker_weierstrassPointHom: its kernel is Λ.
PeriodPair.weierstrassPointEquiv: the group isomorphism ℂ / Λ ≃+ E(ℂ) induced by the point map, which is surjective by PeriodPair.weierstrassPoint_surjective, with PeriodPair.weierstrassPointEquiv_mk and PeriodPair.weierstrassPointEquiv_symm_weierstrassPoint for the isomorphism and its inverse on the class of z.

Implementation notes #

The addition theorem is proved by differentiation rather than by Liouville's theorem, which would need the principal parts of ℘(z + w) and of the slope at z = -w. Along a line z + w = s, the function ℘(z) + ℘(w) - ((℘'(z) - ℘'(w)) / (℘(z) - ℘(w)))² / 4 has derivative zero by the differential equation ℘'² = 4 ℘³ - g₂ ℘ - g₃ and its derivative ℘'' = 6 ℘² - g₂ / 2; its limit as z → 0 is -℘(s). The resulting polynomial identity extends to all z, w, z + w ∉ Λ by the identity theorem, the complement of a countable set in ℂ being connected. The formula for ℘' follows by differentiating again. These give the group law in the chord case ℘(z) ≠ ℘(w). When ℘(z) = ℘(w), it follows by cancelling P(t) in P(z + w) + P(t) = P(z + w + t) = P(z) + P(w + t) = P(z) + P(w) + P(t), where each equality is a chord case for a suitable small t.

References #

E. T. Whittaker and G. N. Watson, A Course of Modern Analysis, 4th ed., Cambridge University Press, 1927, §20.3.
J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009, §VI.3.

The second derivative of `℘` #

source

theorem PeriodPair.hasDerivAt_weierstrassP (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) :

HasDerivAt L.weierstrassP (L.derivWeierstrassP z) z

Off the lattice, ℘ has derivative ℘'.

source

theorem PeriodPair.hasDerivAt_derivWeierstrassP (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) :

HasDerivAt L.derivWeierstrassP (6 * L.weierstrassP z ^ 2 - L.g₂ / 2) z

℘'' = 6 ℘² - g₂ / 2. Off the lattice, ℘' has derivative 6 ℘² - g₂ / 2.

source

@[simp]

theorem PeriodPair.deriv_derivWeierstrassP (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) :

deriv L.derivWeierstrassP z = 6 * L.weierstrassP z ^ 2 - L.g₂ / 2

℘'' = 6 ℘² - g₂ / 2 off the lattice.

The addition theorem for `℘` and `℘'` #

source

theorem PeriodPair.weierstrassP_add (L : PeriodPair) {z w : ℂ} (hz : z ∉ L.lattice) (hw : w ∉ L.lattice) (h : L.weierstrassP z ≠ L.weierstrassP w) :

L.weierstrassP (z + w) = ((L.derivWeierstrassP z - L.derivWeierstrassP w) / (L.weierstrassP z - L.weierstrassP w)) ^ 2 / 4 - L.weierstrassP z - L.weierstrassP w

The addition theorem for ℘. If z, w ∉ Λ and ℘(z) ≠ ℘(w), then ℘(z + w) = ((℘'(z) - ℘'(w)) / (℘(z) - ℘(w)))² / 4 - ℘(z) - ℘(w).

source

theorem PeriodPair.derivWeierstrassP_add (L : PeriodPair) {z w : ℂ} (hz : z ∉ L.lattice) (hw : w ∉ L.lattice) (h : L.weierstrassP z ≠ L.weierstrassP w) :

L.derivWeierstrassP (z + w) = -((L.derivWeierstrassP z - L.derivWeierstrassP w) / (L.weierstrassP z - L.weierstrassP w)) * (L.weierstrassP (z + w) - L.weierstrassP z) - L.derivWeierstrassP z

The addition theorem for ℘'. If z, w ∉ Λ and ℘(z) ≠ ℘(w), then ℘'(z + w) = -m (℘(z + w) - ℘(z)) - ℘'(z) with m = (℘'(z) - ℘'(w)) / (℘(z) - ℘(w)): the points (℘(z), ℘'(z)), (℘(w), ℘'(w)) and (℘(z + w), -℘'(z + w)) lie on a line of slope m.

The group law #

source

@[simp]

theorem PeriodPair.weierstrassPoint_add (L : PeriodPair) (z w : ℂ) :

L.weierstrassPoint (z + w) = L.weierstrassPoint z + L.weierstrassPoint w

The addition law. The point map z ↦ (℘(z), ℘'(z) / 2) (sending Λ to the point at infinity) is additive: P(z + w) = P(z) + P(w) in the group of points of the Weierstrass curve.

source

noncomputable def PeriodPair.weierstrassPointHom (L : PeriodPair) :

ℂ →+ L.weierstrassCurve.toAffine.Point

The point map z ↦ (℘(z), ℘'(z) / 2) as a group homomorphism from ℂ to the points of the Weierstrass curve of L.

Instances For

source

@[simp]

theorem PeriodPair.weierstrassPointHom_apply (L : PeriodPair) (z : ℂ) :

L.weierstrassPointHom z = L.weierstrassPoint z

source

theorem PeriodPair.ker_weierstrassPointHom (L : PeriodPair) :

L.weierstrassPointHom.ker = L.lattice.toAddSubgroup

The kernel of the point map is the period lattice.

source

noncomputable def PeriodPair.weierstrassPointEquiv (L : PeriodPair) :

ℂ ⧸ L.lattice.toAddSubgroup ≃+ L.weierstrassCurve.toAffine.Point

The complex uniformization ℂ / Λ ≃+ E_Λ(ℂ), induced by the point map z ↦ (℘(z), ℘'(z) / 2) (PeriodPair.weierstrassPoint), which is a surjective group homomorphism with kernel Λ.

Instances For

source

@[simp]