Eisenstein series

Stream: maths

[Chris Birkbeck]

So I have now finished porting some Eisenstein series things I had in Lean 3. The new repo is here. So now the task is to start moving this to mathlib. Currently the definition of Eisenstein series is quite basic:

/-- The function on `ℤ × ℤ` whose sum defines an Eisenstein series.-/
def eise (k : ℤ) (z : ℍ) : ℤ × ℤ → ℂ := fun x => 1 / (x.1 * z.1 + x.2) ^ k

/-- The function defining the Eisenstein series of weight `k : ℤ` -/
def Eisenstein_tsum (k : ℤ) : ℍ → ℂ := fun z => ∑' x : ℤ × ℤ, eise k z x

For these definitions I can show that it defines a modular form (of level 1), have the expected q-expansion and $G_4$ is not identically zero. The question is, what should mathlibs definition of Eisenstein series be? This is far from the most general definition, but a realistic generalization would be as a function on lattices in $\mathbb{C}$, but I don't know the best way to define these lattices (and I'm not sure if we already have them for say, complex elliptic curves).

There is another issue, which is that defined like this, for weight 2, the function you get is the zero function (because the infinite sum is not absolutely convergent (i.e. summable in Lean )). But $G_2$ is a non-trivial interesting function. So if we defined them via the q-expansions the definition would work for weight 2 (but at weight 2 would not define a modular form (of level 1)).

So I wanted to see what opinions/ideas people here have. Should the definition be (1) in terms of lattices (or something even more general?) (2) keep the current one (with $G_2$ needing to be a special case), or (3) instead use q-expansions (and be happy that with this definition not all Eisenstein series are modular forms). (sorry I don't know how to make a poll)

[Kevin Buzzard]

These are only level 1 Eisenstein series; more generally people sum over x in some congruence class modulo N.

[Chris Birkbeck]

Yes that's a good point. For other levels, I was thinking of using subseries of the definition above.

[Eric Rodriguez]

I think $G_2$ as a separate definition seems sensible; this seems more extensible to other levels. Why not just start with some more general definition (e.g. I found this in math​.se, not sure if it's "the" most general defn) and maybe make an abbrev for the level 1 case? It doesn't seem to me that proving basic things about this specific more general notion are much harder, for example.

Defining things via the q-expansion doesn't seem the greatest, IMO, unless there's a very generalised way to arrive at the q-expansion

[Chris Birkbeck]

Do you mean as relating to cusps? If so that's like what Kevin suggested, which I think is a reasonable generalization (and hopefully not too much work given what I've done)

[Kevin Buzzard]

If you care about forms with character then another approach is having $\chi$ and $\psi$ Dirichlet characters of level $L$ and $M$, $k\geq3$ an integer, $t$ a positive integer, and then defining $E_k(z;\chi,\psi,t)$ to be the sum of $\chi(c)\overline{\psi}(d)(cMtz+d)^{-k}$ over all $(c,d)\not=(0,0).$ You get a basis for Eisenstein series of level $\Gamma_1(N)$ with these (restrict to $\chi,\psi$ primitive and $MLt\mid N.$)

[Alex Kontorovich]

Do we have Riemann-Roch? How feasible might it be to define the cuspidal subspace of modular forms of any given weight/level/character? (In which case the Eisenstein series could be defined as things spanning the non-cuspidal space... Of course it would be better to also have explicit access to their Fourier coefficients...) Do we also have non-holomorphic Eisenstein series? (Which in many ways are more useful, e.g., in Rankin-Selberg, converse theorems, etc.) I really struggled with this when I thought about it a while ago, because mathlib really wants the most general form of everything, so you can't even get started. You wouldn't want to do, say, the GL(2) level 1 non-holomorphic Eisenstein series (and all the applications that would come as a result...), because you should really be doing Langlands Eisenstein series with arbitrary parabolics twisted by Maass forms, etc etc...?

[Kevin Buzzard]

We don't even have algebraic curves and whilst we have Riemann surfaces we don't really have any theorems about them. So no Riemann-Rochs yet (there are two Riemann-Roch theorems, an algebraic geometry one and a differential geometry one).

[Adam Topaz]

Alex Kontorovich said:

Do we have Riemann-Roch?

No :sad: . But people have been talking about it for a while :smile:

[Ruben Van de Velde]

I've heard "Riemann-Roch" quite a few times here on zulip, but I don't know what happened in the end

[Adam Topaz]

I'm under the impression that formalizing the proof in Serre's book on class fields is very doable with current mathlib.

[Kevin Buzzard]

Regarding "correct generality" -- I realised a while ago that "correct generality" doesn't necessarily mean "some mathematician wrote down a more general object so we can't have the special object". For example one would then argue that we can't have elliptic curves until we have abelian varieties, which we can't have until we have group varieties etc etc. But something is fishy about this argument: it's well known that proving associativity for elliptic curves is hard but proving associativity for abelian varieties is trivial because they're group varieties. So something funny is going on :-) I interpret "correct generality" now as "if the object has a user base then make that object, and who cares if it's a special case of a much more general object". In particular we're allowed to make modular forms even though they're a special case of automorphic forms on a connected reductive group over a global field.

[Alex Kontorovich]

Ok I'm really glad to hear this perspective! :)

[Chris Birkbeck]

Alex Kontorovich said:

Do we have Riemann-Roch? How feasible might it be to define the cuspidal subspace of modular forms of any given weight/level/character? (In which case the Eisenstein series could be defined as things spanning the non-cuspidal space... Of course it would be better to also have explicit access to their Fourier coefficients...) Do we also have non-holomorphic Eisenstein series? (Which in many ways are more useful, e.g., in Rankin-Selberg, converse theorems, etc.) I really struggled with this when I thought about it a while ago, because mathlib really wants the most general form of everything, so you can't even get started. You wouldn't want to do, say, the GL(2) level 1 non-holomorphic Eisenstein series (and all the applications that would come as a result...), because you should really be doing Langlands Eisenstein series with arbitrary parabolics twisted by Maass forms, etc etc...?

We'll we do have the space of cuspforms, but we don't have any finite dimensionality results for any of the spaces (which we could do without RR, but is still annoying). I agree that its hard to decide and what the level of generality to use is, but as Kevin says, we already didn't define general automorphic forms. That said, I think we definitely should define them for more general levels at least!

[Alex Kontorovich]

I'm assuming we have nothing approximating a trace formula, is that right? So no Maass forms... (Even on SL(2,Z)...)

[Chris Birkbeck]

Alex Kontorovich said:

I'm assuming we have nothing approximating a trace formula, is that right? So no Maass forms... (Even on SL(2,Z)...)

Not that I'm aware of.

[Kevin Buzzard]

I think Maass forms would be an excellent test of the multivariable calculus library because you'll have to write down "...is an eigenvalue for the Laplacian" and the analysts are very reluctant to give people access to things like partial d/dx because they don't like picking a basis :-) Everything else will be the same as for the modular form case.

[Kevin Buzzard]

But for the Laplacian it would be better to work more conceptually and this might involve some Lie algebras etc.

[Mario Carneiro]

Kevin Buzzard said:

Regarding "correct generality" -- I realised a while ago that "correct generality" doesn't necessarily mean "some mathematician wrote down a more general object so we can't have the special object". For example one would then argue that we can't have elliptic curves until we have abelian varieties, which we can't have until we have group varieties etc etc.

There is another term I like to use for this, which is "trivial generalization". The idea is, if you can remove a hypothesis to the theorem without breaking the proof, do so; if you can weaken a typeclass assumption without any proof changes, do it. If it can be proven in a more general setting with a more complicated proof (non-trivial generalization), you are allowed but not required to do it. If the more general theorem statement is not directly usable in all cases where the original was, then consider adding the specific theorem statement anyway. (This last sentence explains most large scale "generalizations" like "elliptic curves are abelian varieties".)

[Patrick Massot]

The case of elliptic curves is a bit misleading because a crucial point is there are several equivalent definitions whose equivalence is highly non obvious. As Kevin pointed out, associativity of the group law is trivial if you get to choose the definition.

[Kevin Buzzard]

Sounds like a good time to mention Riemann-Roch again. If we mention it enough times maybe someone will prove it :-)

[Yaël Dillies]

There's also a heavy imports argument to the generality story: many combinatorial inequalities can be generalised to continuous ones but:

1. If we deduced them from the continuous ones, we would introduce very heavy imports in a theory which is otherwise elementary (and which is possibly itself fed into other theories)
2. We want to develop the tools needed for the elementary proof anyway, as those will likely get reused later

[Moritz Doll]

Kevin Buzzard said:

I think Maass forms would be an excellent test of the multivariable calculus library because you'll have to write down "...is an eigenvalue for the Laplacian" and the analysts are very reluctant to give people access to things like partial d/dx because they don't like picking a basis :-) Everything else will be the same as for the modular form case.

For the Laplacian you really don't need partial derivatives. I would guess that the most natural definition is Δ = d^* d (for functions), but that relies on a bunch of differential geometry that we don't have yet. For the hyperbolic plane you can easily just write the Laplacian by hand with the things we already have. For eigenvalues there is no big issue with the domain (thanks to elliptic regularity all eigenvectors are smooth), but if you want to do actual spectral theory, then you need Sobolev spaces to say that the Laplacian is self-adjoint and this will be a huge pain.

[Moritz Doll]

technically speaking one has that the Laplacian on complete manifolds is essentially self-adjoint, which means that there is exactly one self-adjoint extension (you start with compactly supported smooth functions), but without Sobolev spaces one has no good characterization of the domain.

[Patrick Massot]

I heard rumors that Sobolev spaced are coming.