done: Adele, Haar character and Fujisaki miniprojects

Stream: FLT

[Kevin Buzzard]

OK with all the recent PRs merged, we have a sorry-free NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset: if $K$ is a number field and $D$ is finite-dimensional central simple $K$-algebra which is a division algebra, then $D^\times\backslash(D\otimes_K\mathbb{A}_K^f)^\times$ is compact, where $\mathbb{A}_K^f$ is the finite adeles of $K$, and thus if $U\subseteq(D\otimes_K\mathbb{A}_K^f)^\times$ is an open subgroup then the double coset space $D^\times\backslash(D\otimes_K\mathbb{A}_K^f)^\times/U$ is finite. If $K$ is totally real and $D$ is totally definite then weight 2 level $U$ automorphic forms for $D$ over $K$ are functions from this finite set to the complexes, so in particular they're finite-dimensional.

All of this was known in the 1960s, let alone the 1980s, so why did we do this? There were lots of reasons: firstly, I wanted to begin the project by working on something which many people could contribute to as opposed to just people who were experts in $p$-adic Galois representations. Secondly I felt that the theory of adeles was worth developing in mathlib; ultimately we (by which I mean the community) should be doing Tate's thesis, and I am hoping that a bunch of the machinery we developed here will be helpful there. Thirdly, I gave a course on FLT last year and I wanted to make the material accessible to more than just number theorists so I lectured on this material and it just felt natural to then get it over the line.

So what happens now going forwards? I think this might make a nice paper, so that's one thing. There is also the complex question of how to get some of this stuff into mathlib; FLT's Mathlib directory now stands at 548K and much of it is the background for this finiteness result. The stuff in the Mathlib directory is stuff which people felt was definitely mathlib-appropriate at the time. Quite how we're going to get it into mathlib I don't know but this problem needs to be solved.

Another thing which I don't really know the answer to is this: the blueprint now comprises of several independent projects. There's the main top-down FLT project (currently chapters 2 to 3 but a lot more will be appearing soon because in 10 days' time I start lecturing on this stuff, and the blueprint will be my lecture notes). There's a self-contained write-up of the existence of Frobenius elements (chapter 8). There's the proof above (chapters 9-11). But most of these things are not really involved in the proof of FLT; most of these things are just standard stuff known to graduate students in the area. I have decided that really I would like the blueprint to represent "FLT modulo 1980s" and so basically most of what we have there right now doesn't fit into my vision of the blueprint at all. I don't really know what to do about this. I almost feel like I should break things off and start other repos with the proofs; the only other alternative I can think of right now is to change the blueprint software so I can have a multi-chapter "main" branch, and other multi-chapter "subproject" branches with different graphs. Right now I think my only choices are "one blueprint per project" (too few blueprints) and "one blueprint per chapter" (the current choice, which is too many). I think that in the short term I am simply going to switch back to one blueprint per project and then delete a bunch of the completed chapters, so there will be fully-compiling LaTeX correpsonding to fully-compiling Lean code but no way of viewing anything on the website. This is because I've had a year of goofing around with adeles but now I want to get the heart of the matter and I want the public blueprint to represent that (i.e. FLT modulo 1980s) and right now it represents a very different (interesting, but different) story.

[Yaël Dillies]

Kevin Buzzard said:

FLT's Mathlib directory now stands at 548K

:scream: surely you mean ~50K instead?

[Yaël Dillies]

I just computed it myself and it came out as ~7k lines of code

[Kevin Buzzard]

buzzard@MacBook-Pro Mathlib % pwd
/Users/buzzard/lean-projects/FLT/FLT/Mathlib
buzzard@MacBook-Pro Mathlib % du -sh
548K    .
buzzard@MacBook-Pro Mathlib %

[Michael Rothgang]

Ah, so you're talking about different metrics. Like Yael, I had assumed you meant total lines of code --- you're computing the total size of all files.

[Kevin Buzzard]

I just wrote what I wrote because I didn't immediately know how to count total lines of lean code :-)

[Julian Berman]

@Kevin Buzzard brew install tokei followed by tokei FLT/Mathlib (or tokei FLT for the whole project). I get...

⊙  tokei FLT/Mathlib                                                                                                                                                                                                                                                             julian@Mac
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 Language              Files        Lines         Code     Comments       Blanks
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 Lean                     90         6930         5026          873         1031
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
 Total                    90         6930         5026          873         1031
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

on main.

[Kevin Buzzard]

Thanks!

[Riccardo Brasca]

Concerning Tate's thesis, this is the projet me and @Filippo A. E. Nuccio want to give to a PhD student, so please don't work on it, or at least contact us if you already started or absolutely need it.

[Andrew Yang]

Does this project include Fourier analysis on locally compact abelian groups in general?

[Riccardo Brasca]

It is supposed to start in September 2026, so there is nothing really precise at the moment.

[Andrew Yang]

I might need Pontryagin dual for arbitrary locally compact abelian groups for FLT and Yael and I had been claiming that we will do it in some distant future. Should we avoid it then?

[Riccardo Brasca]

Give a a two weeks (we will meet to discuss this), but I don't think so. It could even help to unlock more number theoretic results.

[Kevin Buzzard]

I'm certainly not doing Tate's thesis in FLT, but I feel like we've got a bunch of helpful prerequisites.

[Thomas Browning]

Well, Odlyzko will need analytic continuation of Dedekind zeta, and right now Tate's thesis seems like our best bet...

[Kevin Buzzard]

All this is true but none of it is in my immediate plans. The big goal I want to work towards now is reducing FLT to 1980s + a certain modularity lifting theorem, and this will be the subject of my lectures this term.

[Ryan Smith]

Tate's thesis is beautiful, but if we just need the analytic continuation of the Dedekind zeta function surely there are way simpler ways to prove that. It's been a lot of years but I seem to recall it was just a few pages of complex analysis without any really heavy lifting or big dependencies?

If someone did wish to go the Tate's thesis route, would that actually open the way for further generalization in the future? All of the expositions of Tate's thesis that I'm aware of don't really prove anything more general than is required for the 1 dim case, so future work would need to rewrite everything anyway.

Not trying to be contrarian, just asking.

[Stepan Nesterov]

Ryan Smith said:

Tate's thesis is beautiful, but if we just need the analytic continuation of the Dedekind zeta function surely there are way simpler ways to prove that. It's been a lot of years but I seem to recall it was just a few pages of complex analysis without any really heavy lifting or big dependencies?

If someone did wish to go the Tate's thesis route, would that actually open the way for further generalization in the future? All of the expositions of Tate's thesis that I'm aware of don't really prove anything more general than is required for the 1 dim case, so future work would need to rewrite everything anyway.

Not trying to be contrarian, just asking.

Easier to prove doesn’t necessarily translate to easier to formalize. Iirc, earlier proofs of the functional equation for the Dedekind zeta function heavily rely on the geometry of numbers and things like counting lattice points in domains, which can be tricky to formally work with. I think the fact that Tate’s thesis abstracts this geometry into just formal properties of the Fourier transform for the adeles is a bonus for formalization.

[Ryan Smith]

That's a really good point. I wonder what dependencies Tate's thesis would require and if most of them are already present. Basic Fourier analysis is already in mathlib I think?

As a side note, does that mean we don't have the class number formula formalized?

[Chris Birkbeck]

We do have the class number formula, its docs#NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT

[Kevin Buzzard]

The big missing thing is Pontrjagin duality. And then there are other things such as computation of the canonical norm on a p-adic field (the norm measuring how additive Haar measure is scaled) which are in FLT in some form but are not upstreamed yet.

[Ryan Smith]

Only sort of related but do we have enough Galois cohomology / class field theory in mathlib or FLT?

[Stepan Nesterov]

Enough class field theory for what?

[Stepan Nesterov]

The full proof of FLT requires Poitou-Tate duality, and from what I understand, there is currently no plan to formalize it fully

[Ryan Smith]

That makes sense. I was looking through the section of FLT for known in the 1980s and didn't see very assumptions, so I was wondering if more was formalized than I realized or we just hadn't gotten to the point of needing to explicitly make an assumption.

[Kevin Buzzard]

I think that now we're at the point where we could just about state Poitou-Tate and I'd heard rumours that this was one of the many autoformalization targets but we're yet to discover whether AI can write maintainable/PRable code.