November update

Stream: FLT

[Kevin Buzzard]

OK so we're one month into the FLT project and basically my life is still hugely disrupted by the fact that I said yes to a lot of things earlier in the year, meaning that I just got back from 10 days in California, and in 10 days' time I'm off to run a workshop on alg geom in Lean in Durham, and then I'm going to Pittsburgh. I've now started saying no to everything.

One thing I've realised is that there seems to be a major difference between this project and other projects which I've been involved with, and that is that there are people at Imperial and elsewhere who are working on contributions to FLT as part of their undergraduate or PhD degree, and this really complicates things: these people typically do not want other people collaborating with them. As a result I am not able to sketch out what they are doing as part of the blueprint. In short, there is far more activity on the FLT project than is publically apparent, but a bunch of it is going on in private.

One thing I have realised is that I do have a clear long-term goal, namely to prove a modularity lifting theorem (this is what I promised EPSRC), and a pithy way of summarising this that there are two rings R and T, and we need to prove that they're isomorphic (an "R=T theorem"). This long-term goal naturally leads us to several shorter-term goals, namely (1) define R; (2) define T; (3) define the map from R to T. The hard work is (4) prove that it's an isomorphism, but this can wait. Currently (1) is happening in private but (2) is happening in public, and (3) is going to wait until we've made more progress on (1) and (2).

The ring T is a Hecke algebra, defined as a subalgebra of the linear endomorphisms of a certain space of automorphic forms. These spaces of forms are "quaternionic" analogues of spaces of classical modular forms, however their definition involves no analysis so proving that the spaces are finite-dimensional involves no integrals. It does however involve a detailed study of the adeles of a number field, and unfortunately right now we don't even have the definition of the adeles of a number field. One key result we need is that the adeles are locally compact; this is the main theorem of @Salvatore Mercuri 's repo here and, rather than making this repo a dependency of FLT I think it's better to get it into mathlib. Salvatore has a bunch of PRs stacked upon each other here; one way people could help would be by reviewing them. The moment we have the definition of the adele ring we will be able to start proving basic things about it.

Finally let me talk about miniprojects. I have realised that there is still plenty of material which we need for FLT but (in my opinion at least) clearly belongs in mathlib. I have hence started writing quite self-contained chapters of the blueprint and I'm calling them miniprojects. The first miniproject, on Frobenius elements, has been a success: the main result which we need is now a sorry-free WIP PR to mathlib by Thomas Browning. I have thus launched two more miniprojects: one on adeles and one on quaternion algebras. The latter is mostly blocked by the fact that we're still missing the definition of the adele ring of a number field, but the former is up and running, and I've just opened an "outstanding tasks"-like thread for it here and also created five new tasks on the project dashboard. You can read about project dashboards here and let me again thank Pietro Monticone for setting up all the infrastructure. As far as I am concerned, the adele miniproject is a success once it has size 0, i.e. it's been upstreamed to mathlib.

Regarding the blueprint graph: I now have different graphs per chapter, and in particular each miniproject has its own graph. This was because the full blueprint graph became massive and it was very difficult to see what was going on as miniprojects proceeded (indeed it was actually quite difficult to find each miniproject graph within the full blueprint graph when it was all one graph, and furthermore the miniproject graphs would keep jumping around). I now see that I've done quite a poor job on the adele miniproject blueprint graph, but you can keep track of how it's progressing on the project dashboard.

[Andrew Yang]

As pointed out by someone else somewhere else, I think it is still useful to have a list of what is being worked on even if they are private? Or are they so private that their existence itself is a secret?
And it would be even more useful if the exact statement of the theorem is described so other people can depend on it as a axiom in the time being.

[Shreyas Srinivas]

The project dashboard should help you with that

[Kevin Buzzard]

David Angdinata is working on division polynomials, Javier Lopez is working on defining R, Alex Brodbelt is working on the classification of the finite subgroups of PSL_2(F_p-bar), you're working on patching, Yujie Wang is working on Weierstrass P, Edison Xie is working on Brauer groups, and there are other people who I'm still in discussion with.

[Shreyas Srinivas]

You can create a separate column for claimed mini projects

[Ruben Van de Velde]

Kevin Buzzard said:

One thing I have realised is that I do have a clear long-term goal, namely to prove a modularity lifting theorem (this is what I promised EPSRC), and a pithy way of summarising this that there are two rings R and T, and we need to prove that they're isomorphic (an "R=T theorem"). This long-term goal naturally leads us to several shorter-term goals, namely (1) define R; (2) define T; (3) define the map from R to T. The hard work is (4) prove that it's an isomorphism, but this can wait. Currently (1) is happening in private but (2) is happening in public, and (3) is going to wait until we've made more progress on (1) and (2).

This is the kind of thing that would be great to have in the blueprint, IMO. (I'm not even sure where it would go, though - I've seen you mention "R=T" a number of times before, but if it's in the blueprint, I'm overlooking it)

[Riccardo Brasca]

I am more than happy to have a look at all the PRs you need. Please feel free to ask my review

[Riccardo Brasca]

@Salvatore Mercuri

[Kevin Buzzard]

Ruben Van de Velde said:

This is the kind of thing that would be great to have in the blueprint, IMO.

So I started to write technical material explaining how the proof went, but then I realised that it was in some sense impossible to blueprintize it because we were missing so so many definitions. It's this chapter here and as you can see at the end, I somehow ran out of enthusiasm because was impossible to even state anything in Lean.

[Ruben Van de Velde]

Yeah, I didn't expect there would be lean code - that'd pretty much be the goal of that part of the project

[Kevin Buzzard]

I've started working on a (LaTeX) definition of T

[Chris Birkbeck]

I started defining a T for the modular forms stuff over the summer (using Shimura's definition of Hecke rings) but it might not be exactly what you want for this.

[Kevin Buzzard]

I now think I know what I want, thanks to thinking about this today. I only care about forms of level Gamma_0(N) or Gamma_1(N) where N is a squarefree ideal of O_F, and I only care about the Hecke algebra generated by T_p for p prime to N and U_{p,x} := (x 0; 0 1) at p when p divides N. In particular I need to be careful not to include too many Hecke operators because I want to maintain commutativity.