unitsrat_join_unitszHat

Stream: FLT

[Django Peeters]

Since I finished my finals( :octopus: ), I continued working on unitsrat_join_unitszHat. Iirc, there's no task for this one. Just like the previous one I finished, this lemma also comes down to some tinkering so I figured it'd be ideal for me. The proof is nearing 100+ lines of fooling around and I will make a PR soon.

[Kevin Buzzard]

Sorry, I set up this project a while ago before I started making tasks.

This stuff is not needed in the proof of FLT but I thought it would be an excellent test of whether one could actually compute spaces of quaternionic modular forms in Lean. As a graduate student I did this stuff on paper / in pari-gp and found it very illuminating; it inspired my later work on eigencurves for definite quaternion algebras. However when I was doing it on paper I assumed the Jacquet-Langlands correspondence which meant that I would write code which I knew was correct but the proof of correctness relied on a huge theorem. I think it will be interesting (and definitely possible) trying to prove correctness directly.

[Django Peeters]

Does this mean chapter 5 is obsolete? I'm not sure what to work on if that's the case. Or do you still want to test this?

[Kevin Buzzard]

Oh no not at all! I think it's a very interesting project. @Chris Birkbeck has got a PhD student thinking about this stuff and hopefully formalizing definite quaternion algebra eigenvarieties as part of their PhD, and chapter 5 is experimenting with the basic ideas in this theory.

[Chris Birkbeck]

I don't know what 'unitsrat_join_unitszHat' is. But trying to compute some quaternionic modular forms is definitely something worth doing, and as Kevin says, @William Coram is working on p-adic versions of these things as well as trying to formalise some explicit examples.

[Kevin Buzzard]

It's the statement that $\mathbb{A}_f^\times=\widehat{\Z}^\times\mathbb{Q}^\times$, which is a warm-up to proving that $D_f^\times=\widehat{\mathcal{O}_D}^\times.D^\times$ for e.g. the definite quat alg $D$ over $\mathbb{Q}$ with disc 2.

[Kevin Buzzard]

If you replace $\widehat{\mathcal{O}_D}^\times$ with $U_1(5)$ then you end up in the glorious situation where $D_f^\times=U_1(5).D^\times$ and that $U_1(5)\cap D^\times=\{1\}$ so computing quaternionic modular forms of level 5 for this group is super-easy.

[Django Peeters]

Finished at 162 lines, now it's time for some code golfing. :hole_in_one:

[Django Peeters]

Got it down to 128 lines and making the pr now. I'll also have a look at the dashboard and see if there's a fitting task for me.