The numerical criterion

Stream: FLT

[Brendan Seamas Murphy]

Hi all,

One of the steps in the proof of FLT is to prove "$R = \mathbb{T}$". Or more precisely that a certain surjective ring map $R \to \mathbb{T}$ is an isomorphism. This is done by proving (edit: a module over?) $\mathbb{T}$ has an $R$-free summand, so $\mathbb{T}$ is faithful, so the map is injective. This is done via a "numerical criterion", reducing the existence of a free summand to some inequalities involving finite abelian groups.

I don't know anything else about the proof of FLT really, and I'm not a number theorist. But I am a commutative algebraist and my understanding is that the numerical criterion can be extracted into a self contained, purely commutative algebra based statement/proof. My advisor got interested in this topic a couple years ago, see https://arxiv.org/abs/2206.08212, and he said he'd be open to talking to me about the proof and helping me formalize it if there was interest.

Since this seems reasonably self contained, I thought it might be worth trying to work on it now so that once the overall proof of FLT needs it it can be slotted in. Does anyone have a reason it would be a bad idea to start working on this now? Alternatively, would anyone be interested in working on this part of FLT? Certainly there is background commutative algebra that would need to be developed for this

[Jireh Loreaux]

Have you coordinated / discussed this with @Kevin Buzzard at all yet? (oops, I just realized this was in the FLT stream :face_palm: )

[Brendan Seamas Murphy]

That's the intent of this post :P

[Jireh Loreaux]

The stream colors for FLT and General are the same for me (for everyone?) and my brain just assumed this was in General. Sorry for the noise.

[Brendan Seamas Murphy]

Huh weird, they're distinct for me (yellow for general and red bordering on orange for FLT)

[Damiano Testa]

I think that the colour of the streams depends, among other things, on whether you are viewing it in dark mode or not. I use dark mode on Chrome and see General and FLT with the same colour, but they would be different colours in Light mode.

[Mario Carneiro]

The colors are randomized per-user, so there is no sense trying to cross reference them or refer to them by color to others

[Mario Carneiro]

you can recolor them in the settings

[Kevin Buzzard]

Yeah, I noticed this (colour randomisation) when looking over someone else's shoulder at their Zulip.

[Kevin Buzzard]

Re FLT: we're going live in a week but it's looking increasingly likely that there will be no latex description of the details of the R=T theorem we'll need by then. But you can see many of the details in the notes at the top of this page https://math.berkeley.edu/~fengt/stanford_course.html . Theorem 5.4.1 is the modularity lifting theorem we'll need in the minimal case.

[Kevin Buzzard]

I don't have any reason to suggest it would be a bad idea to start working on this now, other than the fact that I haven't thought myself about how best to formalise it. The patching at the minimal level (ie the point where all the number theory is gone and there's only commutative algebra left) is in sections.8.4 and 8.5 of the notes (which have some errors, they're not the best reference but I'm travelling and they're the reference I have to hand).

[David Michael Roberts]

Kevin Buzzard said:

But you can see many of the details in the notes at the top of this page https://math.berkeley.edu/~fengt/stanford_course.html .

I guess you mean the Automorphy Lifting notes by Taylor? (In case later another set of notes is added above and/or the website gets moved and the link rots)

[Brendan Seamas Murphy]

We've got regular sequences in mathlib now! First step complete :tada: