Zulip Chat Archive

Stream: FLT-regular

Topic: Jacquet-Langlands/base change

Stepan Nesterov (Oct 13 2023 at 21:37):

@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 (Oct 13 2023 at 21:58):

@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 (Oct 13 2023 at 22:07):

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

Patrick Massot (Oct 13 2023 at 22:24):

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

Stepan Nesterov (Oct 13 2023 at 22:24):

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

Kevin Buzzard (Oct 13 2023 at 22:31):

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

Eric Rodriguez (Oct 13 2023 at 22:37):

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 (Oct 14 2023 at 15:38):

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 (Oct 14 2023 at 15:52):

Nice !!

Kevin Buzzard (Oct 14 2023 at 16:01):

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

Last updated: Dec 20 2023 at 11:08 UTC