Jacquet-Langlands/base change

Stream: FLT-regular

[Stepan Nesterov]

@Kevin Buzzard Which parts of anaylsis does 'less analysis' involve? Would you still be formalising (at least the statements of) Jacquet-Langlands? Cyclic base change?

[Kevin Buzzard]

@Stepan Nesterov I'm reluctant to talk about FLT in #announce because everyone is automatically subscribed to that stream. I am going to avoid Langlands--Tunnell but I will still need Jacquet-Langlands for sure (over totally real fields) and also base change. However out of all the things on my todo list, these two things are at the bottom because (a) they're the part of the argument I understand the least (b) they were proved well before FLT and (c) I only have 5 years. Other things I will initially not be touching include Mazur's theorem and class field theory. If all other stuff gets done and we end up reducing the result to stuff like this from the 70s/80s then I would take Mazur and CFT over the analysis any day.

[Stepan Nesterov]

How far is Lean from defining a cuspidal automorphic representation of $GL_2$ or $D^{\times}$ over a number field?
Does it have Hilbert spaces, adeles, Haar measure etc?

[Patrick Massot]

Hilbert spaces and Haar measures sure. I think adeles are not in Mathlib but somewhere in another repository.

[Stepan Nesterov]

It's a good idea to continue discussion in the flt-regular stream, because Wiles' argument only covers p>=7 :wink:

[Kevin Buzzard]

I think Wiles' argument covers $p=5$.

[Eric Rodriguez]

it'd be nice if our work was needed for the big flt thing :b although showing that 5 is regular is still not something we've done... whoops

[Alex Kontorovich]

Just to add: the things @Heather Macbeth and I have been (slowly) moving on (all kinds of issues with measures on quotient spaces, etc) are exactly trying to build up the analytic parts needed to (eventually) get towards Jacquet-Langlands, namely the trace formula. It would be great to have a two-pronged attack, try to divide and conquer...

[Riccardo Brasca]

Nice !!

[Kevin Buzzard]

This is one really nice thing about doing maths in lean; I will be able to say extremely precisely what I want from the analysis side of things. For example I hadn't realised that I would need the characterisation of the image of cyclic base change (in the GL2 number field case) until Taylor and I thrashed it out. I really want to flesh out the details more but it's going to have to wait until I finish teaching and NNG4