The Weierstrass curve of a period lattice

A period pair L with lattice Λ has the lattice invariants g₂ = 60 ∑' λ⁻⁴ and g₃ = 140 ∑' λ⁻⁶ (PeriodPair.g₂, PeriodPair.g₃), and Mathlib proves the differential equation ℘'² = 4 ℘³ - g₂ ℘ - g₃ (PeriodPair.derivWeierstrassP_sq). Dividing ℘' by 2 turns this into a Weierstrass equation with leading coefficient one, so this file attaches to L the Weierstrass curve

y² = x³ - (g₂ / 4) x - g₃ / 4

(PeriodPair.weierstrassCurve) and the map z ↦ (℘(z), ℘'(z) / 2) from ℂ to its points, sending the lattice to the point at infinity (PeriodPair.weierstrassPoint). These are the first steps of the complex uniformization ℂ / Λ ≃ E(ℂ).

The discriminant of the curve is g₂³ - 27 g₃². For the lattice ℤ τ + ℤ of a point τ of the upper half-plane, the lattice sums are Eisenstein series, g₂ = (4 π⁴ / 3) E₄(τ) and g₃ = (8 π⁶ / 27) E₆(τ) (by Mathlib's tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries), so the identity E₄³ - E₆² = 1728 Δ (ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq) gives g₂³ - 27 g₃² = (2 π)¹² Δ(τ), which does not vanish. Every lattice is a nonzero multiple of such a lattice, and rescaling a lattice by c multiplies g₂ by c⁻⁴ and g₃ by c⁻⁶; so the discriminant never vanishes and the curve is elliptic. Its j-invariant is 1728 g₂³ / (g₂³ - 27 g₃²), which for ℤ τ + ℤ is the modular invariant j(τ) = E₄(τ)³ / Δ(τ).

The point map has holomorphic lifts to projective coordinates. Off the lattice this is the holomorphy of ℘ and ℘' in the affine chart. Near the point at infinity the projective curve is covered by the chart Y ≠ 0, with coordinates x / y = 2 ℘ / ℘' and 1 / y = 2 / ℘'. Near a lattice point l₀ write ℘'(z) = ℘'_{l₀}(z) - 2 / (z - l₀)³ and `℘(z) = ℘_{l₀}(z) + 1 / (z - l₀)²

• 1 / l₀², with ℘{l₀} = PeriodPair.weierstrassPExcept L l₀and `℘'{l₀} = PeriodPair.derivWeierstrassPExcept L l₀holomorphic atl₀`; this gives

  1 / ℘'(z) = (z - l₀)³ / ((z - l₀)³ ℘'_{l₀}(z) - 2),

whose denominator is -2 at l₀, and similarly for ℘ / ℘'. So both chart coordinates are holomorphic at l₀, they vanish there, and ℘ / ℘' has derivative -1 / 2 at l₀. In particular the point map is injective near every lattice point.

The point map is surjective. By Liouville's theorem ℘ takes every value x: otherwise 1 / (℘ - x), which near a lattice point l₀ is (z - l₀)² divided by a function with value 1 at l₀, would extend by 0 on Λ to a bounded entire Λ-periodic function, hence a constant, while it vanishes on Λ and nowhere else. A point (x, y) of the curve with ℘(z) = x has y = ± ℘'(z) / 2, and z or -z maps to it.

Main definitions

• PeriodPair.weierstrassCurve: the Weierstrass curve y² = x³ - (g₂ / 4) x - g₃ / 4.
• PeriodPair.weierstrassPoint: the point (℘(z), ℘'(z) / 2), or 0 for z ∈ Λ.
• PeriodPair.pointAddEquivOfLatticeEq: for Λ' = c Λ, the isomorphism E_{Λ'}(ℂ) ≃+ E_Λ(ℂ) given by the change of variables with u = c.

Main results

• PeriodPair.weierstrassCurve_smul: rescaling the lattice by c changes the curve by the variable change with u = c.
• UpperHalfPlane.G_periodPair: G k (ℤ τ + ℤ) = 2 ζ(k) E_k(τ) for k ≥ 3.
• UpperHalfPlane.weierstrassCurve_Δ_periodPair: the discriminant of the curve of ℤ τ + ℤ is (2 π)¹² Δ(τ).
• PeriodPair.weierstrassCurve_Δ, PeriodPair.weierstrassCurve_Δ_ne_zero: the discriminant is g₂³ - 27 g₃², and it is nonzero.
• PeriodPair.weierstrassCurve_j, UpperHalfPlane.weierstrassCurve_j_periodPair: the j-invariant, and its identification with the modular invariant TauCeti.ModularForm.j.
• PeriodPair.weierstrassCurve_j_eq_1728_iff, PeriodPair.weierstrassCurve_j_eq_zero_iff: the j-invariant is 1728 exactly when g₃ = 0, and 0 exactly when g₂ = 0.
• PeriodPair.weierstrassPoint_add_coe, PeriodPair.weierstrassPoint_neg, PeriodPair.weierstrassPoint_eq_zero_iff: the point map is Λ-periodic, odd, and vanishes exactly on Λ.
• PeriodPair.inv_derivWeierstrassP_eq, PeriodPair.weierstrassP_div_derivWeierstrassP_eq: 1 / ℘' and ℘ / ℘' near a lattice point l₀, in terms of ℘_{l₀} and ℘'_{l₀}.
• PeriodPair.analyticAt_weierstrassP_div_derivWeierstrassP, PeriodPair.analyticAt_inv_derivWeierstrassP: the coordinates ℘ / ℘' and 1 / ℘' of the chart at infinity are holomorphic on its domain {℘' ≠ 0} ∪ Λ.
• PeriodPair.hasDerivAt_weierstrassP_div_derivWeierstrassP: ℘ / ℘' has derivative -1 / 2 at every lattice point.
• PeriodPair.exists_analyticAt_toAffine_eq_weierstrassPoint: near every point, the point map has a holomorphic lift to nonsingular projective coordinates.
• PeriodPair.exists_mem_nhds_injOn_weierstrassPoint: the point map is injective near every lattice point.
• PeriodPair.exists_weierstrassP_eq: ℘ takes every complex value off the lattice.
• PeriodPair.weierstrassPoint_surjective: every point of the curve is in the image of the point map.
• PeriodPair.weierstrassCurve_eq_smul_of_lattice_eq, PeriodPair.weierstrassCurve_j_eq_of_lattice_eq_smul: for Λ' = c Λ, the curve of Λ' is the change of variables of that of Λ with u = c, so homothetic lattices have the same j-invariant.
• PeriodPair.pointAddEquivOfLatticeEq_weierstrassPoint, PeriodPair.pointAddEquivOfLatticeEq_symm_weierstrassPoint: rescaling naturality of the point map, sending the point of c z on E_{cΛ} to the point of z on E_Λ. Since the curve only depends on the lattice, the same holds for any basis of cΛ.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009, §VI.3 and §VI.5.
• J.-P. Serre, A Course in Arithmetic, Graduate Texts in Mathematics 7, Springer, 1973, §VII.2.3 and §VII.3.3.

Lattice sums of ℤ τ + ℤ

theorem UpperHalfPlane.G_periodPair (τ : UpperHalfPlane) {k : ℕ} (hk : 3 ≤ k) : τ.periodPair.G k = 2 * riemannZeta ↑k * (ModularForm.E hk) τ

For k ≥ 3 the lattice sum G k of ℤ τ + ℤ is the Eisenstein series 2 ζ(k) E_k(τ).

theorem UpperHalfPlane.g₂_periodPair (τ : UpperHalfPlane) : τ.periodPair.g₂ = 4 * ↑Real.pi ^ 4 / 3 * ModularForm.E₄ τ

g₂(ℤ τ + ℤ) = (4 π⁴ / 3) E₄(τ).

theorem UpperHalfPlane.g₃_periodPair (τ : UpperHalfPlane) : τ.periodPair.g₃ = 8 * ↑Real.pi ^ 6 / 27 * ModularForm.E₆ τ

g₃(ℤ τ + ℤ) = (8 π⁶ / 27) E₆(τ).

The Weierstrass curve of a period lattice

noncomputable def PeriodPair.weierstrassCurve (L : PeriodPair) : WeierstrassCurve ℂ

The Weierstrass curve y² = x³ - (g₂ / 4) x - g₃ / 4 of a period lattice. The point (℘(z), ℘'(z) / 2) lies on it for z ∉ Λ (PeriodPair.equation_weierstrassP).

@[simp]

theorem PeriodPair.weierstrassCurve_a₁ (L : PeriodPair) : L.weierstrassCurve.a₁ = 0

@[simp]

theorem PeriodPair.weierstrassCurve_a₂ (L : PeriodPair) : L.weierstrassCurve.a₂ = 0

@[simp]

theorem PeriodPair.weierstrassCurve_a₃ (L : PeriodPair) : L.weierstrassCurve.a₃ = 0

@[simp]

theorem PeriodPair.weierstrassCurve_a₄ (L : PeriodPair) : L.weierstrassCurve.a₄ = -(L.g₂ / 4)

@[simp]

theorem PeriodPair.weierstrassCurve_a₆ (L : PeriodPair) : L.weierstrassCurve.a₆ = -(L.g₃ / 4)

theorem PeriodPair.weierstrassCurve_Δ (L : PeriodPair) : L.weierstrassCurve.Δ = L.g₂ ^ 3 - 27 * L.g₃ ^ 2

The discriminant of the Weierstrass curve of a lattice is g₂³ - 27 g₃².

theorem PeriodPair.weierstrassCurve_smul (L : PeriodPair) (c : ℂˣ) : (c • L).weierstrassCurve = { u := c, r := 0, s := 0, t := 0 } • L.weierstrassCurve

Rescaling the lattice by c changes its Weierstrass curve by the variable change (x, y) ↦ (c⁻² x, c⁻³ y), that is, with u = c and r = s = t = 0.

theorem PeriodPair.weierstrassCurve_eq_of_lattice_eq {L L' : PeriodPair} (h : L.lattice = L'.lattice) : L.weierstrassCurve = L'.weierstrassCurve

The Weierstrass curve depends only on the lattice, not on the chosen basis.

theorem UpperHalfPlane.weierstrassCurve_Δ_periodPair (τ : UpperHalfPlane) : τ.periodPair.weierstrassCurve.Δ = (2 * ↑Real.pi) ^ 12 * ModularForm.discriminant τ

The discriminant of the Weierstrass curve of ℤ τ + ℤ is (2 π)¹² Δ(τ).

theorem PeriodPair.weierstrassCurve_Δ_ne_zero (L : PeriodPair) : L.weierstrassCurve.Δ ≠ 0

The discriminant g₂³ - 27 g₃² of a lattice does not vanish.

instance PeriodPair.instIsEllipticComplexWeierstrassCurve (L : PeriodPair) : L.weierstrassCurve.IsElliptic

theorem PeriodPair.weierstrassCurve_j (L : PeriodPair) : L.weierstrassCurve.j = 1728 * L.g₂ ^ 3 / (L.g₂ ^ 3 - 27 * L.g₃ ^ 2)

The j-invariant of the Weierstrass curve of a lattice is 1728 g₂³ / (g₂³ - 27 g₃²).

theorem PeriodPair.weierstrassCurve_j_eq_1728_iff {L : PeriodPair} : L.weierstrassCurve.j = 1728 ↔ L.g₃ = 0

The j-invariant of E_Λ is 1728 exactly when g₃(Λ) = 0.

theorem PeriodPair.weierstrassCurve_j_eq_zero_iff {L : PeriodPair} : L.weierstrassCurve.j = 0 ↔ L.g₂ = 0

The j-invariant of E_Λ is 0 exactly when g₂(Λ) = 0.

theorem UpperHalfPlane.weierstrassCurve_j_periodPair (τ : UpperHalfPlane) : τ.periodPair.weierstrassCurve.j = TauCeti.ModularForm.j τ

The j-invariant of the Weierstrass curve of ℤ τ + ℤ is the modular invariant j(τ) = E₄(τ)³ / Δ(τ).

The point (℘(z), ℘'(z) / 2)

theorem PeriodPair.equation_weierstrassP (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) : L.weierstrassCurve.toAffine.Equation (L.weierstrassP z) (L.derivWeierstrassP z / 2)

For z ∉ Λ the point (℘(z), ℘'(z) / 2) lies on the Weierstrass curve of L: this is the differential equation ℘'² = 4 ℘³ - g₂ ℘ - g₃ divided by 4.

theorem PeriodPair.nonsingular_weierstrassP (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) : L.weierstrassCurve.toAffine.Nonsingular (L.weierstrassP z) (L.derivWeierstrassP z / 2)

noncomputable def PeriodPair.weierstrassPoint (L : PeriodPair) (z : ℂ) : L.weierstrassCurve.toAffine.Point

The point (℘(z), ℘'(z) / 2) of the Weierstrass curve of L for z ∉ Λ, and the point at infinity 0 for z ∈ Λ.

theorem PeriodPair.weierstrassPoint_of_mem (L : PeriodPair) {z : ℂ} (hz : z ∈ L.lattice) : L.weierstrassPoint z = 0

theorem PeriodPair.weierstrassPoint_of_notMem (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) : L.weierstrassPoint z = WeierstrassCurve.Affine.Point.some (L.weierstrassP z) (L.derivWeierstrassP z / 2) ⋯

@[simp]

theorem PeriodPair.weierstrassPoint_coe (L : PeriodPair) (l : ↥L.lattice) : L.weierstrassPoint ↑l = 0

@[simp]

theorem PeriodPair.weierstrassPoint_zero (L : PeriodPair) : L.weierstrassPoint 0 = 0

@[simp]

theorem PeriodPair.weierstrassPoint_eq_zero_iff (L : PeriodPair) {z : ℂ} : L.weierstrassPoint z = 0 ↔ z ∈ L.lattice

The point map vanishes exactly on the lattice.

theorem PeriodPair.weierstrassPoint_add_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.weierstrassPoint (z + ↑l) = L.weierstrassPoint z

theorem PeriodPair.periodic_weierstrassPoint (L : PeriodPair) (l : ↥L.lattice) : Function.Periodic L.weierstrassPoint ↑l

@[simp]

theorem PeriodPair.weierstrassPoint_neg (L : PeriodPair) (z : ℂ) : L.weierstrassPoint (-z) = -L.weierstrassPoint z

The point map is odd: -z goes to (℘(z), -℘'(z) / 2).

The point map in the chart at infinity

theorem PeriodPair.inv_derivWeierstrassP_eq (L : PeriodPair) {l₀ : ℂ} (hl₀ : l₀ ∈ L.lattice) (z : ℂ) : (L.derivWeierstrassP z)⁻¹ = (z - l₀) ^ 3 / ((z - l₀) ^ 3 * L.derivWeierstrassPExcept l₀ z - 2)

Near a lattice point l₀, 1 / ℘' is a holomorphic function divided by a holomorphic function that is -2 at l₀. The identity holds everywhere, including the junk value ℘'(l₀)⁻¹ = 0.

theorem PeriodPair.weierstrassP_div_derivWeierstrassP_eq (L : PeriodPair) {l₀ : ℂ} (hl₀ : l₀ ∈ L.lattice) (z : ℂ) : L.weierstrassP z / L.derivWeierstrassP z = (z - l₀) * (((z - l₀) ^ 2 * (L.weierstrassPExcept l₀ z - 1 / l₀ ^ 2) + 1) / ((z - l₀) ^ 3 * L.derivWeierstrassPExcept l₀ z - 2))

Near a lattice point l₀, ℘ / ℘' is z - l₀ times a quotient of holomorphic functions whose value at l₀ is 1 / (-2).

theorem PeriodPair.analyticAt_inv_derivWeierstrassP (L : PeriodPair) {z₀ : ℂ} (h : L.derivWeierstrassP z₀ ≠ 0 ∨ z₀ ∈ L.lattice) : AnalyticAt ℂ (fun (z : ℂ) => (L.derivWeierstrassP z)⁻¹) z₀

The coordinate 1 / ℘' of the chart at infinity is holomorphic on the domain of that chart: where ℘' ≠ 0, and at the lattice points, where it vanishes.

theorem PeriodPair.analyticAt_weierstrassP_div_derivWeierstrassP (L : PeriodPair) {z₀ : ℂ} (h : L.derivWeierstrassP z₀ ≠ 0 ∨ z₀ ∈ L.lattice) : AnalyticAt ℂ (fun (z : ℂ) => L.weierstrassP z / L.derivWeierstrassP z) z₀

The coordinate ℘ / ℘' of the chart at infinity is holomorphic on the domain of that chart: where ℘' ≠ 0, and at the lattice points, where it vanishes.

theorem PeriodPair.hasDerivAt_weierstrassP_div_derivWeierstrassP (L : PeriodPair) {l₀ : ℂ} (hl₀ : l₀ ∈ L.lattice) : HasDerivAt (fun (z : ℂ) => L.weierstrassP z / L.derivWeierstrassP z) (-1 / 2) l₀

At a lattice point, ℘ / ℘' has derivative -1 / 2: the coordinate -x / y = -2 ℘ / ℘' is a local parameter of the curve at the point at infinity.

theorem PeriodPair.eventually_derivWeierstrassP_ne_zero (L : PeriodPair) {l₀ : ℂ} (hl₀ : l₀ ∈ L.lattice) : ∀ᶠ (z : ℂ) in nhdsWithin l₀ {l₀}ᶜ, L.derivWeierstrassP z ≠ 0

℘' has no zeros in a punctured neighbourhood of a lattice point.

theorem PeriodPair.exists_analyticAt_toAffine_eq_weierstrassPoint (L : PeriodPair) (z₀ : ℂ) : ∃ (P : ℂ → Fin 3 → ℂ), AnalyticAt ℂ P z₀ ∧ ∀ᶠ (z : ℂ) in nhds z₀, L.weierstrassCurve.toProjective.Nonsingular (P z) ∧ WeierstrassCurve.Projective.Point.toAffine L.weierstrassCurve.toProjective (P z) = L.weierstrassPoint z

The point map is holomorphic. Near every z₀ ∈ ℂ, the point (℘(z), ℘'(z) / 2) (the point at infinity for z ∈ Λ) has a holomorphic lift to nonsingular projective coordinates: the lift [℘ : ℘' / 2 : 1] off the lattice and [2 ℘ / ℘' : 1 : 2 / ℘'] near the lattice.

theorem PeriodPair.weierstrassP_div_derivWeierstrassP_eq_of_weierstrassPoint_eq (L : PeriodPair) {z w : ℂ} (h : L.weierstrassPoint z = L.weierstrassPoint w) : L.weierstrassP z / L.derivWeierstrassP z = L.weierstrassP w / L.derivWeierstrassP w

The coordinate ℘ / ℘' of the chart at infinity is a function of the point (℘(z), ℘'(z) / 2).

theorem PeriodPair.exists_mem_nhds_injOn_weierstrassPoint (L : PeriodPair) {l₀ : ℂ} (hl₀ : l₀ ∈ L.lattice) : ∃ U ∈ nhds l₀, Set.InjOn L.weierstrassPoint U

The point map is injective near every lattice point, since the local parameter ℘ / ℘' at the point at infinity has nonzero derivative there.

Surjectivity of the point map

theorem PeriodPair.exists_weierstrassP_eq (L : PeriodPair) (x : ℂ) : ∃ z ∉ L.lattice, L.weierstrassP z = x

℘ takes every complex value. For every x : ℂ there is z ∉ Λ with ℘(z) = x.

theorem PeriodPair.weierstrassPoint_surjective (L : PeriodPair) : Function.Surjective L.weierstrassPoint

The point map is surjective: every point of the Weierstrass curve of L is the point at infinity or (℘(z), ℘'(z) / 2) for some z ∉ Λ.

Homothetic lattices

theorem PeriodPair.weierstrassCurve_eq_smul_of_lattice_eq {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) : L'.weierstrassCurve = { u := c, r := 0, s := 0, t := 0 } • L.weierstrassCurve

If Λ' = c Λ, the curve of Λ' is obtained from that of Λ by the change of variables (x, y) ↦ (c⁻² x, c⁻³ y), that is, with u = c and r = s = t = 0.

theorem PeriodPair.weierstrassCurve_j_eq_of_lattice_eq_smul {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) : L'.weierstrassCurve.j = L.weierstrassCurve.j

Homothetic lattices have the same j-invariant.

noncomputable def PeriodPair.pointAddEquivOfLatticeEq {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) : L'.weierstrassCurve.toAffine.Point ≃+ L.weierstrassCurve.toAffine.Point

For Λ' = c Λ, the isomorphism E_{Λ'}(ℂ) ≃+ E_Λ(ℂ) given by the change of variables (x, y) ↦ (c² x, c³ y). It sends the point of c z to the point of z (PeriodPair.pointAddEquivOfLatticeEq_weierstrassPoint).

theorem PeriodPair.pointAddEquivOfLatticeEq_some {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) {x y x' y' : ℂ} (hxy : L'.weierstrassCurve.toAffine.Nonsingular x y) (hxy' : L.weierstrassCurve.toAffine.Nonsingular x' y') (hx : x' = ↑c ^ 2 * x) (hy : y' = ↑c ^ 3 * y) : (pointAddEquivOfLatticeEq h) (WeierstrassCurve.Affine.Point.some x y hxy) = WeierstrassCurve.Affine.Point.some x' y' hxy'

On affine points, PeriodPair.pointAddEquivOfLatticeEq is (x, y) ↦ (c² x, c³ y).

@[simp]

theorem PeriodPair.pointAddEquivOfLatticeEq_weierstrassPoint {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) (z : ℂ) : (pointAddEquivOfLatticeEq h) (L'.weierstrassPoint (↑c * z)) = L.weierstrassPoint z

Rescaling naturality of the point map. If Λ' = c Λ, the change of variables from E_{Λ'} to E_Λ sends the point (℘(c z; Λ'), ℘'(c z; Λ') / 2) to (℘(z; Λ), ℘'(z; Λ) / 2).

@[simp]

theorem PeriodPair.pointAddEquivOfLatticeEq_symm_weierstrassPoint {L L' : PeriodPair} {c : ℂˣ} (h : L'.lattice = (c • L).lattice) (z : ℂ) : (pointAddEquivOfLatticeEq h).symm (L.weierstrassPoint z) = L'.weierstrassPoint (↑c * z)