The Tate curve over ℤ⟦q⟧

The Tate curve is the Weierstrass equation

E_q : y² + xy = x³ + a₄(q) x + a₆(q), a₄(q) = -5 s₃(q), a₆(q) = -(5 s₃(q) + 7 s₅(q)) / 12,

where s_k(q) = ∑_{n ≥ 1} nᵏ qⁿ / (1 - qⁿ) = ∑_{n ≥ 1} σ_k(n) qⁿ. This file defines it as a Weierstrass curve over the formal power series ring ℤ⟦q⟧. The division by 12 in a₆ is carried out on coefficients, using 12 ∣ 5 σ₃(n) + 7 σ₅(n), so no denominator is ever introduced: the curve is defined over ℤ⟦q⟧, and by WeierstrassCurve.map over R⟦q⟧ for every commutative ring R, residue characteristics 2 and 3 included. Over a complete non-archimedean field K and q ∈ Kˣ with |q| < 1 the series converge, and specialising gives the curve whose points are Kˣ / qᶻ; this file contains the formal half of that story.

The formal invariants are those of the Tate curve as an elliptic curve over the Laurent series ℤ⸨q⸩: c₄ = 1 + 240 s₃ and c₆ = -1 + 504 s₅, the discriminant is q times a unit of ℤ⟦q⟧, so that the curve is elliptic over ℤ⸨q⸩, and its j-invariant is 1 / q + 744 + ⋯ with integral coefficients.

Main definitions

• TauCeti.divisorSumSeries k: the series s_k(q) = ∑_{n ≥ 1} σ_k(n) qⁿ in ℤ⟦q⟧.
• TauCeti.tateCurve: the Tate curve, a Weierstrass curve over ℤ⟦q⟧.

Main results

• TauCeti.tateCurve_a₄ and TauCeti.twelve_mul_tateCurve_a₆: a₄ = -5 s₃ and 12 a₆ = -(5 s₃ + 7 s₅), which determine the coefficients since ℤ⟦q⟧ is torsion-free.
• TauCeti.constantCoeff_tateCurve_a₄ and TauCeti.constantCoeff_tateCurve_a₆: at q = 0 the Tate curve is the nodal cubic y² + xy = x³.
• TauCeti.tateCurve_c₄ and TauCeti.tateCurve_c₆: c₄ = 1 + 240 s₃ and c₆ = -1 + 504 s₅.
• TauCeti.order_tateCurve_Δ and TauCeti.exists_tateCurve_Δ_eq_X_mul: Δ = q · u with u a power series of constant coefficient 1, and Δ = q - 24 q² + ⋯.
• TauCeti.exists_tateCurve_j_eq: over ℤ⸨q⸩ the Tate curve is elliptic and j = q⁻¹ · J(q) with J ∈ ℤ⟦q⟧ and J = 1 + 744 q + ⋯.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, §V.3.
• J. Tate, A review of non-Archimedean elliptic functions, in Elliptic curves, modular forms, & Fermat's last theorem (Hong Kong, 1993), International Press (1995), 162–184.

noncomputable def TauCeti.tateCurve : WeierstrassCurve (PowerSeries ℤ)

The Tate curve y² + xy = x³ + a₄ x + a₆ over ℤ⟦q⟧, with a₄ = -5 s₃ and a₆ = -(5 s₃ + 7 s₅) / 12. The n-th coefficient of a₆ is -(5 σ₃(n) + 7 σ₅(n)) / 12, an integer by twelve_dvd_five_mul_sigma_three_add_seven_mul_sigma_five; use coeff_tateCurve_a₆ and twelve_mul_tateCurve_a₆ rather than the definition.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.tateCurve_a₁ : tateCurve.a₁ = 1

@[simp]

theorem TauCeti.tateCurve_a₂ : tateCurve.a₂ = 0

@[simp]

theorem TauCeti.tateCurve_a₃ : tateCurve.a₃ = 0

@[simp]

theorem TauCeti.coeff_tateCurve_a₄ (n : ℕ) : (PowerSeries.coeff n) tateCurve.a₄ = -5 * ↑((ArithmeticFunction.sigma 3) n)

@[simp]

theorem TauCeti.coeff_tateCurve_a₆ (n : ℕ) : (PowerSeries.coeff n) tateCurve.a₆ = -↑((5 * (ArithmeticFunction.sigma 3) n + 7 * (ArithmeticFunction.sigma 5) n) / 12)

The n-th coefficient of a₆ is -(5 σ₃(n) + 7 σ₅(n)) / 12.

theorem TauCeti.twelve_mul_coeff_tateCurve_a₆ (n : ℕ) : 12 * (PowerSeries.coeff n) tateCurve.a₆ = -(5 * ↑((ArithmeticFunction.sigma 3) n) + 7 * ↑((ArithmeticFunction.sigma 5) n))

The coefficients of a₆: 12 · [qⁿ] a₆ = -(5 σ₃(n) + 7 σ₅(n)).

theorem TauCeti.tateCurve_a₄ : tateCurve.a₄ = -5 * divisorSumSeries 3

a₄ = -5 s₃.

@[simp]

theorem TauCeti.twelve_mul_tateCurve_a₆ : 12 * tateCurve.a₆ = -(5 * divisorSumSeries 3 + 7 * divisorSumSeries 5)

12 a₆ = -(5 s₃ + 7 s₅).

@[simp]

theorem TauCeti.tateCurve_c₄ : tateCurve.c₄ = 1 + 240 * divisorSumSeries 3

c₄ = 1 + 240 s₃, the normalised Eisenstein series of weight 4.

@[simp]

theorem TauCeti.tateCurve_c₆ : tateCurve.c₆ = -1 + 504 * divisorSumSeries 5

c₆ = -1 + 504 s₅, minus the normalised Eisenstein series of weight 6.

@[simp]

theorem TauCeti.constantCoeff_tateCurve_a₄ : PowerSeries.constantCoeff tateCurve.a₄ = 0

a₄ vanishes at q = 0.

@[simp]

theorem TauCeti.constantCoeff_tateCurve_a₆ : PowerSeries.constantCoeff tateCurve.a₆ = 0

a₆ vanishes at q = 0.

@[simp]

theorem TauCeti.constantCoeff_tateCurve_Δ : PowerSeries.constantCoeff tateCurve.Δ = 0

Δ vanishes at q = 0.

@[simp]

theorem TauCeti.coeff_one_tateCurve_Δ : (PowerSeries.coeff 1) tateCurve.Δ = 1

The q-coefficient of Δ is 1.

@[simp]

theorem TauCeti.coeff_two_tateCurve_Δ : (PowerSeries.coeff 2) tateCurve.Δ = -24

The q²-coefficient of Δ is -24.

@[simp]

theorem TauCeti.order_tateCurve_Δ : tateCurve.Δ.order = 1

v(Δ) = v(q): the discriminant of the Tate curve has order 1 in q.

theorem TauCeti.exists_tateCurve_Δ_eq_X_mul : ∃ (u : PowerSeries ℤ), PowerSeries.constantCoeff u = 1 ∧ IsUnit u ∧ tateCurve.Δ = PowerSeries.X * u

The discriminant of the Tate curve is q times a unit: Δ = q · u with u ∈ ℤ⟦q⟧ of constant coefficient 1, hence invertible in ℤ⟦q⟧.

instance TauCeti.isElliptic_baseChange_tateCurve : (tateCurve.baseChange (LaurentSeries ℤ)).IsElliptic

Over the Laurent series ℤ⸨q⸩, where q is invertible, the Tate curve is elliptic.

theorem TauCeti.exists_tateCurve_j_eq : ∃ (J : PowerSeries ℤ), PowerSeries.constantCoeff J = 1 ∧ (PowerSeries.coeff 1) J = 744 ∧ (tateCurve.baseChange (LaurentSeries ℤ)).j = (HahnSeries.single (-1)) 1 * (HahnSeries.ofPowerSeries ℤ ℤ) J

j(q) = 1 / q + 744 + ⋯: over ℤ⸨q⸩ the j-invariant of the Tate curve is q⁻¹ · J(q) for a power series J ∈ ℤ⟦q⟧ with J = 1 + 744 q + ⋯. In particular j has a simple pole at q = 0 and integral coefficients.