Modular curves

Stream: maths

[Bryan Wang]

Is there any work currently being done to formalise modular curves in mathlib? The background being that I was wondering if it is a reasonable project (i.e. time scale not on the order of years) to formalise the Eichler-Shimura relation for modular curves.

[Kenny Lau]

@Bryan Wang yes, i'm working on elliptic curves in my personal project https://github.com/kckennylau/EllipticCurve

[Kevin Buzzard]

@Bryan Wang right now I feel the biggest tension is deciding whether to plough on with the "plane cubic" definition or try and make a working "smooth proper group scheme" definition. The advantage of the plane cubic definition is that it still gives you a path to a correct definition of elliptic curve over a scheme ("there exists an affine cover of the base over which it's iso to a nonsingular plane cubic") and then getting modular curves out of this will hopefully be pretty straightforward. This way also avoids stacky considerations. If you want to prepare for Eichler-Shimura and also help FLT then we have nothing about reduction of an elliptic curve over say the field of fractions of a complete DVR. For example no definition of good reduction, no group hom from the generic fibre to the special fibre etc.

[Bryan Wang]

Thanks! Just to clarify, when you say "plane cubic" definition, you mean the one currently in mathlib as docs#WeierstrassCurve ?

[Bryan Wang]

I am somehow vaguely reminded of that old joke about Serre's answer to the question "what is a variety?" ("integral scheme of finite type over a field") I guess this type of tension has always existed and will continue to exist in Lean..

[Kevin Buzzard]

My feelings right now are that we need to develop both the smooth proper story and the "five numbers" (aka plane cubic) story, because having the model is super-useful (e.g. Tate's algorithm). Note that we don't have alg-geom Riemann-Roch yet so moving between the two stories will be hard; right now we're talking a "Silverman-like" approach by just developing the plane cubic story.

[Bryan Wang]

ok! Re: the "Silverman approach", let me see if I get anywhere with first defining (and showing existence of) minimal Weierstrass equations, which are needed to define reduction.

[Bryan Wang]

#28115 defines minimal Weierstrass equations and the reduction of elliptic curves over the fraction field of a DVR. Any comments are appreciated, as I am still pretty new to the EllipticCurve API in mathlib!

[Kevin Buzzard]

@Adam Topaz in what generality should we have concepts such as "this plane cubic equation with coefficients in a field actually has coefficients in an integer ring"?

[David Ang]

Thanks! I'd love to review this properly but I'm stuck writing my thesis for the next month or so... Note that there was prior discussion about reduction in #maths > thoughts on elliptic curves @ 💬 but that's for the points rather than the coefficients of the curve itself

[Bryan Wang]

So I realised we didn't get back to modular curves in the end - it seems like the best way is to develop elliptic curves over schemes first and base the definition of modular curves on that?

[Chris Birkbeck]

What level modular curves would this give? Would this be Gamma_1?

[Chris Birkbeck]

It would be nice to be able to do full level N so that one can get all the other ones, like they do here

[Chris Birkbeck]

But that might be beyond what we can currently do as it probably needs some representability of moduli spaces

[Riccardo Brasca]

I think this is exactly the problem, nobody wants to do a particular case by hand if it ends up being outdated but on the other hand we are not ready for the "correct" generality.

[Kenny Lau]

(with the obvious conflict of interest being https://github.com/kckennylau/EllipticCurve) I would say that it seems a bit pointless to talk about "a moduli of elliptic curves" if we can't talk about the (correct) elliptic curves

[Chris Birkbeck]

Oh yes that is definitely a problem. I should definitely be clear, all I wanted to know is what level this approach would give. I think its worth doing even if not in the fullest level of generality.

[Chris Birkbeck]

I think we it would be nice to at least have some modular curves. If we later get the 'correct' ones then anything else can just be updated.

[Kenny Lau]

well Y1(4)(R) is Spec R[x]/(1/Δ(x),16x-1) or something like that, so we can have Y1(4) "today" :slight_smile:

[Kevin Buzzard]

I think one feasible plan is define an elliptic curve over a scheme to be "locally Y^2+...=cubic" and worry about why 1-dimensional abelian varieties have this property later. If we have Y_1(4) and Y_1(5) (which can both be done by hand) then I think we can make Y_1(N) by looking at N-torsion in universal curves.

[Kenny Lau]

that is the plan for my project linked above