Weierstrass P-function

Stream: FLT

[Kevin Buzzard]

Just to give an update on FLT: although the grant doesn't kick in until October, I am currently working on the blueprint (in private) and the project is definitely going public in April (by which I probably mean "the very end of April" -- basically the more material I work on in private the better the project looks at release).

Over the last couple of weeks I've been working on the initial reductions of FLT to questions about elliptic curves, and I am not entirely surprised to discover that I need the theory of the Weierstrass P-function. In fact I can be completely precise about what I need; it is a purely algebraic statement which I write down here (mathoverflow). But I think that question is the wrong question; I think that the question shouldn't be "can we avoid using the Weierstrass P-function in a proof of FLT", I think that instead the conclusion should be "shall we use FLT as motivation to define the Weierstrass P-function?".

So if anyone is looking for an FLT-related project then I can offer the following: (1) define the meromorphic function $P(z,\tau)$; (2) prove the standard relationship between $P$ and $dP/dz$, namely $P'^2=4P^3+a_4P+a_6$ (@Chris Birkbeck do you have $E_4$ and $E_6$ somewhere?) and (3) compute the power series representing $P$ as a function of $q:=e^{2\pi i\tau}$ and $u:=e^{2\pi i z}.$

[Chris Birkbeck]

We do have E4 and E6, the PRs showing they are mod forms (i.e. holomorphic and bounded at infinity are in the queue). I also have their q-expansions done, also needing PRing. After next week I should have some time to get these PRs done hopefully.

[Chris Birkbeck]

I'm also interested in having these defined for the modular forms stuff, so I am happy to help work on this :)

[Kevin Buzzard]

I'm sorry I can't supply a coherent blueprint at this point; on the other hand I suspect that people interested in this sort of thing will know well where to look. One reference for the basics is Silverman "arithmetic of elliptic curves", section VI.3, and all this stuff should really just go directly into mathlib.

[Chris Birkbeck]

Diamond--Shurman also has some bits of this.

[Ruben Van de Velde]

(#10377 just caught a trivial merge conflict)

[Alex Kontorovich]

In case it may help, I just recently recorded some lectures on the construction of P, E4, E6, and these properties... see Lecture 30 here: https://sites.math.rutgers.edu/~alexk/2020F503/lectures.html

[Kevin Buzzard]

Chris Birkbeck said:

We do have E4 and E6, the PRs showing they are mod forms (i.e. holomorphic and bounded at infinity are in the queue). I also have their q-expansions done, also needing PRing. After next week I should have some time to get these PRs done hopefully.

How are you making the sum of the k-1st powers of the divisors of a positive natural?

[Chris Birkbeck]

I don't need them to be a positive natural, since its only showing up in the q-expansion whose terms are complex numbers so they get coerced automatically from Nat.

[Chris Birkbeck]

basically all the things I have look like

theorem Eisenstein_Series_q_expansion_Bernoulli (k : ℕ) (hk : 3 ≤ (k : ℤ))
(hk2 : Even k) (z : ℍ) : (eisensteinSeriesOfWt_ k) z =
   2 * ((-1) ^ (k / 2 + 1) * 2 ^ (2 * (k / 2) - 1) * π ^ k * bernoulli k / k !) +
     2 * ((-2 * ↑π * I) ^ k / (k - 1)!) *
       ∑' n : ℕ+, sigma (k - 1) n * Complex.exp (2 * ↑π * I * z * n) := by...

(ignore the old names)

[Kevin Buzzard]

Is this your own sigma?

[Michael Stoll]

There is docs#ArithmeticFunction.sigma .

[Chris Birkbeck]

No its the one we have

[Chris Birkbeck]

Why do you want them to be positive naturals and not just naturals?

[Kevin Buzzard]

Here is the algebraic result I want, modulo the problem that I am not sure of a computationally efficient way to proceed to see if I can check a few more terms of the power series.

import Mathlib.RingTheory.PowerSeries.Basic
import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.NumberTheory.Divisors

/-

# An algebraic identity



## Uniformising elliptic curves

Every (algebro-geometric) elliptic curve over ℂ is (as compact Riemann surface and
abelian Lie group), `ℂ` modulo a lattice; the proof of this uses integration. Note
that you can scale the lattice to make it of the form `Λ(τ) := ℤ + τℤ` for some `τ`
in the upper half-plane, without changing the isomorphism class of the curve.

We can form this quotient `ℂ / Λ(τ)` via a two-stage process: we first quotient out
by `ℤ` and then by `τℤ`. Let's analyse both steps in turn.

## Quotienting out by `ℤ`.

The additive quotient `ℂ / ℤ` can be identified with the multiplicative group `ℂˣ`, via the
function `z ↦ u := e ^ {2πiz}`.

Note that at the point the notation for the group law changed, an interesting power series
appeared. Indeed, modulo the "twist" `2πi`, the dictionary is a function `e^x`. This is
`∑ₙ(1/n!)x^n`, the generating function of the sequence whose `n`'th term is the size of the
algebraic stack of sets of size `n`. The theorem `e^(x+y)=e^x*e^y` can be proved by
translating it into a statement about power series and verifying it using the binomial theorem.

Conversely, sometimes it's possible to prove identities in power series involving `e^x` using
complex analysis. For example, proving that `log(e^x)=x` for `x` close to `0`, just by
using power series, turns into a real mess; it is easier to define the complex log in a
neighbourhood of 1, prove the result using analysis and deduce the algebraic result by
working out the power series of everything.

The main conjecture of this file can be proved in the same way; it is a combinatorial
identity in the multiplicative `(q,u)` coordinates defined entirely over the rationals
(and even over the integers in some precise sense), which can be proved by observing that it
suffices to prove it for all pairs of complex numbers in a small ball and then deduce it from
a standard fact relating `P'²` and `4P³`, via the result that a holomorphic
function on a compact Riemann surface which vanishes at some point must be identically zero.

## Quotienting out by `τℤ`

The second stage is to quotient out `ℂˣ` by the subgroup `<q>` generated by `q := e ^ {2πiτ}`.
At this point we are regarding `q` as fixed, and we would like to write down meromorphic functions
`f` in one nonzero complex variable `u` with the property that they satisfy `f(qu)=f(u)`
for all `u` and thus descend to the curve. One example is `F_q(u) := ∑_{n∈ℤ} uq^n/(1-uq^n)^2`
(which for a fixed `q` converges for all non-zero `u` other than those in the subgroup `<q>`,
where there is a double pole.

Expanding `F_q(u)` as a power series in `q` (deal with the three cases `n<0,n=0,n>0` separately)
we get `F_q(u) = u/(1-u)^2+∑_{n>=1}(uq^n/(1-uq^n)^2+u^{-1}q^n/(1-u^{-1}q^n)^2),`
This descends to a meromorphic function on `ℂˣ/<q>=ℂ/Λ(τ)` with a pole of order 2 at `z=0`
and no other poles. We also know that the Weierstrass P-function `P_τ(z)`, considered as a function
on the curve, has a pole of order 2 at `0` and no other poles, so some linear combination
of these functions will have a pole of order at most 1 at `0` and no other poles.
An explicit analysis of the power series in `z` shows that the
difference `P_τ(z)-(2πi)²F_q(u)`, or if you like `P_τ(z) - (2πi)²F_{2^{2πiq}}(e^{2πiz})`,
is the linear combination where the order 2 poles cancel, and one can check explicitly
that in fact the order 1 poles cancel too, so this difference is holomorphic everywhere
and must thus be constant. An explicit calculation gives that this constaint
is `- 1/12 + 2∑_{n≥1}q^n/(1-q^n)^2`, sometimes known as `(-1/12)*E₂`. Note of course that
this is a function of `q` only.

## A proof of the algebraic identity

Step 1) Prove the standard result about X=P and Y=dP/dz satisfying a cubic equation
`Y^2=4X^3+g₄X+g₆` where `g₄` and `g₆` are Eisenstein series.

Step 2) Translate into a statement involving `F`, with `u` and `q` variables,
then note that all the `π`s cancel and what comes out is the result we seek.

Step 3) Argue that a certain meromorphic function of two variables being zero at lots
of complex points implies that it must be identically zero.

## Notation

Notation plays an important part in this game, where there are several copies of the complex
numbers floating around. `τ` will be in the upper half plane and it will parametrise the
lattice `Λ(τ)`. `z` will be the complex number which is a parameter for the `ℂ` which gets
quotiented out by `Λ(τ)`. `u := e^{2πiz}` is the parameter on `ℂˣ`, and `q := e^{2πiτ}` will
be a complex number with `0<|q|<1`.

-/

namespace UniversalEllipticCurve.AlgebraicUniformisation
-- The point of this namespace is simply to state the combinatorial identity.

suppress_compilation -- maybe should be removed

open Polynomial PowerSeries  -- to get `R[X]` and `R⟦X⟧` notation

-- let `K` be `ℚ(u)`, the field of fractions of `ℤ[u]`.
variable {K : Type} [Field K] [Algebra ℤ[X] K] [IsFractionRing ℤ[X] K]
-- When we say `u` we mean the one in `K`

abbrev u : K := algebraMap ℤ[X] K X

open BigOperators Finset -- to get `∑` notation and `range`

-- Can I rely on the fact that that sum will be 0 if n is 0?
abbrev s3 := PowerSeries.mk (fun n ↦ ∑ i in n.divisors, (i : K)^3)

-- it's true
example : PowerSeries.coeff K 0 s3 = 0 := by
  simp

abbrev s5 := PowerSeries.mk (fun n ↦ ∑ i in n.divisors, (i : K)^5)

-- check junk value
example : PowerSeries.coeff K 0 s5 = 0 := by simp

scoped notation:9001 R "⟦q⟧" => PowerSeries R

abbrev a4 : K⟦q⟧ := PowerSeries.C K (-5 : K) * s3

-- remark: just like the others above, this descends to ℤ⟦q⟧
abbrev a6 : K⟦q⟧ := (PowerSeries.C K (-5/12 : K) * s3 + PowerSeries.C K (-7/12 : K) * s5)

-- this one really is now in `K⟦q⟧`, it involves `u`. It is related to the power series
-- of the Weierstraß P-function.
abbrev X₀ : K⟦q⟧ := PowerSeries.C K (u / (1 - u)^2) +
  PowerSeries.mk (fun n ↦ ∑ d in n.divisors, (d : K) * (u^d + u⁻¹^d - 2))

example : PowerSeries.coeff K 0 X₀ = (u / (1 - u)^2) := by simp

-- This is also a true power series, related to the derivative of P.
abbrev Y₀ : K⟦q⟧ := PowerSeries.C K (u^2 / (1 - u)^3) +
  PowerSeries.mk (fun n ↦ ∑ d in n.divisors, ((d : K) * (d - 1) / 2 * u ^ d -
    (d : K) * (d + 1) / 2 * u⁻¹ ^ d + d))

-- if I got it right then

abbrev ShouldBeZeroIfICopiedCorrectly : K⟦q⟧ := Y₀^2+X₀*Y₀-X₀^3-a4*X₀-a6
-- Proof: see Silverman 2 theorem V.1.1

-- the main goal
theorem uniformisation : (ShouldBeZeroIfICopiedCorrectly : K⟦q⟧) = 0 := sorry

-- missing?
@[simp] lemma PowerSeries.constantCoeff_mk {f : ℕ → K} :
    PowerSeries.constantCoeff K (PowerSeries.mk f) = f 0 := rfl

-- unit tests

example : PowerSeries.coeff K 0 (ShouldBeZeroIfICopiedCorrectly) = 0 := by
  have foo : (1 - u : K) ≠ 0 := sorry -- not sure which tactic to use
  field_simp
  ring

example : PowerSeries.coeff K 1 (ShouldBeZeroIfICopiedCorrectly) = 0 := by
  simp
  -- not sure I should be solving this with simp lemmas any more
  sorry

/- Can we get up to ten like Pari does in a fraction of a second?

```pari
q
u
s3=sum(n=1,10,sigma(n,3)*q^n)+O(q^11)
s5=sum(n=1,10,sigma(n,5)*q^n)+O(q^11)
a4=-5*s3
a6=-(5*s3+7*s5)/12
X=u/(1-u)^2+sum(n=1,10,sumdiv(n,d,d*(u^d+u^(-d)-2))*q^n)+O(q^11)
Y=u^2/(1-u)^3+sum(n=1,10,sumdiv(n,d,d*(d-1)/2*u^d-d*(d+1)/2*u^(-d)+d)*q^n)+O(q^11)
Y^2+X*Y-X^3-a4*X-a6

The result is O(q^11) i.e. zero up until degree 11 at least.
-/

end UniversalEllipticCurve.AlgebraicUniformisation

[Kevin Buzzard]

Chris Birkbeck said:

No its the one we have

sigma.png

Well that didn't go well (it's what I did before I asked)

[Joël Riou]

I am not able to fully understand the relation, but is not it possible to relate the expected differential equation to the identities obtained by Ramanujan in On certain arithmetical functions, Transaction of the Cambridge Philosophical Society, XXII, No. 9, 1916, 159--184. (The series s3 and s5 are closely related to the series denoted Q and R in the paper, and there is a remark about the expansion of the Weierstrass function.)