## Stream: FLT-regular

### Topic: Kummer's lemma

#### Riccardo Brasca (Jan 29 2022 at 09:49):

@Alex J. Best @Chris Birkbeck Have you ideas on a reasonable strategy to prove Kummer's lemma? I mean that if a unit of $\mathbb{Z}[\zeta_p]$ is congruent to an integer modulo $p$ then it is a $p$-th power? @Eric Rodriguez noted that certain proofs use the characterization of regularity using Bernoulli numbers, and I don't think we want to prove it. The proof I've studied it's much harder than I thought (with class theory).

#### Chris Birkbeck (Jan 29 2022 at 10:56):

Sorry for being slow, but where do we need to use this result? I remember needing to use the fact that the p-th power of an element is congruent to an integer. But not this statement.

#### Riccardo Brasca (Jan 29 2022 at 11:03):

Ah maybe we can avoid it, I am not sure. I don't remember the details, but it seems to be needed for case II. If the proof we have in the blueprint avoid it I will not complain :D

#### Chris Birkbeck (Jan 29 2022 at 11:05):

Oh wait, for case II you mean. It might be needed there. Let me have a look, I don't remember how that case goes, I was only thinking if case I.

#### Alex J. Best (Jan 29 2022 at 11:07):

I've done a lot of reading a few weeks ago and my impression is that some form of class field theory is unavoidable for case II.

#### Riccardo Brasca (Jan 29 2022 at 11:07):

We can also postpone it if it's too hard. I think Kummer included it in the original definition of regular prime and proved it's automatic later.

#### Riccardo Brasca (Jan 29 2022 at 11:10):

this seems reasonable, but I didn't check all the details.

#### Chris Birkbeck (Jan 29 2022 at 11:13):

Is that not case I?

#### Eric Rodriguez (Jan 29 2022 at 11:14):

The last time I learnt about this this was mentioned as a "small detour" for case II; I think it was understated

#### Chris Birkbeck (Jan 29 2022 at 11:16):

The proof of case I is in the blueprint and indeed doesn't need anything from CFT or Bernoulli numbers. Case II, does certainly seem to need a "detour"...

#### Riccardo Brasca (Jan 29 2022 at 11:17):

Chris Birkbeck said:

Is that not case I?

Ah yes, I was confused by theorem 5.8 about units, but it's not what we need.

#### Riccardo Brasca (Jan 29 2022 at 11:22):

Hmm... I think we can concentrate in case I for the moment, it's already a lot of work... maybe someone will include CFT in mathlib in the meantime :big_smile:

#### Kevin Buzzard (Jan 29 2022 at 11:37):

Is this one of those situations where there is more than one definition of "regular prime" and the proof that they're all the same is hard, and so you just choose the definition of regular in your repo which works for you? We had this in the perfectoid project. The definition of the topology on an adic space is "it's the topology generated by subsets of this form" and then it's a 30 page theorem proving that the topology is equal to "the one generated by subsets of that form". We chose one of the definitions at random (in fact we chose the one used in our source material), didn't prove the 30 page theorem (which was proved in the source material), and then when we wanted to define a presheaf on an affinoid adic space we realised we couldn't do it! So we switched to the other definition and it became easy. The question now becomes "what is the actual definition of the topology?" And this is a meaningless question in some sense because the two definitions coincide. But the literature certainly usually uses the definition which we did not use. I do not lose sleep over this issue.

#### Kevin Buzzard (Jan 29 2022 at 11:41):

On the other hand one could argue that if I was asked to formalise the definition of the Poincaré conjecture I reply that it's 2+2=4 and argue that it's a theorem in the literature that this is equivalent to the usual definition ;-)

#### Eric Rodriguez (Jan 29 2022 at 11:41):

To be fair, that may also be a good idea - I can't even find a proof of the equivalence to the Bernoulli number condition anywhere, but they're widely accepted as equivalent + we don't use the original condition at all in flt-regular

#### Riccardo Brasca (Jan 29 2022 at 11:41):

Yes, we can very well change the definition using Bernoulli numbers, but this will create problems for case I I think. We can also define something like "strong regular" meaning regular (via class number) plus Kummer's lemma. Sooner or later we want to prove that regularity implies strong regularity, but this seems to be a separate project (and maybe even more complicated than the whole flt-regular, depending on the proof one wants to use)

#### Riccardo Brasca (Jan 29 2022 at 11:42):

@Chris Birkbeck you use regularity via class number in case I, right?

#### Riccardo Brasca (Jan 29 2022 at 11:42):

In the blueprint I mean

#### Kevin Buzzard (Jan 29 2022 at 11:42):

You can define regular to be both of the conditions which you require -- the case 1 regular and the case 2 regular

yes

#### Kevin Buzzard (Jan 29 2022 at 11:43):

Then it's still absolutely the case that you've proved FLT for regular primes

#### Chris Birkbeck (Jan 29 2022 at 11:43):

I think even for case 2 one needs "both" versions. Or at least thats what Washington's seems to say

#### Kevin Buzzard (Jan 29 2022 at 11:45):

I would not worry too much about this. Obviously we're a million miles from Ribet's converse to Kummer Herbrand or whatever it's called but one could thus argue that this shows that in 1847 there was more than one definition of regular prime anyway

#### Riccardo Brasca (Jan 29 2022 at 11:46):

We should check this carefully, but I have the impression that Bernoulli numbers used to prove Kummer's lemma (the one I stated at the beginning of this thread) and that's it. So if we include this property in the definition our proof of case II would be the good one, but just for "strong regular primes".

#### Kevin Buzzard (Jan 29 2022 at 11:47):

But it's a theorem that strong regular is regular. You just say "our definition of regular is the following; there are many equivalent definitions but this is the one which is most convenient for us"

#### Chris Birkbeck (Jan 29 2022 at 11:48):

Riccardo Brasca said:

We should check this carefully, but I have the impression that Bernoulli numbers used to prove Kummer's lemma (the one I stated at the beginning of this thread) and that's it. So if we include this property in the definition our proof of case II would be the good one, but just for "strong regular primes".

Yes I think this is the way to go. Washington gives a couple of proofs using different versions of regular, so I'm looking to see what exactly is needed

#### Kevin Buzzard (Jan 29 2022 at 11:49):

If you just throw in everything you need then you're splitting off the task of proving equivalence to some other definition as a problem which someone else can work on eg a student

#### Riccardo Brasca (Jan 29 2022 at 11:50):

I agree this seems the best solution.

#### Kevin Buzzard (Jan 29 2022 at 11:54):

There are many different definitions of what it means for an elliptic curve over Q to be modular and I remember the time before BCDT where people would have to explicitly put these assumptions into their theorems. Nobody thought hard about which definition they were using because they were all the same. To get from rho_E = rho_f to E isogenous to E_f you need Faltings' theorem. If someone proved all elliptic curves were modular in Lean for the weaker definition (which is what Wiles does) then nobody is going to complain that they didn't also prove Faltings' theorem. However people might need it in applications.

#### Eric Rodriguez (Jan 29 2022 at 11:55):

this is almost bike-shedding, but is bernoulli-regular equivalent to class-group-regular for non-primes? we seem to have defined is_regular_number instead of is_regular_prime

#### Kevin Buzzard (Jan 29 2022 at 11:55):

Fortunately I'm not sure there are too many people out there who want to apply flt-regular; it's an endpoint. The conclusion is that you've solved many hard Diophantine equations all at once.

#### Kevin Buzzard (Jan 29 2022 at 11:58):

Will you be able to prove that 23 is a regular prime in the sense you need? I mention 23 because the class number isn't 1 (it's 3 IIRC) so a concrete consequence of your work is no nontrivial solutions to x^23+y^23=z^23 which in my opinion is a formalisation milestone because this Diophantine equation is hard.

#### Kevin Buzzard (Jan 29 2022 at 11:59):

@Eric Rodriguez what's the maths question you're asking? I don't know my way around your repo

#### Eric Rodriguez (Jan 29 2022 at 11:59):

Alex mentioned struggling to prove 2 was regular with the current criterion so we'll see

#### Riccardo Brasca (Jan 29 2022 at 11:59):

In my opinion the characterization using Bernoulli numbers is useful only for concrete computations like this one. Otherwise the characterization is only needed to prove Kummer's lemma (I think) but in my opinion (I am maybe too much algebraic-number-theory oriented) this should be proved using CFT.

#### Eric Rodriguez (Jan 29 2022 at 12:01):

Kevin Buzzard said:

Eric Rodriguez what's the maths question you're asking? I don't know my way around your repo

we have is_regular_number n, instead of is_regular_prime n; I was wondering if both definitions lined up naturally for non-prime n, but I think few people have considered ℤ[ζₙ] much for n non-prime and so it'll be open; Herbrand-Ribet is only about odd primes (according to Wiki anyways)

#### Riccardo Brasca (Jan 29 2022 at 12:03):

I wrote that just because it was for free, but I never intended to seriously using it.

#### Riccardo Brasca (Jan 29 2022 at 12:04):

I will not be very active until Monday, enjoy the weekend!

#### Kevin Buzzard (Jan 29 2022 at 12:05):

Well I know CFT is a long way away but one of my favourite maths books is Cassels-Froehlich (which proves the main theorems of CFT) and for a while now I've been pushing people slowly in the direction of formalising the first few chapters of this book (and of course others formalise results in it independently). Maria has done Adeles, Amelia has done group cohomology, Anne/Sander/Filippo/Ashvni have done Dedekind domain stuff and your work will make Birch's chapter on Kummer theory pretty straightforward. We still need some basic results on the Galois theory of local and global fields but it is not at all unreasonable to start looking at local class field theory and realise that it's a possible goal, and then global stuff is accessible. The global stuff needs some complex analysis but this is finally coming our way.

#### Chris Birkbeck (Jan 29 2022 at 12:05):

Yeah I think we just define strong regular prime and go with that. I have no idea what happens for non-primes.

#### Kevin Buzzard (Jan 29 2022 at 12:05):

@Eric Rodriguez I am asking what the mathematical definitions of these things are -- I'm on mobile and don't know where to start looking in your repo

#### Chris Birkbeck (Jan 29 2022 at 12:08):

Kevin Buzzard said:

Eric Rodriguez I am asking what the mathematical definitions of these things are

One will be that for n an integer, we have n doesnt divide the class group of zeta_n. The other will be that n doesnt divide the numerator of Bernoulli numbers up to n-3 (?) . The question is are these equivalent for non prime n. (If I understand the question correctly)

#### Kevin Buzzard (Jan 29 2022 at 12:09):

CFT is an essential prerequisite for FLT and even though the math community probably won't place too much importance on a full FLT formalisation, computer scientists talk about it as if it's some kind of holy grail. If they mean this then they'll find money for us to do it and this should take me up nicely to my retirement. My advisor proved it, his advisor proved it too -- why can't I prove it? I think proving FLT should become a British tradition

#### Kevin Buzzard (Jan 29 2022 at 12:11):

Thanks Chris. My guess is that these will not be the same. I think it's quite hard to calculate class groups of cyclotomic fields so it might be interesting to find out if there's an accessible counterexample. Hopefully 9 or 15 will work

#### Kevin Buzzard (Jan 29 2022 at 12:14):

"n doesn't divide any of a list of numbers" is equivalent to "n doesn't divide the product of these numbers" if n is prime (or even preprime) but not in general. If you use the product instead of the list then I bet 15 is a counterexample

#### Chris Birkbeck (Jan 29 2022 at 12:14):

Kevin Buzzard said:

CFT is an essential prerequisite for FLT and even though the math community probably won't place too much importance on a full FLT formalisation, computer scientists talk about it as if it's some kind of holy grail. If they mean this then they'll find money for us to do it and this should take me up nicely to my retirement. My advisor proved it, his advisor proved it too -- why can't I prove it? I think proving FLT should become a British tradition

Also, what if we find a mistake? We definitely need to do this before all of the authors retire in case we need them to fix the proof, so the money to do this soon is even more important. :P

#### Kevin Buzzard (Jan 29 2022 at 12:17):

That's the sort of argument which seems to fly in the CS world and gets mathematicians all steamed up! I don't know if people have read all this non-Galois cubic base change stuff properly but presumably somebody has. The analytic people seem confident that it's fine but would you trust Michael Harris? ;-)

#### Kevin Buzzard (Jan 29 2022 at 12:18):

OTOH the CS people seem to have latched onto this and classification of finite simple groups as some kind of milestones in the area of formalisation

#### Kevin Buzzard (Jan 29 2022 at 12:18):

This is why they'll love flt_regular ;-)

#### Eric Rodriguez (Jan 29 2022 at 12:19):

sorry, I went to have some lunch - yes, Chris got what I meant right. I might get out some pen-and-paper and try find some explicit ones :)

15 does work...

#### Chris Birkbeck (Jan 29 2022 at 12:21):

i.e. its not a counter example

#### Chris Birkbeck (Jan 29 2022 at 12:32):

Looking at the first few Bernoulli numbers, it seems the smallest we can maybe hope for is that the class number zeta_1441 is not divisible by 1441, since the numerator B_22 is divisible by 1441=11*131. But I dont want to try and compute this class number.

#### Eric Rodriguez (Jan 29 2022 at 12:42):

oh my god they grow so fast

#### Eric Rodriguez (Jan 29 2022 at 12:42):

I thought they were quite small! Dear lord

#### Chris Birkbeck (Jan 29 2022 at 12:47):

Oh yeah, everything explodes pretty quickly. The class number calculations are just crazy. Let me help you out, here is the Minkowski bound for Q(\zeta_1441): 26275234640582515846607757842030988969136677244719357034756466233590998270915462831212165310988801751368599489966389964393013562340128825400158229156548267474116324696425893112812481934453795931493114492465437447060155417540015946408120650004339956524727277866230065349696487027411267673860978600269170327244023243598393058085534920475536669555980548936153663568524851089457915793679927208941285781778777169241474066870329251479954335215551250874422104453565073943680446098655529440144662890679716756504887805077699119182276609956688375838728649393859017719565651090496406677664543883386307836276905994239369385448504324644741281179330376770358751940219102307954807380505398257366273165817994111921572646135029380409318587416443337065693453830667366315946376715178387658359273621719419884761733021165768701215923663637962099340308725592880116232411658532452756725625106219776209933437016071869574626385928480015194158802497339607967848193745147344922931713209399245810186320430099197477657842774097010514199871847045397620118354782585513795941216178623262424936766552916527722340026365776970206104875947169676895631693151165966764006997144852360220105024903505021631825401820482823311186637596921898433727691578178394404861275389442672949367929406200561728121620678141532148448725111378983437192261983586791123397576151753079131084151615498763766713252632840734823527382162071292472615506519316137566114231838710136388708533645779980597116630955602527907370214031751382010161433711 :joy:

#### Kevin Buzzard (Jan 29 2022 at 13:41):

For small degree it's manageable but when the degree gets big quickly like it does for Q(zeta_n) you have problems even if you assume GRH

#### Chris Birkbeck (Jan 29 2022 at 13:43):

Yeah, I checked your claim about 23 having class number 3 and even for that I needed to assume GRH.

#### Kevin Buzzard (Jan 29 2022 at 13:45):

The order divides 3 because the class group of the quadratic subext is 3

#### Chris Birkbeck (Feb 04 2022 at 09:44):

Ok looking at this lemma...its a bit annoying as most proofs I can see are quite long. I'll look around for a relatively nice one and try and add some of the steps to the blueprint

#### Antoine Chambert-Loir (Feb 05 2022 at 18:00):

Kevin Buzzard said:

"n doesn't divide any of a list of numbers" is equivalent to "n doesn't divide the product of these numbers" if n is prime (or even preprime) but not in general. If you use the product instead of the list then I bet 15 is a counterexample

Does this result help ? (http://www.numdam.org/item/CM_1976__33_2_179_0/)
image.png

#### Kevin Buzzard (Feb 05 2022 at 18:13):

Ha! Is it known whether is a cyclotomic field with class number 6?

#### Kevin Buzzard (Feb 05 2022 at 18:15):

Rather annoyingly h_m < m in these examples. My understanding is that this doesn't last long...

#### Thomas Browning (Feb 05 2022 at 18:21):

Washington's book has some tables with big numbers, IIRC

#### Antoine Chambert-Loir (Feb 05 2022 at 18:31):

By the way, if I had to cook up a definition of a regular integer, I would say that n is a regular integer if the class group of the number field cyclotomic Q n is coprime to the order of its group of roots of unity (rather than does not divide)

#### Kevin Buzzard (Feb 05 2022 at 19:17):

So 56 is an irregular number!

#### Riccardo Brasca (Jan 29 2022 at 09:49):

@Alex J. Best @Chris Birkbeck Have you ideas on a reasonable strategy to prove Kummer's lemma? I mean that if a unit of $\mathbb{Z}[\zeta_p]$ is congruent to an integer modulo $p$ then it is a $p$-th power? @Eric Rodriguez noted that certain proofs use the characterization of regularity using Bernoulli numbers, and I don't think we want to prove it. The proof I've studied it's much harder than I thought (with class theory).

#### Chris Birkbeck (Jan 29 2022 at 10:56):

Sorry for being slow, but where do we need to use this result? I remember needing to use the fact that the p-th power of an element is congruent to an integer. But not this statement.

#### Riccardo Brasca (Jan 29 2022 at 11:03):

Ah maybe we can avoid it, I am not sure. I don't remember the details, but it seems to be needed for case II. If the proof we have in the blueprint avoid it I will not complain :D

#### Chris Birkbeck (Jan 29 2022 at 11:05):

Oh wait, for case II you mean. It might be needed there. Let me have a look, I don't remember how that case goes, I was only thinking if case I.

#### Alex J. Best (Jan 29 2022 at 11:07):

I've done a lot of reading a few weeks ago and my impression is that some form of class field theory is unavoidable for case II.

#### Riccardo Brasca (Jan 29 2022 at 11:07):

We can also postpone it if it's too hard. I think Kummer included it in the original definition of regular prime and proved it's automatic later.

#### Riccardo Brasca (Jan 29 2022 at 11:10):

this seems reasonable, but I didn't check all the details.

#### Chris Birkbeck (Jan 29 2022 at 11:13):

Is that not case I?

#### Eric Rodriguez (Jan 29 2022 at 11:14):

The last time I learnt about this this was mentioned as a "small detour" for case II; I think it was understated

#### Chris Birkbeck (Jan 29 2022 at 11:16):

The proof of case I is in the blueprint and indeed doesn't need anything from CFT or Bernoulli numbers. Case II, does certainly seem to need a "detour"...

#### Riccardo Brasca (Jan 29 2022 at 11:17):

Chris Birkbeck said:

Is that not case I?

Ah yes, I was confused by theorem 5.8 about units, but it's not what we need.

#### Riccardo Brasca (Jan 29 2022 at 11:22):

Hmm... I think we can concentrate in case I for the moment, it's already a lot of work... maybe someone will include CFT in mathlib in the meantime :big_smile:

#### Kevin Buzzard (Jan 29 2022 at 11:37):

Is this one of those situations where there is more than one definition of "regular prime" and the proof that they're all the same is hard, and so you just choose the definition of regular in your repo which works for you? We had this in the perfectoid project. The definition of the topology on an adic space is "it's the topology generated by subsets of this form" and then it's a 30 page theorem proving that the topology is equal to "the one generated by subsets of that form". We chose one of the definitions at random (in fact we chose the one used in our source material), didn't prove the 30 page theorem (which was proved in the source material), and then when we wanted to define a presheaf on an affinoid adic space we realised we couldn't do it! So we switched to the other definition and it became easy. The question now becomes "what is the actual definition of the topology?" And this is a meaningless question in some sense because the two definitions coincide. But the literature certainly usually uses the definition which we did not use. I do not lose sleep over this issue.

#### Kevin Buzzard (Jan 29 2022 at 11:41):

On the other hand one could argue that if I was asked to formalise the definition of the Poincaré conjecture I reply that it's 2+2=4 and argue that it's a theorem in the literature that this is equivalent to the usual definition ;-)

#### Eric Rodriguez (Jan 29 2022 at 11:41):

To be fair, that may also be a good idea - I can't even find a proof of the equivalence to the Bernoulli number condition anywhere, but they're widely accepted as equivalent + we don't use the original condition at all in flt-regular

#### Riccardo Brasca (Jan 29 2022 at 11:41):

Yes, we can very well change the definition using Bernoulli numbers, but this will create problems for case I I think. We can also define something like "strong regular" meaning regular (via class number) plus Kummer's lemma. Sooner or later we want to prove that regularity implies strong regularity, but this seems to be a separate project (and maybe even more complicated than the whole flt-regular, depending on the proof one wants to use)

#### Riccardo Brasca (Jan 29 2022 at 11:42):

@Chris Birkbeck you use regularity via class number in case I, right?

#### Riccardo Brasca (Jan 29 2022 at 11:42):

In the blueprint I mean

#### Kevin Buzzard (Jan 29 2022 at 11:42):

You can define regular to be both of the conditions which you require -- the case 1 regular and the case 2 regular

yes

#### Kevin Buzzard (Jan 29 2022 at 11:43):

Then it's still absolutely the case that you've proved FLT for regular primes

#### Chris Birkbeck (Jan 29 2022 at 11:43):

I think even for case 2 one needs "both" versions. Or at least thats what Washington's seems to say

#### Kevin Buzzard (Jan 29 2022 at 11:45):

I would not worry too much about this. Obviously we're a million miles from Ribet's converse to Kummer Herbrand or whatever it's called but one could thus argue that this shows that in 1847 there was more than one definition of regular prime anyway

#### Riccardo Brasca (Jan 29 2022 at 11:46):

We should check this carefully, but I have the impression that Bernoulli numbers used to prove Kummer's lemma (the one I stated at the beginning of this thread) and that's it. So if we include this property in the definition our proof of case II would be the good one, but just for "strong regular primes".

#### Kevin Buzzard (Jan 29 2022 at 11:47):

But it's a theorem that strong regular is regular. You just say "our definition of regular is the following; there are many equivalent definitions but this is the one which is most convenient for us"

#### Chris Birkbeck (Jan 29 2022 at 11:48):

Riccardo Brasca said:

We should check this carefully, but I have the impression that Bernoulli numbers used to prove Kummer's lemma (the one I stated at the beginning of this thread) and that's it. So if we include this property in the definition our proof of case II would be the good one, but just for "strong regular primes".

Yes I think this is the way to go. Washington gives a couple of proofs using different versions of regular, so I'm looking to see what exactly is needed

#### Kevin Buzzard (Jan 29 2022 at 11:49):

If you just throw in everything you need then you're splitting off the task of proving equivalence to some other definition as a problem which someone else can work on eg a student

#### Riccardo Brasca (Jan 29 2022 at 11:50):

I agree this seems the best solution.

#### Kevin Buzzard (Jan 29 2022 at 11:54):

There are many different definitions of what it means for an elliptic curve over Q to be modular and I remember the time before BCDT where people would have to explicitly put these assumptions into their theorems. Nobody thought hard about which definition they were using because they were all the same. To get from rho_E = rho_f to E isogenous to E_f you need Faltings' theorem. If someone proved all elliptic curves were modular in Lean for the weaker definition (which is what Wiles does) then nobody is going to complain that they didn't also prove Faltings' theorem. However people might need it in applications.

#### Eric Rodriguez (Jan 29 2022 at 11:55):

this is almost bike-shedding, but is bernoulli-regular equivalent to class-group-regular for non-primes? we seem to have defined is_regular_number instead of is_regular_prime

#### Kevin Buzzard (Jan 29 2022 at 11:55):

Fortunately I'm not sure there are too many people out there who want to apply flt-regular; it's an endpoint. The conclusion is that you've solved many hard Diophantine equations all at once.

#### Kevin Buzzard (Jan 29 2022 at 11:58):

Will you be able to prove that 23 is a regular prime in the sense you need? I mention 23 because the class number isn't 1 (it's 3 IIRC) so a concrete consequence of your work is no nontrivial solutions to x^23+y^23=z^23 which in my opinion is a formalisation milestone because this Diophantine equation is hard.

#### Kevin Buzzard (Jan 29 2022 at 11:59):

@Eric Rodriguez what's the maths question you're asking? I don't know my way around your repo

#### Eric Rodriguez (Jan 29 2022 at 11:59):

Alex mentioned struggling to prove 2 was regular with the current criterion so we'll see

#### Riccardo Brasca (Jan 29 2022 at 11:59):

In my opinion the characterization using Bernoulli numbers is useful only for concrete computations like this one. Otherwise the characterization is only needed to prove Kummer's lemma (I think) but in my opinion (I am maybe too much algebraic-number-theory oriented) this should be proved using CFT.

#### Eric Rodriguez (Jan 29 2022 at 12:01):

Kevin Buzzard said:

Eric Rodriguez what's the maths question you're asking? I don't know my way around your repo

we have is_regular_number n, instead of is_regular_prime n; I was wondering if both definitions lined up naturally for non-prime n, but I think few people have considered ℤ[ζₙ] much for n non-prime and so it'll be open; Herbrand-Ribet is only about odd primes (according to Wiki anyways)

#### Riccardo Brasca (Jan 29 2022 at 12:03):

I wrote that just because it was for free, but I never intended to seriously using it.

#### Riccardo Brasca (Jan 29 2022 at 12:04):

I will not be very active until Monday, enjoy the weekend!

#### Kevin Buzzard (Jan 29 2022 at 12:05):

Well I know CFT is a long way away but one of my favourite maths books is Cassels-Froehlich (which proves the main theorems of CFT) and for a while now I've been pushing people slowly in the direction of formalising the first few chapters of this book (and of course others formalise results in it independently). Maria has done Adeles, Amelia has done group cohomology, Anne/Sander/Filippo/Ashvni have done Dedekind domain stuff and your work will make Birch's chapter on Kummer theory pretty straightforward. We still need some basic results on the Galois theory of local and global fields but it is not at all unreasonable to start looking at local class field theory and realise that it's a possible goal, and then global stuff is accessible. The global stuff needs some complex analysis but this is finally coming our way.

#### Chris Birkbeck (Jan 29 2022 at 12:05):

Yeah I think we just define strong regular prime and go with that. I have no idea what happens for non-primes.

#### Kevin Buzzard (Jan 29 2022 at 12:05):

@Eric Rodriguez I am asking what the mathematical definitions of these things are -- I'm on mobile and don't know where to start looking in your repo

#### Chris Birkbeck (Jan 29 2022 at 12:08):

Kevin Buzzard said:

Eric Rodriguez I am asking what the mathematical definitions of these things are

One will be that for n an integer, we have n doesnt divide the class group of zeta_n. The other will be that n doesnt divide the numerator of Bernoulli numbers up to n-3 (?) . The question is are these equivalent for non prime n. (If I understand the question correctly)

#### Kevin Buzzard (Jan 29 2022 at 12:09):

CFT is an essential prerequisite for FLT and even though the math community probably won't place too much importance on a full FLT formalisation, computer scientists talk about it as if it's some kind of holy grail. If they mean this then they'll find money for us to do it and this should take me up nicely to my retirement. My advisor proved it, his advisor proved it too -- why can't I prove it? I think proving FLT should become a British tradition

#### Kevin Buzzard (Jan 29 2022 at 12:11):

Thanks Chris. My guess is that these will not be the same. I think it's quite hard to calculate class groups of cyclotomic fields so it might be interesting to find out if there's an accessible counterexample. Hopefully 9 or 15 will work

#### Kevin Buzzard (Jan 29 2022 at 12:14):

"n doesn't divide any of a list of numbers" is equivalent to "n doesn't divide the product of these numbers" if n is prime (or even preprime) but not in general. If you use the product instead of the list then I bet 15 is a counterexample

#### Chris Birkbeck (Jan 29 2022 at 12:14):

Kevin Buzzard said:

CFT is an essential prerequisite for FLT and even though the math community probably won't place too much importance on a full FLT formalisation, computer scientists talk about it as if it's some kind of holy grail. If they mean this then they'll find money for us to do it and this should take me up nicely to my retirement. My advisor proved it, his advisor proved it too -- why can't I prove it? I think proving FLT should become a British tradition

Also, what if we find a mistake? We definitely need to do this before all of the authors retire in case we need them to fix the proof, so the money to do this soon is even more important. :P

#### Kevin Buzzard (Jan 29 2022 at 12:17):

That's the sort of argument which seems to fly in the CS world and gets mathematicians all steamed up! I don't know if people have read all this non-Galois cubic base change stuff properly but presumably somebody has. The analytic people seem confident that it's fine but would you trust Michael Harris? ;-)

#### Kevin Buzzard (Jan 29 2022 at 12:18):

OTOH the CS people seem to have latched onto this and classification of finite simple groups as some kind of milestones in the area of formalisation

#### Kevin Buzzard (Jan 29 2022 at 12:18):

This is why they'll love flt_regular ;-)

#### Eric Rodriguez (Jan 29 2022 at 12:19):

sorry, I went to have some lunch - yes, Chris got what I meant right. I might get out some pen-and-paper and try find some explicit ones :)

15 does work...

#### Chris Birkbeck (Jan 29 2022 at 12:21):

i.e. its not a counter example

#### Chris Birkbeck (Jan 29 2022 at 12:32):

Looking at the first few Bernoulli numbers, it seems the smallest we can maybe hope for is that the class number zeta_1441 is not divisible by 1441, since the numerator B_22 is divisible by 1441=11*131. But I dont want to try and compute this class number.

#### Eric Rodriguez (Jan 29 2022 at 12:42):

oh my god they grow so fast

#### Eric Rodriguez (Jan 29 2022 at 12:42):

I thought they were quite small! Dear lord

#### Chris Birkbeck (Jan 29 2022 at 12:47):

Oh yeah, everything explodes pretty quickly. The class number calculations are just crazy. Let me help you out, here is the Minkowski bound for Q(\zeta_1441): 26275234640582515846607757842030988969136677244719357034756466233590998270915462831212165310988801751368599489966389964393013562340128825400158229156548267474116324696425893112812481934453795931493114492465437447060155417540015946408120650004339956524727277866230065349696487027411267673860978600269170327244023243598393058085534920475536669555980548936153663568524851089457915793679927208941285781778777169241474066870329251479954335215551250874422104453565073943680446098655529440144662890679716756504887805077699119182276609956688375838728649393859017719565651090496406677664543883386307836276905994239369385448504324644741281179330376770358751940219102307954807380505398257366273165817994111921572646135029380409318587416443337065693453830667366315946376715178387658359273621719419884761733021165768701215923663637962099340308725592880116232411658532452756725625106219776209933437016071869574626385928480015194158802497339607967848193745147344922931713209399245810186320430099197477657842774097010514199871847045397620118354782585513795941216178623262424936766552916527722340026365776970206104875947169676895631693151165966764006997144852360220105024903505021631825401820482823311186637596921898433727691578178394404861275389442672949367929406200561728121620678141532148448725111378983437192261983586791123397576151753079131084151615498763766713252632840734823527382162071292472615506519316137566114231838710136388708533645779980597116630955602527907370214031751382010161433711 :joy:

#### Kevin Buzzard (Jan 29 2022 at 13:41):

For small degree it's manageable but when the degree gets big quickly like it does for Q(zeta_n) you have problems even if you assume GRH

#### Chris Birkbeck (Jan 29 2022 at 13:43):

Yeah, I checked your claim about 23 having class number 3 and even for that I needed to assume GRH.

#### Kevin Buzzard (Jan 29 2022 at 13:45):

The order divides 3 because the class group of the quadratic subext is 3

#### Chris Birkbeck (Feb 04 2022 at 09:44):

Ok looking at this lemma...its a bit annoying as most proofs I can see are quite long. I'll look around for a relatively nice one and try and add some of the steps to the blueprint

#### Antoine Chambert-Loir (Feb 05 2022 at 18:00):

Kevin Buzzard said:

"n doesn't divide any of a list of numbers" is equivalent to "n doesn't divide the product of these numbers" if n is prime (or even preprime) but not in general. If you use the product instead of the list then I bet 15 is a counterexample

Does this result help ? (http://www.numdam.org/item/CM_1976__33_2_179_0/)
image.png

#### Kevin Buzzard (Feb 05 2022 at 18:13):

Ha! Is it known whether is a cyclotomic field with class number 6?

#### Kevin Buzzard (Feb 05 2022 at 18:15):

Rather annoyingly h_m < m in these examples. My understanding is that this doesn't last long...

#### Thomas Browning (Feb 05 2022 at 18:21):

Washington's book has some tables with big numbers, IIRC

#### Antoine Chambert-Loir (Feb 05 2022 at 18:31):

By the way, if I had to cook up a definition of a regular integer, I would say that n is a regular integer if the class group of the number field cyclotomic Q n is coprime to the order of its group of roots of unity (rather than does not divide)

#### Kevin Buzzard (Feb 05 2022 at 19:17):

So 56 is an irregular number!

#### Johan Commelin (Oct 03 2023 at 10:33):

If I understand correctly, Kummer's lemma is the main remaining goal in the FLT-regular project.

• Is it really the only sorry left, or are there others?
• Can someone give a general status update of where the project is? (I've kept an eye on things, but didn't follow too closely in the past few months.)
• Is there a plan / blueprint for Kummer's lemma?

#### Riccardo Brasca (Oct 03 2023 at 10:48):

Yes, it is the only remaining goal. It is a difficult result (even mathematically), and probably need quite a lot of prerequisites (L functions or classi field theory).

#### Riccardo Brasca (Oct 03 2023 at 10:49):

In my opinion we can keep one stream at the moment, especially since Kevin's project is not going to start immediately

#### Riccardo Brasca (Oct 03 2023 at 10:50):

BTW it is literally this sorry (of course it will be split in many others), and we are not completely sure on which math proof formalize

#### Antoine Chambert-Loir (Oct 03 2023 at 12:13):

From what I see, Lang uses class field theory, but Washington does it by studying units.
Keith Conrad has written a detailed exposition of it.

#### Chris Birkbeck (Oct 03 2023 at 12:14):

Yeah I would avoid CFT. The proof Conrad has follows the Borevich-shafarevich one I had in mind

#### Ruben Van de Velde (Oct 03 2023 at 12:16):

6.5 pages, how hard can it be :sweat_smile:

#### Antoine Chambert-Loir (Oct 03 2023 at 12:24):

In fact, I did not pay attention, but Conrad defines “regular” using Bernoulli numbers.

#### Riccardo Brasca (Oct 03 2023 at 12:25):

It's a little intricate to follow the various definitions/proofs. For example what Conrad proves is not what we want (I think). @Chris Birkbeck BS proof also gives the connection with Bernoulli numbers?

#### Chris Birkbeck (Oct 03 2023 at 12:31):

Yes I think they also connect with Bernoulli numbers.

#### Riccardo Brasca (Oct 03 2023 at 12:32):

Well, then this is the way to go I think

#### Riccardo Brasca (Oct 03 2023 at 12:36):

Mmh, they define regular primes via Bernoulli numbers

The book is here

#### Riccardo Brasca (Oct 03 2023 at 12:36):

But they also prove flt, so somehow they must prove the connection with the class number

#### Chris Birkbeck (Oct 03 2023 at 12:40):

Yeah they have this $h^*$ and $h_0$ which I think correspond to the different definitions

#### Andrew Yang (Oct 03 2023 at 20:03):

I wonder if we could do the algebraic proof without going through the whole class field theory?
We only need the reciprocity law for an unramified Kummer extension $K(u^{1/p})/K$ with $K = \mathbb{Q}[\zeta_p]$.
Since $u$ is congruent to an integer modulo $p$, wouldn't Eisenstein reciprocity suffice?

#### Riccardo Brasca (Oct 03 2023 at 21:58):

It's possible that there are shortcuts, but personally I would rather prefer to develop the relevant tools (unless the short proof is much easier). It's just a personal opinion, but I think the main goals of projects like this one is to develop mathlib.

#### Antoine Chambert-Loir (Oct 04 2023 at 06:24):

You know, Kummer hadn't class field theory at his disposal, in 1850...
From what I read, the approach by constructing units is more in the spirit of the Leopoldt conjecture.

#### Anders Larsson (Oct 04 2023 at 06:34):

Just out of curiosity, what's the downsides with class field theory for solving FLT regular?

It seems from the threads here that most participants thinks they are not the best option here. But why is that?

#### Johan Commelin (Oct 04 2023 at 06:37):

I think mostly because CFT is a whole bunch of work

#### Riccardo Brasca (Oct 04 2023 at 06:38):

Antoine Chambert-Loir said:

You know, Kummer hadn't class field theory at his disposal, in 1850...
From what I read, the approach by constructing units is more in the spirit of the Leopoldt conjecture.

If I understand correctly we have already proved what Kummer proved, he supposed kummer's lemma, at least at the beginning, and then someone (maybe himself) realized that the condition is automatic.

#### Kevin Buzzard (Oct 04 2023 at 06:54):

Working on hard mathematical problems is a great way to expose the big machines that power everything. Working on number theory is exposing the fact that CFT is everywhere. I had a student working on Iwasawa theory and one plan was to prove Iwasawa's results on growth of class groups in a tower but this also relies on CFT for the descent step. CFT has long been known to be a bottleneck for the kind of things we want to do here and it will take a concerted effort to do it. The group at Imperial has started ploughing through Cassels-Froehlich but there is still a huge amount of work to do there before even the local results are proved, and of course the global ones are even harder.

#### Joël Riou (Oct 04 2023 at 10:56):

About CFT, I would recommend the book by my colleague David Harari Galois Cohomology and Class Field Theory (exists both in French and English) which is mostly self-contained.

#### Thomas Browning (Oct 04 2023 at 18:06):

When I was talking with @Filippo A. E. Nuccio about CFT, my memory was that Neukirch's "The Bonn Lectures" and the book by Artin and Tate navigate the cohomological approach quite well.

#### Filippo A. E. Nuccio (Oct 04 2023 at 19:30):

I certainly still believe that Artin-Tate is a very complete treatment of CFT (local+global) following the cohomological approach, and my (limited) knowledge of Harari's book is that in that respect it contains little novelty. What is really interesting in his book is the final part IV, where Poitou-Tate is discussed, whereas this is completely missing in Artin-Tate or Cassels-Fröhlich (and if one looks at Neukirch-Schmidt-Wingberg, then there are some 400 pages to digest assuming CFT). So, IMHO, if we are going to formalize the "basic" result of CFT, at least in the form

$\hat{H}^i(L/K,C_L) \cong \hat{H}^{i-2}(L/K,\mathbb{Z})\qquad \text{for all } i\in\mathbb{Z}$

(where $C_L$ denotes idèle classes), both Harari and Artin-Tate or Cassels-Fröhlich would do. I am sure that Poitou-Tate would certainly be interesting and necessary at some point, but for the time being we still lack so many more fundamental results that perhaps we could also let it aside for the time being.

#### Andrew Yang (Oct 04 2023 at 19:48):

IIRC Neukirch's "Class Field Theory" contains an purely algebraic exposition of CFT without analysis or homological algebra, which might be of interest?

#### Filippo A. E. Nuccio (Oct 04 2023 at 20:37):

Well, the references quoted above do basically the same: Neukirch's book is not significantly different from Artin-Tate, from which it borrows most of the proofs.

#### Thomas Browning (Oct 05 2023 at 01:35):

Be aware that there are two books of Neukirch titled "Class Field Theory". The Bonn Lectures is the one that deals with Tate cohomology groups.

#### Chris Birkbeck (Oct 05 2023 at 10:55):

Chris Birkbeck said:

Yeah they have this $h^*$ and $h_0$ which I think correspond to the different definitions

Ok so I was forgetting something that Kevin and others mentioned ages ago, in that, to show regular = Bernoulli regular one needs the analytic class number formula. I wen't back and checked Kummer's orginal proof (and even though I know no German) I think the class number formula is on page 1. So we could do something we mentioned at some point, which is to define something like super regular to be regular+Bernoulli regular and then we can prove the FLT super regular case (which shouldn't be too much work hopefully).

Then what remains is to prove that super regular = regular using the analytic class number formula, which is maybe less work than just going for the CFT proof? but who knows. Maybe there's already someone working on the analytic class number formula? or we start it or we leave it to someone else.

#### Riccardo Brasca (Oct 05 2023 at 11:17):

regular + bernoulli regular implies flt-regular amounts to regular + bernoulli regular implies kummer's lemma, and for this we can follow Conrad's notes, that look very doable (regular is probably useless, what he does is bernoulli regular implies kummer's lemma).

#### Riccardo Brasca (Oct 05 2023 at 11:25):

Well, I don't know how doable it is. It is certainly not very difficult mathematically, but with a lot of computations

#### Chris Birkbeck (Oct 05 2023 at 12:17):

hmm maybe I was wrong. I just found out that in this book by Swinnerton-Dyer, there is a extended excercise that maybe proves Kummer's lemma without Bernoulli numbers and without CFT. I need to check it more closely, but its on page 74-78

#### Chris Birkbeck (Oct 05 2023 at 12:48):

Its funny beause if true we have a proof by Swinnerton-Dyer that avoids calculating an algebraic invariant via an analytic method.

#### Kevin Buzzard (Oct 05 2023 at 13:30):

I've always suggested that you define regular to mean "all the conditions you need to make the proof work" and worry about the equivalence later. That way you can publish earlier. Another example of this shenanigans: there are two topologies you can put on an adic space and it's a lot of work with valuation theory to prove they coincide. The standard definition in the books is one topology, but in the perfectoid project we used the other topology because it made our life easier when constructing the structure presheaf. So it's a theorem that the lean definition equals the usual definition but we never formalised that theorem.

#### Andrew Yang (Nov 16 2023 at 08:21):

While I'm laying down some prerequisites for Kummer's lemma, I'm also thinking about the proof of Hilbert 92, but the proof in Swinnerton-Dyer seems a bit hard to formalize. I wonder if anyone has put thought into it and/or is working on it?

#### Chris Birkbeck (Nov 16 2023 at 08:22):

Is the proof in Hilberts book easier? It has more details I think and what was what I thought we would use for this result

#### Chris Birkbeck (Nov 16 2023 at 08:23):

But it does entail lots more dealing with units, which I remember being challenging at times

#### Johan Commelin (Nov 16 2023 at 09:24):

Wait, you mean Hilbert 90, right? Or have I somehow missed Hilbert 92 in the past 15 years of my life?

#### Chris Birkbeck (Nov 16 2023 at 09:24):

No we really mean 92. But don't worry I didn't know about it either until recently

#### Chris Birkbeck (Nov 16 2023 at 09:25):

We also need hilbert 90

#### Kevin Buzzard (Nov 16 2023 at 09:25):

Amelia has Hilbert 90 on a branch :-)

#### Chris Birkbeck (Nov 16 2023 at 09:25):

Kevin Buzzard said:

Amelia has Hilbert 90 on a branch :-)

Oh great, that'll be useful!

#### Kevin Buzzard (Nov 16 2023 at 09:26):

She's working on relating explicit constructions of H^1 via concrete cocycles to fancy ext constructions and has made great progress

#### Johan Commelin (Nov 16 2023 at 09:28):

Can someone please tell me the statement of Hilbert 92? A quick search on the internet only turned up silly pictures of Hilbert

#### Damiano Testa (Nov 16 2023 at 09:38):

I think that it is just the negation of Hilbert 92:

:upside_down:

image.png

#### Damiano Testa (Nov 16 2023 at 09:44):

This is what I searched for:

hilbert satz 92


I mean this as a "let me google that for you", but with love, rather than passive-aggressiveness!

#### Kevin Buzzard (Nov 16 2023 at 09:46):

I tried this on duck duck go and got nowhere, and so then I tried Google and it was successful.

#### Oliver Nash (Nov 16 2023 at 09:55):

FWIW, McQuillan's article is the fifth result using DDG for me. I'm happy to make a small effort to avoid using the company that decided it no longer believed in don't be evil

#### Chris Birkbeck (Nov 16 2023 at 09:56):

Johan Commelin said:

Can someone please tell me the statement of Hilbert 92? A quick search on the internet only turned up silly pictures of Hilbert

It's in the blueprint here: https://leanprover-community.github.io/flt-regular/blueprint/sect0005.html

#### Chris Birkbeck (Nov 16 2023 at 09:57):

(or what Damiano said)

#### Riccardo Brasca (Nov 16 2023 at 10:12):

It will be really satisfactory when it will be formalized!

#### Riccardo Brasca (Nov 16 2023 at 10:12):

BTW @Chris Birkbeck lemma 5.1 is for sure in mathlib

#### Chris Birkbeck (Nov 16 2023 at 10:13):

Riccardo Brasca said:

BTW Chris Birkbeck lemma 5.1 is for sure in mathlib

Yeah, now that I look at it, I dont remember why I added it to the blueprint (there are much harder things not yet in the blueprint)

#### Riccardo Brasca (Nov 16 2023 at 10:18):

It is something like docs#isIntegrallyClosed_iff

#### Andrew Yang (Nov 16 2023 at 10:22):

I think it is docs#IsIntegralClosure.isLocalization.

#### Eric Rodriguez (Nov 16 2023 at 10:25):

So the content of 92 is that the eps in 90 isn't always a unit?

#### Andrew Yang (Nov 16 2023 at 10:26):

It states that it is never a unit.

#### Chris Birkbeck (Nov 16 2023 at 10:27):

No it says that there is some element (of norm one) which can't be of the form $\epsilon /\sigma(\epsilon)$ for $\epsilon$ a unit.

#### Andrew Yang (Nov 16 2023 at 10:27):

The proof in Hilbert's book does look more formalizable. At least we don't need to calculate the rank of the unit group.
Pasting it here for (my) convenience:
image.png
image.png

#### Chris Birkbeck (Nov 16 2023 at 10:29):

Andrew Yang said:

It states that it is never a unit.

Oh sorry, maybe I misunderstood what you meant. Given that $\eta$ then yes, the $\epsilon$ is never a unit

#### Chris Birkbeck (Nov 16 2023 at 10:31):

Andrew Yang said:

The proof in Hilbert's book does look more formalizable. At least we don't need to calculate the rank of the unit group.
Pasting it here for (my) convenience:
image.png
image.png

Don't we have Dirichlet's unit theorem? But I agree its nice if we dont need to use it. But I don't remember if its used in the relative unit construction.

#### Ruben Van de Velde (Nov 16 2023 at 10:31):

Is this what 5.1 means?

import Mathlib

variable (K : Type*) [Field K] [NumberField K] (α : K)

example : ∃ k : ℤ, k ≠ 0 ∧ IsAlgebraic ℤ (k • α) := by
obtain ⟨y, hy, h⟩ := exists_integral_multiples ℤ ℚ (L := K) {α}
refine ⟨y, hy, h α (Finset.mem_singleton_self _) |>.isAlgebraic⟩


#### Chris Birkbeck (Nov 16 2023 at 10:32):

Yep that looks like right.

#### Riccardo Brasca (Nov 16 2023 at 10:33):

Chris Birkbeck said:

Andrew Yang said:

The proof in Hilbert's book does look more formalizable. At least we don't need to calculate the rank of the unit group.
Pasting it here for (my) convenience:
image.png
image.png

Don't we have Dirichlet's unit theorem? But I agree its nice if we dont need to use it. But I don't remember if its used in the relative unit construction.

We have the rank. docs#NumberField.Units.rank

#### Andrew Yang (Nov 16 2023 at 10:34):

Yeah the proof in Swinnerton-Dyer uses expcitly that the rank of the relative unit group of $F[\sqrt[p]{u}]/F$ is $(p - 1)^2/2$. It is not hard but still non-trivial to calculate this from what we have, I think.

#### Eric Rodriguez (Nov 16 2023 at 11:50):

sorry, I feel like I'm a bit confused - is this correct?

Hilbert 90 says that for all a : K with N_K/F(a) = 1, then a = b/o(b) for some b : O_K.
Hilbert 92 says that there exists some unit u : O_K but it is _not_ of the form b/o(b) for some _unit_ b : O_K

#### Chris Birkbeck (Nov 16 2023 at 11:53):

Yeah exactly, in 92 you still have it has norm one, so Hilbert 90 applies, but the $b$ you have can't be a unit (for the specific choice of $u$)

(deleted)

#### Andrew Yang (Nov 16 2023 at 17:31):

I have reduced Kummer's lemma to Hilbert 90 and Hilbert 92 following the blueprint: https://github.com/leanprover-community/flt-regular/pull/97.

#### Andrew Yang (Nov 16 2023 at 17:31):

The downside is that I have doubled the sorries :P

#### Riccardo Brasca (Nov 16 2023 at 17:32):

I can have a look tomorrow, but I don't see any problem in merging it!

#### Riccardo Brasca (Nov 16 2023 at 17:33):

@Andrew Yang this is still the abstract thing, right? Without connections with Bernoulli numbers?

#### Andrew Yang (Nov 16 2023 at 17:33):

Yes. No Bernoulli and no analysis.

#### Riccardo Brasca (Nov 16 2023 at 17:34):

That's still a fantastic job!

#### Riccardo Brasca (Nov 16 2023 at 17:36):

@Amelia Livingston (I am subscribing you to the stream, sorry for the noise), do you have Hilbert 90 somewhere?

#### Chris Birkbeck (Nov 16 2023 at 17:36):

So is this the ramification bits of the proof as well?

#### Chris Birkbeck (Nov 16 2023 at 17:39):

Oh wow it is, amazing! I was dreading dealing with that part (for no serious reasons)

#### Riccardo Brasca (Nov 16 2023 at 17:45):

@Andrew Yang can you summarize what do you prove about unramified extensions? This seems something can go very quickly in mathlib

#### Amelia Livingston (Nov 23 2023 at 15:39):

Apologies for my very slow reply - I'm opening a PR with Noether's generalisation of Hilbert 90 in a moment. I wanted to deduce the original version about cyclic extensions by showing what the cohomology of a general finite cyclic group is, which might take a few more PRs.

#### Riccardo Brasca (Nov 23 2023 at 16:34):

No pressure, and thanks a lot!!

#### Riccardo Brasca (Nov 24 2023 at 10:25):

The PR is #8599. I will try to prove our version from Amelia's (and review the PR).

#### Riccardo Brasca (Nov 24 2023 at 10:56):

@Amelia Livingston do we have anything about cocycles for cyclic groups?

#### Riccardo Brasca (Nov 24 2023 at 11:20):

Good news, adapting Amelia's formulation seems very easy. The proof of Hilbert90 contains now 3 sorry: the first is trivial (I am just lazy), and the third one should be easy, but I think it should be done at the same time as the second developing a reasonable API.

#### Eric Rodriguez (Nov 24 2023 at 11:24):

Did you push this to flt-reg?

Yes

#### Riccardo Brasca (Nov 24 2023 at 11:24):

Feel free to finish the sorry if you want

#### Amelia Livingston (Nov 24 2023 at 11:45):

Riccardo Brasca said:

Amelia Livingston do we have anything about cocycles for cyclic groups?

Not yet, but working on that kind of thing at the moment. I'll PR API that would be useful for your proof first and then do cohomology of finite cyclic groups.

#### Riccardo Brasca (Nov 24 2023 at 15:46):

My formula for the cocycle was wrong, it should be

let f : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ η ⬝ σ(η) ⬝... ⬝ σ^(i-1)(η)


where η = σ^i. Anyway we should develop the general theory.

#### Amelia Livingston (Nov 24 2023 at 17:55):

Trying to prove that that's a 1-cocycle but the required lemmas seem mostly specific to that particular function - the only slightly useful general thing I could isolate was that if G is finite and cyclic with a generator g and f: G -> A is a function satsifyingf (gⁿ) = ∑ i < n, gⁱ • (f g) for all n : ℕ, then f is a 1-cocycle. Am I missing something? If not, I'll just focus on doing cohomology of general finite cyclic groups so that e.g. H^1(G, A) = Ker(N)/(g-1)A for g a generator. (and applying your review comments :smile: )

#### Riccardo Brasca (Nov 24 2023 at 20:45):

The only thing it's needed is that if the Galois group is cyclic you can specify a cocycle choosing the image of the generator. If I didn't make any mistake the formula is the one I wrote above, but the point is to find a cocycle that sends the generator to whatever you want.

#### Riccardo Brasca (Nov 27 2023 at 11:01):

I've added a reasonable definition of f. It is

let φ := (finEquivZpowers _ (isOfFinOrder_of_finite σ)).symm
let f : (L ≃ₐ[K] L) → Lˣ := fun τ ↦  ∏ i in range (φ ⟨τ, hσ τ⟩), Units.map (σ ^ i) ηu


here ηu is η as a unit.

#### Riccardo Brasca (Nov 27 2023 at 11:16):

And I don't think is possible to completely avoid it to get the version with the elements of norm 1.

#### Riccardo Brasca (Nov 27 2023 at 18:20):

Hilbert90 is done. It only depends on hilbert90 that is literally the statement proved in #8599. @Amelia Livingston if you want to have a look feel free to copy my code to prove this version.

#### Amelia Livingston (Nov 28 2023 at 18:43):

Awesome, thank you very much! Maybe I should add it as the next PR so the current one doesn't get too long?

#### Riccardo Brasca (Nov 28 2023 at 18:47):

Yes, that's a good idea.

#### Riccardo Brasca (Nov 29 2023 at 20:27):

@Filippo A. E. Nuccio says there is maybe a cohomological PROOF of Hilbert 92

#### Riccardo Brasca (Nov 29 2023 at 20:28):

we are interested in anything about it

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:28):

Well, actually I say that the "reasonable" proof is cohomological. The one I have in mind relies on the isomorphism $\hat{H}^{-1}\cong\hat{H}^1$ for cyclic groups.

#### Riccardo Brasca (Nov 29 2023 at 20:28):

This is Tate cohomology, right?

Yes

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:30):

But the iso is explicit each time you fix a degree, so if you only want it for $-1$ and $1$ you migh not need the full theory.

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:33):

I will try to come up with a nice proof and will report here if I get somewhere.

#### Riccardo Brasca (Nov 29 2023 at 20:33):

For everybody interested here is a recap of what's going on.

Hilbert 92 is the only sorry left to finish the proof of FLT for regular primes (but we don't have the connection of regularity with Bernoulli's number, so checking that 19 is regular is basically impossible in Lean).

Hilbert 92 is the following statement:
let $L/K$ a degree $p$ Galois extension of number fields (in our application we can suppose that $K$ is the $p$-th cyclotomic extension of $\mathbb{Q}$, but this is not needed), where $p > 2$ is prime. Let $G$ be the Galois group and let $U = \mathcal{O}_L^\ast$. Then $H^1(G, U)$ is non trivial.

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:36):

Just to know (I might not need it neither): for you, are the assumptions that $K=\mathbb{Q}(\zeta_p)$ and $[L:K]=p$ really enough? I mean: if I find an easier proof in this case, would it suffice?

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:36):

(and I guess you mean $H^1(G,U)$)

#### Riccardo Brasca (Nov 29 2023 at 20:38):

So it is like Hilbert 90, but one replaces $L^\ast$ with $U$ and the cohomology is non trivial.

Like for Hilbert 90, one can easily (and I mean easily in Lean) translates the statement in a statement about units of norm $1$. In this case we are looking for a unit $\eta$ in $U$ of norm $1$ that is not of the form $\varepsilon / \sigma(\varepsilon)$, where $\varepsilon$ is another unit and $\sigma$ is a generator of the Galois group.

#### Riccardo Brasca (Nov 29 2023 at 20:40):

Filippo A. E. Nuccio said:

Just to know (I might not need it neither): for you, are the assumptions that $K=\mathbb{Q}(\zeta_p)$ and $[L:K]=p$ really enough? I mean: if I find an easier proof in this case, would it suffice?

For us the base field if $\mathbb{Q}(\zeta_p)$, we don't think this really simplify the proof (one has to separate the case where there are roots of unit in the smaller field, but our case is the difficult one).

#### Riccardo Brasca (Nov 29 2023 at 20:41):

On the other hand the assumption that $G$ is cyclic is surely crucial, and the fact that it is of order $p$ helps, since in this case the group algebra is just $\mathbb{Z}[X]/(1+X+ \ldots X^{p-1})$

#### Riccardo Brasca (Nov 29 2023 at 20:42):

this last ring is isomorphic to $\mathbb{Z}[\zeta_p]$ (but this is unrelated to our other assumption that $K$ is cyclotomic, this is what confused me in my first message to you), and we know a lot of stuff about this ring.

#### Riccardo Brasca (Nov 29 2023 at 20:45):

So, we are following Hilbert's original proof (slightly modernized by Swinnerton-Dyer), that is rather elementary, but not so fun to formalize.

It is almost surely doable in very reasonable amount of time, but it would be very nice to find a more conceptual proof.

#### Riccardo Brasca (Nov 29 2023 at 20:46):

Any proof of this

variable (p : ℕ+) {K : Type*} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
variable {k : Type*} [Field k] [NumberField k] (hp : Nat.Prime p)

lemma Hilbert92
[Algebra k K] [IsGalois k K] [FiniteDimensional k K]
(hKL : finrank k K = p) (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) :
∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := sorry


would finish the project.

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:49):

Can you explain (hσ : ∀ x, x ∈ Subgroup.zpowers σ)?

#### Eric Rodriguez (Nov 29 2023 at 20:49):

We are saying the extension is cyclic

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:49):

So x is an element of the Galois group?

#### Riccardo Brasca (Nov 29 2023 at 20:51):

Yes, sorry for the notation (that Lean code literally compiles)

#### Riccardo Brasca (Nov 29 2023 at 20:51):

σ is the generator

#### Riccardo Brasca (Nov 29 2023 at 20:51):

I mean, we choose a generator

#### Riccardo Brasca (Nov 29 2023 at 20:53):

Feel free to assume that p is odd.

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:53):

OK, all good (if we were forced to specify the type of x the code would be easier to read)

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:53):

Riccardo Brasca said:

Feel free to assume that p is odd.

Sure!

#### Filippo A. E. Nuccio (Nov 29 2023 at 20:54):

Thanks, I will think about it.

#### Andrew Yang (Nov 29 2023 at 21:10):

The most straightforward cohomological proof is to show that the herbrand quotient $h(G_{K/k}, U_K) = \frac{1}{[K:k]} \prod_{p | \infty} e(p)$ if $K/k$ is cyclic. Now if $[K:k]$ is an odd prime then it is unramified at Archimedean places so $h(G_{K/k}, U_K) = 1/p$, i.e. $|\hat{H}^1(G, U_K)|= p |\hat{H}^0(G, U_K)| > 1$.

#### Andrew Yang (Nov 29 2023 at 21:12):

For a proof of the herbrand quotient, see Lang's Algebraic number theory IX §4.

#### Riccardo Brasca (Nov 29 2023 at 21:12):

Yes, this is the modern proof, but it needs some class field theory I think

#### Filippo A. E. Nuccio (Nov 29 2023 at 21:17):

No, it does not class field theory. It only needs Dirichlet's unit's theorem and some group cohomology. The one I like is given on pages 178--179 of Tate's paper in Cassels-Fröhlich.

#### Filippo A. E. Nuccio (Nov 29 2023 at 21:17):

But I think it is still hard to formalize it with what we have in mathlib

#### Xavier Roblot (Nov 30 2023 at 11:07):

I agree with Filippo that proving the general statement would be quite difficult with what we have at the moment in Mathlib. There is still the possibility that proving an ad-hoc version may be simpler. Looking at the code, is it correct that the version you need is the following:
$K = \mathbb{Q}(\zeta_p, u^{1/p})$ where $u$ is an unit of $\mathbb{Q}(\zeta_p)$ such that $u \equiv 1 \pmod{(\zeta_p-1)^p}$

#### Chris Birkbeck (Nov 30 2023 at 11:24):

Yes I think that's correct

#### Andrew Yang (Nov 30 2023 at 11:39):

As a plus, $K$ is even unramified over $\mathbb{Q}(\zeta_p)$.
However, I'm not inclined to proving anything more specific or weaker than what we are aiming for, considering we already have a relatively short (though maybe a bit painful) path in sight.

#### Riccardo Brasca (Nov 30 2023 at 11:53):

I agree with Andrew. If we can improve the proof (finding a more conceptual proof) than we should go for it, otherwise let's just follows Hilbert. It's 19th math, but it still OK.

#### Filippo A. E. Nuccio (Dec 02 2023 at 15:52):

Andrew Yang said:

As a plus, $K$ is even unramified over $\mathbb{Q}(\zeta_p)$.
However, I'm not inclined to proving anything more specific or weaker than what we are aiming for, considering we already have a relatively short (though maybe a bit painful) path in sight.

Hold on, what do you mean that $K$ is unramified over $\mathbb{Q}(\zeta_p)$? Are you arguing by contradiction?

#### Filippo A. E. Nuccio (Dec 02 2023 at 15:53):

If $p$ is regular, $\mathbb{Q}(\zeta_p)$ should not have any degree-$p$ extensions that is unramified...

#### Andrew Yang (Dec 02 2023 at 16:27):

Filippo A. E. Nuccio said:

Yes. The main goal is Hilbert 94, which states that if $K/k$ is a degree $p$ unramified cyclic extension, then $p | \mathcal{O}_k$