Introduction + algebraic/arithmetic geometry

Stream: new members

[Nathanial Lowry]

Hey all! My name is Nathan; I'm a third year PhD student at IU Bloomington. I work in algebraic and arithmetic geometry, and I've recently become interested in Lean. I've done the natural numbers game and the Lean tutorial, and I figured the best way to get started was the just jump right in! I'd like to help implement some facts about elliptic curves. A reasonable amount of progress can be made by simply doing algebraic manipulations with Weierstrass equations, but to really do it justice, one needs a fair amount of algebraic geometry machinery, e.g. curve/function field duality, divisors, Riemann-Roch, etc. It looks like some scheme theory has been implemented, but there's certainly a lot to do.

Any advice on how to get started or other resources would be greatly appreciated!

[Kevin Buzzard]

There's a group of people at Imperial working on Mordell-Weil. I suspect you'd be welcome to join them or to get ideas from them about related things to do next. @David Ang ?

[Arthur Paulino]

Welcome!!
The community website has a lot of good material on how to get started. In particular, the "Documentation" and "Contributing" sections of the left menu may offer some practical guidance :+1:

[Kevin Buzzard]

I think the plan is group cohomology, Galois cohomology, Mordell-Weil, Tate-Shafarevich and Selmer groups.

[Kevin Buzzard]

Riemann-Roch is a long way off because we don't have sheaf cohomology for schemes, you could think about that but it's a bit of a harsh project for a beginner.

[David Ang]

@Nathanial Lowry Welcome! Here is the current status of Mordell-Weil: https://github.com/leanprover-community/mathlib/blob/mordell_weil/src/algebraic_geometry/EllipticCurve/mordell_weil.lean

[David Ang]

Indeed, currently the main block is associativity of the group law because we don't have Riemann-Roch, but we also need some theory of local fields which I suspect should be a more feasible as a first project?

[David Ang]

I believe someone else is working on group and Galois cohomology, and once those are done, things like Selmer groups should be immediate (assuming associativity of course)

[Kevin Buzzard]

A theory of local fields might be a really cool first project.

[Nathanial Lowry]

Great! I took a class using Serre's local fields last year, so that's still pretty fresh in my mind

[Riccardo Brasca]

If you are in number theory you may be interested in the flt-regular project (Fermat last theorem for regular primes). Any contribution is very welcome!

[Adam Topaz]

Nathanial Lowry said:

Great! I took a class using Serre's local fields last year, so that's still pretty fresh in my mind

Great idea!
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Krull.20topology.20on.20Galois.20groups/near/270762221

[Kevin Buzzard]

My post-doc @María Inés de Frutos Fernández just defined the adeles and ideles, and stated the main theorem of global class field theory; one target could be stating the corresponding local theorem so we could have local-global compatibility. Of course this will be a lot of work, e.g. you'd have to prove that the completion of a number field at a prime was a local field etc.

[David Ang]

Do we have the definition of a local field anywhere? What’s the current status?

[Kevin Buzzard]

The current status is that a few days ago Adam proposed that "we use Serre's definition, whatever it is" and since then probably nobody did anything.

[Kevin Buzzard]

Serre starts with DVRs and Dedekind domains, both of which we have, although I strongly suspect that he proves lemmas that we don't have. We don't have Frobenius elements in Galois groups AFAIK. Chapter 2: we have Haar measure and completion. We don't have anything about finite extensions AFAIK, or structure of complete DVRs, although we do have Witt vectors. It would be interesting to fill in the remaining holes in the first two chapters although this would be a lot of work. I don't think he's mentioned the phrase "local field" yet!

[Junyan Xu]

I learned local class field theory via central simple algebras (which seems not in mathlib) at IUB from Darrell Haile using Falko Lorenz's Algebra, Volume II (which I think is a very nice reference), but he has now retired.