Kummer's lemma

Stream: FLT-regular

[Riccardo Brasca]

@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]

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]

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]

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]

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]

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]

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

[Chris Birkbeck]

Is that not case I?

[Eric Rodriguez]

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

[Chris Birkbeck]

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]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

In the blueprint I mean

[Kevin Buzzard]

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

[Chris Birkbeck]

yes

[Kevin Buzzard]

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

[Chris Birkbeck]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

I agree this seems the best solution.

[Kevin Buzzard]

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]

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]

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]

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]

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

[Eric Rodriguez]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

@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]

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]

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]

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]

"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]

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]

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]

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]

This is why they'll love flt_regular ;-)

[Eric Rodriguez]

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 :)

[Chris Birkbeck]

15 does work...

[Chris Birkbeck]

i.e. its not a counter example

[Chris Birkbeck]

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]

oh my god they grow so fast

[Eric Rodriguez]

I thought they were quite small! Dear lord

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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

[Thomas Browning]

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

[Antoine Chambert-Loir]

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]

So 56 is an irregular number!

[Riccardo Brasca]

@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]

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]

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]

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]

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]

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]

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

[Chris Birkbeck]

Is that not case I?

[Eric Rodriguez]

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

[Chris Birkbeck]

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]

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]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

In the blueprint I mean

[Kevin Buzzard]

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

[Chris Birkbeck]

yes

[Kevin Buzzard]

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

[Chris Birkbeck]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

I agree this seems the best solution.

[Kevin Buzzard]

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]

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]

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]

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]

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

[Eric Rodriguez]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

@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]

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]

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]

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]

"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]

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]

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]

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]

This is why they'll love flt_regular ;-)

[Eric Rodriguez]

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 :)

[Chris Birkbeck]

15 does work...

[Chris Birkbeck]

i.e. its not a counter example

[Chris Birkbeck]

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]

oh my god they grow so fast

[Eric Rodriguez]

I thought they were quite small! Dear lord

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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

[Thomas Browning]

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

[Antoine Chambert-Loir]

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]

So 56 is an irregular number!

[Johan Commelin]

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]

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]

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

[Riccardo Brasca]

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

[Ruben Van de Velde]

What's with the duplicated comments?

[Antoine Chambert-Loir]

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.
https://kconrad.math.uconn.edu/blurbs/gradnumthy/kummer.pdf

[Chris Birkbeck]

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

[Ruben Van de Velde]

6.5 pages, how hard can it be :sweat_smile:

[Antoine Chambert-Loir]

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

[Riccardo Brasca]

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]

Yes I think they also connect with Bernoulli numbers.

[Riccardo Brasca]

Well, then this is the way to go I think

[Riccardo Brasca]

Mmh, they define regular primes via Bernoulli numbers

[Chris Birkbeck]

The book is here

[Riccardo Brasca]

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

[Chris Birkbeck]

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

[Andrew Yang]

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]

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]

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]

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]

I think mostly because CFT is a whole bunch of work

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Chris Birkbeck]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Johan Commelin]

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

[Chris Birkbeck]

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

[Chris Birkbeck]

We also need hilbert 90

[Kevin Buzzard]

Amelia has Hilbert 90 on a branch :-)

[Chris Birkbeck]

Kevin Buzzard said:

Amelia has Hilbert 90 on a branch :-)

Oh great, that'll be useful!

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Damiano Testa]

https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=&cad=rja&uact=8&ved=2ahUKEwix7P3QnMiCAxVG_7sIHWevAxgQFnoECBcQAQ&url=https%3A%2F%2Fbibliotekanauki.pl%2Farticles%2F1393835.pdf&usg=AOvVaw04Hw__XTobnY76VgtyylX5&opi=89978449

:upside_down:

[Damiano Testa]

image.png

[Damiano Testa]

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]

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

[Johan Commelin]

Classical duck-duck-no :sad:

[Oliver Nash]

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]

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]

(or what Damiano said)

[Kevin Buzzard]

Finally a satisfactory answer :-)

[Riccardo Brasca]

It will be really satisfactory when it will be formalized!

[Riccardo Brasca]

BTW @Chris Birkbeck lemma 5.1 is for sure in mathlib

[Chris Birkbeck]

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]

It is something like docs#isIntegrallyClosed_iff

[Andrew Yang]

I think it is docs#IsIntegralClosure.isLocalization.

[Eric Rodriguez]

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

[Andrew Yang]

It states that it is never a unit.

[Chris Birkbeck]

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]

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]

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]

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]

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]

Yep that looks like right.

[Riccardo Brasca]

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]

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]

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]

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$)

[Chris Birkbeck]

(deleted)

[Andrew Yang]

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]

The downside is that I have doubled the sorries :P

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Andrew Yang]

Yes. No Bernoulli and no analysis.

[Riccardo Brasca]

That's still a fantastic job!

[Riccardo Brasca]

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

[Chris Birkbeck]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

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

[Amelia Livingston]

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]

No pressure, and thanks a lot!!

[Riccardo Brasca]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

Did you push this to flt-reg?

[Riccardo Brasca]

Yes

[Riccardo Brasca]

Feel free to finish the sorry if you want

[Amelia Livingston]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

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]

Yes, that's a good idea.

[Riccardo Brasca]

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

[Riccardo Brasca]

we are interested in anything about it

[Filippo A. E. Nuccio]

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]

This is Tate cohomology, right?

[Filippo A. E. Nuccio]

Yes

[Filippo A. E. Nuccio]

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]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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

[Eric Rodriguez]

We are saying the extension is cyclic

[Filippo A. E. Nuccio]

So x is an element of the Galois group?

[Riccardo Brasca]

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

[Riccardo Brasca]

σ is the generator

[Riccardo Brasca]

I mean, we choose a generator

[Riccardo Brasca]

Feel free to assume that p is odd.

[Filippo A. E. Nuccio]

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

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Feel free to assume that p is odd.

Sure!

[Filippo A. E. Nuccio]

Thanks, I will think about it.

[Andrew Yang]

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]

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

[Riccardo Brasca]

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

[Filippo A. E. Nuccio]

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]

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

[Xavier Roblot]

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]

Yes I think that's correct

[Andrew Yang]

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]

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]

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]

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

[Andrew Yang]

Filippo A. E. Nuccio said:

Are you arguing by contradiction?

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$