Outstanding Tasks, V2

Stream: FLT

[Kevin Buzzard]

For the previous (rather chaotic) version, see here. I have now got the hang of updating the initial post.

What I had hoped to get the community working on initially was the proof that Mazur's theorem could be used to prove things about Fermat's Last Theorem. However this has turned out to be difficult. For a start, the maths is complex. Secondly, my PhD student David Ang is right in the middle of it working out some key basic things, and without these we cannot really proceed. So I propose that we give up on this and let David tell us when he's ready.

---

The next thing on my list is stating the modularity lifting theorem which we are going to prove. My initial plan was to put this off, because it involves some technical definition of modular forms on a quaternion algebra, which needs the p-adic numbers, adeles, totally real fields etc and it is all much harder.

But then this weekend I realised that actually there's a really cool project the community could work on, which would be to write down an explicit example of a space of weight 2 quaternionic modular forms, prove that it is nonzero by finding an explicit element in it, and then proving that the space is 1-dimensional and is spanned by the form we wrote down. If we did this then it would be the first example in Lean of a space of weight 2 modular forms which is proved to be finite-dimensional (the classical modular forms people are still stuck on the integrals :P ).

So I've been trying to figure out how to teach quaternionic modular forms to people who don't know what the $p$-adic numbers are, by working towards writing an example down. This involves making the basic theory of two rings called $\widehat{\Z}$ and $\widehat{\mathbb{Q}}$ (the finite adeles of $\mathbb{Q}$), whose API I have just sketched in a file called FLT.AutomorphicRepresentation.Example.

Over the next few days I'll develop more of the material here. Right now the main connected component is the main connected component in this picture:

example.png

This thread will work towards developing the basic theory of the completions of $\Z$ and $\mathbb{Q}$.

1) I define $\widehat{\Z}$ to be the subset of $\prod_{M\geq1}(\Z/M\Z)$ consisting of elements $(z_M)_M$ which were "compatible" (i.e. if $D\mid N$ then $z_N$ mod $D$ is $z_D$. I didn't fill in the proof that this was a subring. This is FLT#ZHat.commRing (I assume that doesn't work).

Status: done by Ruben.

2) The characterisation ZHat.multiples of the multiples of $N$ in $\widehat{Z}$ is a good one to experiment with if you want to figure out how to work with this exotic ring $\widehat{\Z}$.

Status: done by Dagur.

3) I call $e$ the element $0!+1!+2!+3!+4!+\cdots$ of $\widehat{Z}$. We need to prove that this does give a well-defined element of $\widehat{\Z}$.

Status: done by Ruben.

One could also try and prove that $e$ is not an integer. I mentioned this question to my friend Alain Verberkmoes and he suggested the following argument. Say $n\geq0$ is equal to $e$. Keep adding up factorials until you go beyond $$n$, say $0!+1!+2!+\cdots+N!>n$. Now let's evaluate these two equal elements modulo $i:=(N+1)!$. The point is that modulo $i$ the series defining $e$ converges really quickly, because way before you get to $i!$ you hit $(N+1)!$ and beyond this point everything is a multiple of $i$. So these elements can't be equal because $0\leq n < e_i < i.$ A similar trick works for $n<0$.

Status: LaTeX proof done, Lean statement ZHat.e_not_in_Int done, Lean proof missing.

4) The natural map from the naturals into $\widehat{Z}$ is injective.
I prove $0\not=1$ and this argument is just a generalisation.

Status: done by Ruben

5) $\widehat{Z}$ is torsion-free; again the proof is in the LaTeX but sorried in lean.
Status: done by Ruben.

6) We now move onto $\widehat{\mathbb{Q}}=\mathbb{Q}\otimes\widehat{\Z}$. The theorem whose proof is fully in the LaTeX is the proof that every element of this tensor product is pure, i.e. of the form $q\otimes_tz.$

Status: done by Dagur

7) Turns out that elements of $\widehat{\mathbb{Q}}$ can uniquely be put into lowest terms $z/N$ with $N\in\N^+$ and $z\in\widehat{\Z}.$ "Lowest terms" means that z_N is a unit mod N.

Status: statement QHat.lowestTerms formalised, LaTeX proof in notes.

8) The maps from $$\Q$$ and from $\widehat{\Z}$ into $\widehat{\mathbb{Q}}$ are both injective. This follows from torsion-freeness implying flatness for $\Z$ although there will be a more low-level way to argue.

Status: Stated as injective_rat and injective_zHat in FLT#AutomorphicRepresentation.Example (can I link to files?).
maths proof is "follows from torsionfreeness"

9) Inside $\widehat{\mathbb{Q}}$ we have $\mathbb{Q}\cap\widehat{\Z}=\Z$.

Status: stated as rat_meet_zHat in Lean, LaTeX proof

10) We have $\mathbb{Q}+\widehat{\Z}=\widehat{\mathbb{Q}}$

Status: stated as rat_join_zHat in Lean, LaTeX proof

11) We have $\mathbb{Q}^\times\cap\widehat{\Z}^\times=\Z^\times$

Status: stated in Lean asQHat.unitsrat_meet_unitszHat, LaTeX proof

12) We have $$\mathbb{Q}^\times\widehat{\Z}^\times=\widehat{\mathbb{Q}}^\times

Status: unitsrat_join_unitszHat, LaTeX proof

[Mario Carneiro]

The next thing on my list is stating the modularity lifting theorem which we are going to prove. My initial plan was to put this off, because it involves some technical definition of modular forms on a quaternion algebra, which needs the p-adic numbers, adeles, totally real fields etc and it is all much harder.

Maybe working on building up this definition could be an initial task at this point? Without doing any proofs. Maybe it's enough to just write a quick definition of this in latex and get people to figure out how to render it in lean

[Mario Carneiro]

(Speaking only for myself, I don't like working on things which are not clearly in the dependency closure of a theorem of interest. Yak shaving is fine and expected, but I'm not a fan of formalizing examples for their own sake / for learning purposes)

[Kevin Buzzard]

Yeah! How do you make tasks? Mario, the definition is super-long. I mean, it's $S_2(U):=\{f:D^\times\backslash D\otimes\widehat{\Z}/U\mathbb{A}_F^f\to\mathbb{C}\}$ but now I need to define the topology on $D\otimes\widehat{\Z}$ and various canonical maps before this even typechecks (here $U$ is a compact open subgroup).

[Chris Birkbeck]

Do you really need to restrict to weight two?

[Kevin Buzzard]

I've started by defining $\widehat{\Z}$. I figured that if we worked out an example then it might inform which API we will need in general. As the chapter increases I will give an example of $D$ (it's $\mathbb{Q}\oplus\mathbb{Q}i\oplus\mathbb{Q}j\oplus\mathbb{Q}k$) and $U$ (with no proof that it's open or compact) but we're not there yet.

[Mario Carneiro]

I think that once we have the definition of Zhat we can immediately move (in parallel) to proofs about Zhat and the definition of things that depend on Zhat (Qhat?)

[Mario Carneiro]

I expect the proofs to take a lot longer than the definitions, although of course the definitions will be wrong and fixed later

[Kevin Buzzard]

Chris Birkbeck said:

Do you really need to restrict to weight two?

No I don't need to, and I don't need to restrict to quaternion algebras when there are central simple algebras, and I don't need to restrict to number fields when there are function fields. But you have to draw a line somewhere and I've decided to draw it at weight 2 because then I don't even need to introduce the infinite adeles at all.

I view the AutomorphicRepresentationas a potential sandbox for experimenting with various definitions of an automorphic representations. We don't have the tools to write down the definition even for $GL_2$ because (amongst other reasons) we cannot talk about the Lie algebra of a Lie group so we cannot write down the automorphy condition at infinity in the case where the Shimura variety is positive-dimensional.

[Mario Carneiro]

maybe I'm being too optimistic but I don't see any reason we can't have all the key definitions for the modularity lifting theorem (with lots of sorried proofs and mistakes) formalized in a week

[Kevin Buzzard]

If I'm allowed to sorry definitions e.g. Topological Space QHat := sorry then I believe you, because we can just do def ModularityLiftingTheorem := sorry.

If we are not allowed to sorry definitions then this becomes a lot more painful, unless you're happy with the idea that some of these definitions might actually have to change when we've figured out how to make the API for them.

I guess right now I am stuck on "if $R$ is a topological ring then $\mathbb{Q}\otimes_{\Z}R$ naturally inherits a topology and in the case of $\widehat{\mathbb{Q}}$ it's the one I want i.e. the one on the finite adeles".

[Terence Tao]

Regarding classical modular forms and integrals, I posed a question on MathOverflow on whether there were ways to reduce the reliance on contour integration to establish basic facts about them: https://mathoverflow.net/questions/467276/proofs-of-the-valence-formula-that-avoid-tricky-contours . It sounds like this wouldn't be directly relevant for the direction youare going towards, but I wanted to mention it anyway in case it is somehow helpful.

[Chris Birkbeck]

Kevin Buzzard said:

Chris Birkbeck said:

Do you really need to restrict to weight two?

No I don't need to, and I don't need to restrict to quaternion algebras when there are central simple algebras, and I don't need to restrict to number fields when there are function fields. But you have to draw a line somewhere and I've decided to draw it at weight 2 because then I don't even need to introduce the infinite adeles at all.

I view the AutomorphicRepresentationas a potential sandbox for experimenting with various definitions of an automorphic representations. We don't have the tools to write down the definition even for $GL_2$ because (amongst other reasons) we cannot talk about the Lie algebra of a Lie group so we cannot write down the automorphy condition at infinity in the case where the Shimura variety is positive-dimensional.

Yeah that's fair enough. One "cheat" would be to define them as a direct sum (over some fintype) of some (sub)spaces of polynomials of some bounded degree and give them the Hecke action. You could then develop the quaternion algebra stuff and then it gives you the fintype needed above. You can use this to define the modular forms attached to that specific quaternion algebra. But I don't really think it makes much difference either way.

[Kevin Buzzard]

Another issue for stating the $R=T$ theorem will be Frobenius elements. Here the following phenomenon arises. If $L/\mathbb{Q}$ is a finite Galois extension then there are "elements" called $Frob_p$ (here $p$ is a prime number not dividing the discriminant of $L$) in $Gal(L/\mathbb{Q})$. But actually these elements are not elements, they are conjugacy classes defined by "the elements which have some property", and the trick is that whenever you say things about $Frob_p$ you make sure that they're conjugacy-invariant (such as $trace(\rho(Frob_p))=a_p$ where $\rho$ is a representation of the Galois group). So now one has to decide whether this statement $trace(\rho(Frob_p))=a_p$ means "for all Frobenius elements, blah" or "for an explicit random choice of Frobenius element, blah". Students of mine have managed to write down both definitions but their code needs review.

[Mitchell Lee]

Is this at all useful for this sort of thing? #12669

[Mitchell Lee]

Also, here's a theorem that can help to define $0! + 1! + 2! + \cdots$, although you may prefer to still do it directly: docs#NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero

[Adam Topaz]

I wonder if we want the full result about representations of elements of Zhat with the “factorial number system”. Should all this stuff about Zhat should go directly to mathlib?

[Terence Tao]

Regarding Frobenius, perhaps we could use Lean’s axiom of choice to canonically (but artificially) define Frobenius, then add as API the lemma that another element obeys the properties of a Frobenius element iff it is conjugate to the canonical Frobenius?

[Adam Topaz]

I remember Kevin mentioning at some point (maybe privately?) that he already had a IsFrobeniusElement predicate. Maybe I’m misremembering?

[Kevin Buzzard]

The problem with the AC approach is that it's not at all obvious that any Frobenius elements exist at all; this boils down to the surjectivity of a certain map which is quite delicate.

[Kevin Buzzard]

IsFrobeniusElement exists only in student-code-land and the student in question has exams right now.

[Ruben Van de Velde]

I couldn't resist your latex proof "follow your nose" so (1) is done at FLT#55

[Terence Tao]

Kevin Buzzard said:

The problem with the AC approach is that it's not at all obvious that any Frobenius elements exist at all; this boils down to the surjectivity of a certain map which is quite delicate.

Then it sounds like a math issue rather than a Lean issue; any rigorous use of Frobenius would have to prove existence of a Frobenius element first, surely.

[Adam Topaz]

If you index by the unramified primes of L, then you don’t need to make any choices and everything is well-defined without conjugation. You could then prove that the Galois action on primes of L respect being unramified, and that the corresponding action on decomposition groups and Frobenius elements is by conjugation, and that it’s transitive for primes over a given rational prime. Then you could work with this canonical notion of Frobenius element up to the Galois action (e.g. using Quotient or something).

[Kevin Buzzard]

I'll ask Ivan if he can PR his code to FLT (IsFrobenius). Reviews of Jou's work (Frobenius) at FLT#18 are welcome!

[Dagur Asgeirsson]

FLT#56 fixes the statement of (2) to match that of the blueprint (the old one was equivalent to z = 0 \iff z N = 0 using that ZHat is torsion free). I started the proof and didn't finish, so anyone else should feel free to continue

[Kevin Buzzard]

Thanks, I merged! I also added a couple more things; I proved that the map from $\mathbb{Q}$ to $\widehat{\mathbb{Q}}$ was injective, for example, but I used torsion-free => flat; I'm sure there will be an easier way. I also developed some of the theory of putting an element of $\mathbb{Q}$ into lowest terms; I discovered that you can uniquely write an element of $\widehat{\mathbb{Q}}$ as $z/N$ with $N$ a positive natural and $z\in\widehat{\Z}$ coprime to $N$, by which I mean $z_N\in(\Z/N\Z)^\times.$

[Kevin Buzzard]

QHat.png

Many nodes are now blue for the additive structure of $\widehat{\mathbb{Q}}.$

I'm going to start work on the multiplicative structure of $\widehat{\mathbb{Q}}$ and then we'll be ready to introduce quaternions into the mix.

[Johan Commelin]

Kevin Buzzard said:

If I'm allowed to sorry definitions e.g. Topological Space QHat := sorry then I believe you

One thing that Adam and I claim is that you should sorry definitions. Together with a bunch of "spec lemmas" that give all the important properties of the definition (redundancy is good).

[Johan Commelin]

Because then you can parallelize. People can start using the concept, via the spec. And others can worry about the best way to fill in the sorried defn + spec lemmas.

[Mario Carneiro]

At the very least, having these objects exist with the right types will unlock being able to start stating the theorems about them

[Mario Carneiro]

In particular def ModularityLiftingTheorem := sorry isn't sufficient unless you add : Prop, and even then only if you intend to indirect the proof through a definition (and I don't see why you would in this case). For theorems we generally want the statement to at least look vaguely correct

[Mario Carneiro]

But if you really want to take my words to the logical conclusion, sure we can have def ModularityLiftingTheorem : Prop := sorry in just a few minutes of work; but then we want to keep going and "progressively disclose" the parts of this expression until we have all the major definitions stated. This on its own is not a particularly good target because it's too easy

[Yaël Dillies]

Mario Carneiro said:

In particular def ModularityLiftingTheorem := sorry isn't sufficient unless you add : Prop, and even then only if you intend to indirect the proof through a definition (and I don't see why you would in this case). For theorems we generally want the statement to at least look vaguely correct

I think Kevin wants ModularityLiftingTheorem to be the theorem, not merely its statement. Yes, it is a Type-valued "theorem".

[Johan Commelin]

But sorrying an implicit type isn't helpful. And sorrying data without accompanying spec lemmas isn't very helpful either, I claim.

[Dagur Asgeirsson]

(2) is done: FLT#64

[Ruben Van de Velde]

Nice!

[Dagur Asgeirsson]

It seems like lean has a bit of trouble seeing that z N and z.val N are the same, for z : ZHat. I often couldn't rewrite using h : z N = 0 (erw didn't work either) but instead had to do something like have : z.val N = 0 := h; rw [this]

[Ruben Van de Velde]

I'll take a look

[Ruben Van de Velde]

@Dagur Asgeirsson you should be able to hit the merge button on https://github.com/dagurtomas/FLT/pull/1 to add my changes to your PR

[Dagur Asgeirsson]

Nice, thank you!

[Ruben Van de Velde]

Update:

1. is done and landed
2. is done in FLT#64
3. first half is done and landed
4. is done and landed but needs a leanok in the blueprint
5. is done in FLT#66

6-10 are open

[Dagur Asgeirsson]

I'm going to work on (6) for a bit

[Dagur Asgeirsson]

6 is done: FLT#67

[Dagur Asgeirsson]

It's a lot of fun to work on this example. I've mostly been doing abstract nonsense in lean and it's a nice change to figure out how to work with things like ℚ. Thank you for proposing it @Kevin Buzzard!

[Kevin Buzzard]

I'm stuck on a low-level approach for the result I want, which is that if A is the quaternions Zhat+Zhat i + ZHat j + ZHat k with i^2=j^2=k^2=-1 etc, and x in A is a divisor of some positive integer N then the left A-module Ax is equal to Ay for some y in Z + Zi + Zj + Zk.

[Kevin Buzzard]

I think I can prove this using Jacquet-Langlands :-/

[Johan Commelin]

Seems hard to believe that there wouldn't be a low-level proof...

[Riccardo Brasca]

Is the Lean statement somewhere? I can give it a try.

[Terence Tao]

It seems to be at least as nontrivial as the Lagrange four-square theorem (or the Hasse-Minkowski theorem), since it implies that the (unique) natural number that is equivalent (up to profinite units) to the norm of a profinite quarternion (which divides $N^2$ by hypothesis), is the sum of four integer squares.

[Terence Tao]

In fact the Hasse-Minkowski theorem may offer the simplest route to proving this claim, though I don't quite see how to do it yet; the norm condition certainly falls within the scope of this theorem, but there are some other conditions that I don't quite understand. Seems like a job for someone expert in algebraic number theory and quadratic forms.

[Riccardo Brasca]

@Kevin Buzzard if you are sure about the Lean statement you need I am happy to take care of this (even if it is a middle sized project)

[Kevin Buzzard]

I now know a low-level proof of the analogue of what I need for the Hurwitz quaternions $R := \Z+\Z i+\Z j+\Z\omega$, with $\omega=\frac{-1+(i+j+k)}{2}$ (notation inspired by the fact that $(i+j+k)^2=-3$; more generally any pure imaginary quaternion $z=ai+bj+ck$ has $\overline{z}=-z$ and thus $z^2=-|z|^2=-a^2-b^2-c^2$). So I'm going to switch to level $R$, which is slightly annoying for expositional purposes, but it's a (non-commutative) Euclidean domain and this is key. The order $R$ is maximal in the rational quaternions (but it's not unique, because of external conjugation). We write $\hat{R}:=R\otimes_{\Z}\widehat{\Z},$ the completion of $R$. We can also define $D:=\mathbb{Q}\otimes R$ and $\hat{D}:=D\otimes\widehat{\Z}.$

My claim is that $\hat{D}^\times=D^{\times}(\hat{R})^{\times}$ and if I can prove this (and I'm writing up the LaTeX proof) then I can prove that a space of quaternionic modular forms is 1-dimensional and exhibit an example of a nonzero quaternionic modular form which is a basis.

Later on we'll be able to compute and prove theorems about Hecke operators $T_p$ and their eigenvalues. I have written code which does this sort of thing in pari-gp. Sometimes you only know the algorithms are correct because of tricky mathematical results which aren't in mathlib.

[Kevin Buzzard]

Ruben Van de Velde said:

Update:

1. is done and landed
2. is done in FLT#64
3. first half is done and landed
4. is done and landed but needs a leanok in the blueprint
5. is done in FLT#66

6-10 are open

#64 has landed but #66 has conflicts :-( I'll update the first post.

[Johan Commelin]

(I suggest moving the messages about the quaternion question to a new thread.)

[Ruben Van de Velde]

Will fix when I get to my desk

[Ruben Van de Velde]

Oh, you already landed. Thanks

[Kevin Buzzard]

Ok! So is that V3? I've realised we're probably going to have to make the Hurwitz questions. Great project for a student -- unfortunately they're all doing exams...

[Ruben Van de Velde]

7-10 still need to be done, right? I distracted myself with e_not_in_Int

[Ruben Van de Velde]

Please merge my open PRs, though :)

[Kevin Buzzard]

Geez managing a project is hard!

[Ruben Van de Velde]

Would you be interested in a bot that announces new pull requests in this stream?

[Kevin Buzzard]

I had sat down yesterday evening and cleared all the PRs, so it was surprising to find there were already some more :-) I guess I need to check up on the project every day. Right now things are a bit out of control, I even have hundreds of unread Zulip messages which is never a good sign.

[Kevin Buzzard]

I'm in the midst of term IRL

[Ruben Van de Velde]

e_not_in_Int FLT#72 is done

[Kevin Buzzard]

Oh nice! In the 1990s one of my lecturers claimed to me that the p-adic component was conjectured to be transcendental for all p. I have no idea if this is still open.

[Ruben Van de Velde]

I will not attempt to resolve that question :)

[Kevin Buzzard]

@Dagur Asgeirsson @Ruben Van de Velde I'm going to split off Z-hat into its own file, because I want to start work on the Galois side and I need it there too. I hope this isn't too disruptive. I can leave Q-hat. I've added a proof that Nat is dense in Z-hat. This is precisely the statement that if a is in Z-hat and N is a positive natural, then it's possible to write a=qN+r with r a natural, and you can even get uniqueness if you demand r<N (although I didn't prove this, and I also didn't construct the iso Z/NZ -> Zhat/NZhat).

[Dagur Asgeirsson]

I'm not working on anything related to this right now, so nothing you do is disruptive to me.

[Ruben Van de Velde]

Sounds good

[Django Peeters]

Hello everyone!
I'm an undergraduate Math student and just started the 3rd year of my bachelor's degree.

About a week ago I stumbled upon the Lean blog about the FLT project and got interested immediately since I've been slowly (passively) learning Lean for the past year. It said if I wanted to contribute I'd have to make myself known, so here I am :) I've almost finished reading chapter 3 of the Mathematics in Lean textbook.

I also tried my hand at 9 (rat_meet_zHat) and found it's just a lot of coercions besides the relatively easy proof from the blueprint. Is it okay if I start working on this lemma?

[Kevin Buzzard]

Yes please do -- it would be a great way to start learning Lean!

[Django Peeters]

Will do!

[Django Peeters]

rat_meet_zHat is proven! Below is my current proof. I'm gonna try to do some codegolfing and maybe install Loogle/Moogle for juggling with all these theorem-names.
image.png

[Kevin Buzzard]

Nice!

[Django Peeters]

I got it down from 63 to 30 lines. Is that enough for this project?
image.png

[Mario Carneiro]

I can't speak for the project but I'm guessing that codegolfing is not required for submitting proofs to FLT. But I do think that some amount of proof compaction is good for you as a writer and also improves the resulting proof, so keep it up

[Ruben Van de Velde]

That seems to be fine, but please squeeze the non-terminal simps, and I wonder if the m and n variables are helping or actually making your proof harder

[Ruben Van de Velde]

I don't think reducing the length is a goal on its own, but you definitely want to remove unused code, avoid reproving the same thing several times, and reuse existing theorems where they exist

[Django Peeters]

Ruben Van de Velde zei:

That seems to be fine, but please squeeze the non-terminal simps, and I wonder if the m and n variables are helping or actually making your proof harder

Simp's are now squeezed I think. The m was mostly for the annoying casesplit on l.num < 0.
As for removing redundancies, this is the result:
image.png
(PNat.coe_toPNat' came close, but was just not what I needed)
Is this better?

[Ruben Van de Velde]

If you push it to a PR, I'll make some more suggestions

[Django Peeters]

This is taking way longer than neccessary. GitHub is confusing. Anyway, I'll try to push it to a PR.

[Django Peeters]

Done.

[Django Peeters]

rat_join_zHat is now done too!

[Ruben Van de Velde]

I commented on FLT#161; I hope you don't mind the wall of text :)

[Django Peeters]

Thank you very much for all this feedback! It is of high value for me since I'm still learning Lean.

[Django Peeters]

Ruben something went wrong on my PR check.

[Django Peeters]

It says the proof your 2nd lemma isn't legit. But it is legit when I let my VSCode lean check it.

[Ruben Van de Velde]

It works for me locally as well, so I'm not sure what happened

[Django Peeters]

It seems I have fixed it.