Zulip Chat Archive

Stream: FLT-regular

Topic: zeta vs zeta'

Eric Rodriguez (Dec 27 2021 at 19:08):

do we have any particular reason to keep zeta around? to me it seems that zeta' is much better behaved

Alex J. Best (Dec 27 2021 at 19:44):

Sometimes you really want to consider zeta' as a unit right?

Alex J. Best (Dec 27 2021 at 19:45):

Even if it's not used as much i find it hard to imagine it's totally useless

Eric Rodriguez (Dec 28 2021 at 00:50):

I think we can certainly make the current zeta' be a unit; I just worry because it uses the explicit constructions and I'd rather avoid that if possible

Eric Rodriguez (Dec 28 2021 at 00:52):

hmm, there's a lot of zeta in Unit_lemmas... I'll have a toy with this at some point

Eric Rodriguez (Dec 28 2021 at 01:27):

ooh, we can even put it in the roots_of_unity subgroup

Eric Rodriguez (Dec 28 2021 at 01:30):

even unconditionally, with Riccardo's power stuff; it's only primitive on the ne_zero (n : R) case though

Riccardo Brasca (Dec 28 2021 at 03:16):

We can maybe change the name, using zeta for zeta' and something like zeta_unit for zeta.

Riccardo Brasca (Dec 28 2021 at 03:17):

In any case we know the order of zeta', it is given by is_root_cyclotomic_iff_char_p when ne_zero does not hold, but I think we can safely assume ne_zero.

Eric Rodriguez (Dec 28 2021 at 04:43):

I started toying with this; I think it's definitely worth having zeta and zeta_root_of_unity involved. Here's some work on this; no renaming and no removing of the old zeta yet, but if people want to push anything here, feel free!

Eric Rodriguez (Dec 28 2021 at 04:44):

We'll get some of the theorems for free, too, from roots_of_unity :)

Riccardo Brasca (Dec 28 2021 at 16:34):

Good! The definition of cyclotomic extension is now in mathlib: I will keep on PRing small properties, but the next relevant step is to have zeta and their basic properties. Do you agree on using zeta instead of zeta'?

Chris Birkbeck (Dec 28 2021 at 16:50):

I'm confused about which is which now. zeta' is the root of the cyclotomic poly and zeta is the same thing but as an element of the units of the ring of integers?

Chris Birkbeck (Dec 28 2021 at 16:53):

In the proof I guess the main one will be zeta as most of the arguments happen in the ring of integers.

Riccardo Brasca (Dec 28 2021 at 16:53):

For now zeta' is any root the the cyclotomic polynomial:

def zeta' : B :=
classical.some (exists_root (set.mem_singleton n) : ∃ r : B, aeval r (cyclotomic n A) = 0)

Riccardo Brasca (Dec 28 2021 at 16:53):

So it is an element of the big algebra, and we know is_primitive_root (zeta') (with the appropriate assumptions).

Eric Rodriguez (Dec 28 2021 at 16:58):

the current zeta has a fair few typeclass issues... I should put this thread in the code; we can rederive some instances so hopefully TC search doesn't do this

Alex J. Best (Dec 28 2021 at 16:58):

Renaming zeta' to zeta and zeta to zeta_unit or something sounds sensible to me, sorry for the original non descriptive name

Chris Birkbeck (Dec 28 2021 at 17:00):

Yeah I agree, the name zeta_unit is a good idea.

Eric Rodriguez (Dec 28 2021 at 17:01):

do people like my new definition in the branch? I think we can get easily that it's in the ring of integers (we can probably make an is_cyclotomic_extension instance for ring_of_integers K for K : is_cyclotomic_extension)

Chris Birkbeck (Dec 28 2021 at 17:04):

I like it being a root of unity. If we can easily make it into an element of the ring of integers, then I think that's fine. Does this fix any of these TC issues?

Riccardo Brasca (Dec 28 2021 at 17:05):

Sorry, which branch?

Chris Birkbeck (Dec 28 2021 at 17:05):

(I haven't really followed the discussion on these TC issues)

Eric Rodriguez (Dec 28 2021 at 17:05):

https://github.com/leanprover-community/flt-regular/commits/zeta_refactor

Eric Rodriguez (Dec 28 2021 at 17:05):

the TC issues aren't really fleshed out, I'm still digging around because it's not really an easy to fix issue

Chris Birkbeck (Dec 28 2021 at 17:06):

Aha I see.

Riccardo Brasca (Dec 28 2021 at 17:07):

Having zeta as a root of unity seems a very good idea!

Riccardo Brasca (Dec 28 2021 at 17:08):

I guess we are not loosing anything, and we can use the existing API for roots of unity

Eric Rodriguez (Dec 31 2021 at 04:50):

I've pushed some more onto that branch, I think it's nearly there. If anyone has any suggestions (either golfing or maths) for the ring_of_integers proof, please let me know. I think it may require fintype S; I don't see how it would, but if helps to consider S as a singleton, I feel like that's fine too

Riccardo Brasca (Dec 31 2021 at 13:50):

I don't have a lot of time today, I will try to have a look during the weekend, but if it compiles feel free to merge into master

Riccardo Brasca (Jan 02 2022 at 16:49):

I will check this tomorrow, sorry for the delay

Eric Rodriguez (Jan 02 2022 at 16:54):

no worries ^^ I've been very busy too so also not had much time to do things

Riccardo Brasca (Jan 03 2022 at 15:10):

@Eric Rodriguez the class ne_zero is now in mathib, right? If there there are no more PR to wait for I think we should first of all start using it everywhere

Riccardo Brasca (Jan 03 2022 at 15:11):

And then refactor zeta

Riccardo Brasca (Jan 03 2022 at 15:15):

Ah, bors failed in #11071 because of some changes in master. @Johan Commelin since it is now fixed, can you merge it? Thank you!

Eric Rodriguez (Jan 03 2022 at 22:00):

ahh, I was already bumping master Riccardo! should've said here, sorry ^^

Riccardo Brasca (Jan 03 2022 at 22:26):

:grinning_face_with_smiling_eyes:

Riccardo Brasca (Jan 03 2022 at 22:27):

No problem! Have you already finished the bump?

Eric Rodriguez (Jan 03 2022 at 22:29):

no, doing some of the leaf files right now

Eric Rodriguez (Jan 03 2022 at 22:29):

give me a couple minutes and I'll push what I have

Riccardo Brasca (Jan 03 2022 at 22:30):

OK, I've fixed src/ready_for_mathlib/cyclotomic/basic.lean and src/ready_for_mathlib/cyclotomic.lean.

Riccardo Brasca (Jan 03 2022 at 22:30):

I've added two simple lemmas in src/ready_for_mathlib/ne_zero.lean. I will PR them later

Eric Rodriguez (Jan 03 2022 at 22:39):

btw, ne_nat exists as (ne_zero.of_ne_zero_coe R).out; a bit of a motuhful, I agree, but that's mathlib naming for ya...

Riccardo Brasca (Jan 03 2022 at 22:41):

So let's throw the whole file away

Eric Rodriguez (Jan 03 2022 at 22:49):

there was actually some other lemmas that I put in therre ^^ sorry for overriding half the stuff, but I merged now

Eric Rodriguez (Jan 03 2022 at 22:50):

I've been trying to use no_zero_smul_divisors a bit more because it seems to be a bit easier to scale than injective algerbra maps (they're equivalent); otherwise we just did pretty much the same

Eric Rodriguez (Jan 03 2022 at 22:50):

I also messed a little with cycl_poly; the last lemma now takes ne_zero and doesn't require 0 < k

Eric Rodriguez (Jan 03 2022 at 22:50):

I'm going to work on the discirminant file now

Eric Rodriguez (Jan 03 2022 at 22:56):

ok, the bump should be done now

Riccardo Brasca (Jan 03 2022 at 23:00):

I also get some timeout in src/number_theory/cyclotomic/cyclotomic_units.lean, but it compiles in the terminal

Riccardo Brasca (Jan 03 2022 at 23:02):

BTW if you want to make it working in VS Code it suffices to increase the time limit

Eric Rodriguez (Jan 03 2022 at 23:07):

yeah, it's so weird... anyways, hopefully that will be gone with the remaster soon so

Eric Rodriguez (Jan 03 2022 at 23:08):

refactor*...

Eric Rodriguez (Jan 04 2022 at 05:56):

ok, zeta_refactors _builds_; I broke a lot of your stuff though, @Alex J. Best ; if you have any free time at some point would be great if you could take a look. The more I think about it I think I used the wrong zeta over in your stuff

Eric Rodriguez (Jan 04 2022 at 05:57):

and so I had to sorry a few previously unsorried things. I'll see if I can think about those things a bit more carefully tomorrow

Eric Rodriguez (Jan 04 2022 at 05:58):

quicklink: https://github.com/leanprover-community/flt-regular/tree/zeta_refactor

Riccardo Brasca (Jan 10 2022 at 13:39):

@Eric Rodriguez what is the situation with your refactor of zeta? I would like to PR the definition and some basic properties

Eric Rodriguez (Jan 10 2022 at 14:42):

still just trying to crack on and deal with some ring of integers stuff, feel free to merge but stuff isn't quite at feature parity yet

Eric Rodriguez (Jan 10 2022 at 22:00):

ohhh, I see what the issue is, and how to get around ir

Eric Rodriguez (Jan 10 2022 at 22:01):

essentially, I wanted to define is_cyclotomic_extension (O K) (O L) for is_cyclotomic_extension K L, but this doesn't work

Eric Rodriguez (Jan 10 2022 at 22:01):

we instead have is_cyclotomic_extension (O K) (cyclotomic_ring blah O K), and it is a theorem of Q that cyclotomic_ring O K is O L

Eric Rodriguez (Jan 10 2022 at 22:02):

which is what you're proving right now riccardo

Eric Rodriguez (Jan 10 2022 at 22:02):

so i'm just going to try to get the current stuff building somehow and then work from there

Riccardo Brasca (Jan 10 2022 at 22:11):

Yes, currently the definition of cyclotomic_ring is the ring obtained adjoining the roots of the cyclotomic polynomials. In particular the proof that it is a cyclotomic extension should be easy (maybe it's even already there). The difficult part is that in the case of Q it is also the integral closure of Z.

Riccardo Brasca (Jan 10 2022 at 22:19):

If your new definition works don't hesitate to merge into master!

Riccardo Brasca (Jan 10 2022 at 22:19):

Don't worry if you add some more sorry

Riccardo Brasca (Jan 11 2022 at 15:57):

I've merged master in zeta_refactor

Riccardo Brasca (Jan 11 2022 at 16:00):

And I am trying to fix the errors

Riccardo Brasca (Jan 11 2022 at 16:30):

@Eric Rodriguez It now compiles (I just had to add some sorry, we will fix them sooner or later). I think having zeta instead of zeta' is better. If you are satisfied with the definition you can merge into master.

Riccardo Brasca (Jan 11 2022 at 16:31):

We are now quite close to the computation of the ring of integers of the cyclotomic extension of the rationals, that is already a non trivial result, so I would like to PR all the stuff leading to it quite soon.

Eric Rodriguez (Jan 11 2022 at 17:07):

sure, argh sorry didn't want to break people's stuff but will merge then

Eric Rodriguez (Jan 11 2022 at 17:16):

oki, done, i'll now add docstrings and things will build again

Eric Rodriguez (Dec 27 2021 at 19:08):

do we have any particular reason to keep zeta around? to me it seems that zeta' is much better behaved

Alex J. Best (Dec 27 2021 at 19:44):

Sometimes you really want to consider zeta' as a unit right?

Alex J. Best (Dec 27 2021 at 19:45):

Even if it's not used as much i find it hard to imagine it's totally useless

Eric Rodriguez (Dec 28 2021 at 00:50):

I think we can certainly make the current zeta' be a unit; I just worry because it uses the explicit constructions and I'd rather avoid that if possible

Eric Rodriguez (Dec 28 2021 at 00:52):

hmm, there's a lot of zeta in Unit_lemmas... I'll have a toy with this at some point

Eric Rodriguez (Dec 28 2021 at 01:27):

ooh, we can even put it in the roots_of_unity subgroup

Eric Rodriguez (Dec 28 2021 at 01:30):

even unconditionally, with Riccardo's power stuff; it's only primitive on the ne_zero (n : R) case though

Riccardo Brasca (Dec 28 2021 at 03:16):

We can maybe change the name, using zeta for zeta' and something like zeta_unit for zeta.

Riccardo Brasca (Dec 28 2021 at 03:17):

In any case we know the order of zeta', it is given by is_root_cyclotomic_iff_char_p when ne_zero does not hold, but I think we can safely assume ne_zero.

Eric Rodriguez (Dec 28 2021 at 04:43):

I started toying with this; I think it's definitely worth having zeta and zeta_root_of_unity involved. Here's some work on this; no renaming and no removing of the old zeta yet, but if people want to push anything here, feel free!

Eric Rodriguez (Dec 28 2021 at 04:44):

We'll get some of the theorems for free, too, from roots_of_unity :)

Riccardo Brasca (Dec 28 2021 at 16:34):

Good! The definition of cyclotomic extension is now in mathlib: I will keep on PRing small properties, but the next relevant step is to have zeta and their basic properties. Do you agree on using zeta instead of zeta'?

Chris Birkbeck (Dec 28 2021 at 16:50):

I'm confused about which is which now. zeta' is the root of the cyclotomic poly and zeta is the same thing but as an element of the units of the ring of integers?

Chris Birkbeck (Dec 28 2021 at 16:53):

In the proof I guess the main one will be zeta as most of the arguments happen in the ring of integers.

Riccardo Brasca (Dec 28 2021 at 16:53):

For now zeta' is any root the the cyclotomic polynomial:

def zeta' : B :=
classical.some (exists_root (set.mem_singleton n) : ∃ r : B, aeval r (cyclotomic n A) = 0)

Riccardo Brasca (Dec 28 2021 at 16:53):

So it is an element of the big algebra, and we know is_primitive_root (zeta') (with the appropriate assumptions).

Eric Rodriguez (Dec 28 2021 at 16:58):

the current zeta has a fair few typeclass issues... I should put this thread in the code; we can rederive some instances so hopefully TC search doesn't do this

Alex J. Best (Dec 28 2021 at 16:58):

Renaming zeta' to zeta and zeta to zeta_unit or something sounds sensible to me, sorry for the original non descriptive name

Chris Birkbeck (Dec 28 2021 at 17:00):

Yeah I agree, the name zeta_unit is a good idea.

Eric Rodriguez (Dec 28 2021 at 17:01):

do people like my new definition in the branch? I think we can get easily that it's in the ring of integers (we can probably make an is_cyclotomic_extension instance for ring_of_integers K for K : is_cyclotomic_extension)

Chris Birkbeck (Dec 28 2021 at 17:04):

I like it being a root of unity. If we can easily make it into an element of the ring of integers, then I think that's fine. Does this fix any of these TC issues?

Riccardo Brasca (Dec 28 2021 at 17:05):

Sorry, which branch?

Chris Birkbeck (Dec 28 2021 at 17:05):

(I haven't really followed the discussion on these TC issues)

Eric Rodriguez (Dec 28 2021 at 17:05):

https://github.com/leanprover-community/flt-regular/commits/zeta_refactor

Eric Rodriguez (Dec 28 2021 at 17:05):

the TC issues aren't really fleshed out, I'm still digging around because it's not really an easy to fix issue

Chris Birkbeck (Dec 28 2021 at 17:06):

Aha I see.

Riccardo Brasca (Dec 28 2021 at 17:07):

Having zeta as a root of unity seems a very good idea!

Riccardo Brasca (Dec 28 2021 at 17:08):

I guess we are not loosing anything, and we can use the existing API for roots of unity

Eric Rodriguez (Dec 31 2021 at 04:50):

I've pushed some more onto that branch, I think it's nearly there. If anyone has any suggestions (either golfing or maths) for the ring_of_integers proof, please let me know. I think it may require fintype S; I don't see how it would, but if helps to consider S as a singleton, I feel like that's fine too

Riccardo Brasca (Dec 31 2021 at 13:50):

I don't have a lot of time today, I will try to have a look during the weekend, but if it compiles feel free to merge into master

Riccardo Brasca (Jan 02 2022 at 16:49):

I will check this tomorrow, sorry for the delay

Eric Rodriguez (Jan 02 2022 at 16:54):

no worries ^^ I've been very busy too so also not had much time to do things

Riccardo Brasca (Jan 03 2022 at 15:10):

@Eric Rodriguez the class ne_zero is now in mathib, right? If there there are no more PR to wait for I think we should first of all start using it everywhere

Riccardo Brasca (Jan 03 2022 at 15:11):

And then refactor zeta

Riccardo Brasca (Jan 03 2022 at 15:15):

Ah, bors failed in #11071 because of some changes in master. @Johan Commelin since it is now fixed, can you merge it? Thank you!

Eric Rodriguez (Jan 03 2022 at 22:00):

ahh, I was already bumping master Riccardo! should've said here, sorry ^^

Riccardo Brasca (Jan 03 2022 at 22:26):

:grinning_face_with_smiling_eyes:

Riccardo Brasca (Jan 03 2022 at 22:27):

No problem! Have you already finished the bump?

Eric Rodriguez (Jan 03 2022 at 22:29):

no, doing some of the leaf files right now

Eric Rodriguez (Jan 03 2022 at 22:29):

give me a couple minutes and I'll push what I have

Riccardo Brasca (Jan 03 2022 at 22:30):

OK, I've fixed src/ready_for_mathlib/cyclotomic/basic.lean and src/ready_for_mathlib/cyclotomic.lean.

Riccardo Brasca (Jan 03 2022 at 22:30):

I've added two simple lemmas in src/ready_for_mathlib/ne_zero.lean. I will PR them later

Eric Rodriguez (Jan 03 2022 at 22:39):

btw, ne_nat exists as (ne_zero.of_ne_zero_coe R).out; a bit of a motuhful, I agree, but that's mathlib naming for ya...

Riccardo Brasca (Jan 03 2022 at 22:41):

So let's throw the whole file away

Eric Rodriguez (Jan 03 2022 at 22:49):

there was actually some other lemmas that I put in therre ^^ sorry for overriding half the stuff, but I merged now

Eric Rodriguez (Jan 03 2022 at 22:50):

I've been trying to use no_zero_smul_divisors a bit more because it seems to be a bit easier to scale than injective algerbra maps (they're equivalent); otherwise we just did pretty much the same

Eric Rodriguez (Jan 03 2022 at 22:50):

I also messed a little with cycl_poly; the last lemma now takes ne_zero and doesn't require 0 < k

Eric Rodriguez (Jan 03 2022 at 22:50):

I'm going to work on the discirminant file now

Eric Rodriguez (Jan 03 2022 at 22:56):

ok, the bump should be done now

Riccardo Brasca (Jan 03 2022 at 23:00):

I also get some timeout in src/number_theory/cyclotomic/cyclotomic_units.lean, but it compiles in the terminal

Riccardo Brasca (Jan 03 2022 at 23:02):

BTW if you want to make it working in VS Code it suffices to increase the time limit

Eric Rodriguez (Jan 03 2022 at 23:07):

yeah, it's so weird... anyways, hopefully that will be gone with the remaster soon so

Eric Rodriguez (Jan 03 2022 at 23:08):

refactor*...

Eric Rodriguez (Jan 04 2022 at 05:56):

ok, zeta_refactors _builds_; I broke a lot of your stuff though, @Alex J. Best ; if you have any free time at some point would be great if you could take a look. The more I think about it I think I used the wrong zeta over in your stuff

Eric Rodriguez (Jan 04 2022 at 05:57):

and so I had to sorry a few previously unsorried things. I'll see if I can think about those things a bit more carefully tomorrow

Eric Rodriguez (Jan 04 2022 at 05:58):

quicklink: https://github.com/leanprover-community/flt-regular/tree/zeta_refactor

Riccardo Brasca (Jan 10 2022 at 13:39):

@Eric Rodriguez what is the situation with your refactor of zeta? I would like to PR the definition and some basic properties

Eric Rodriguez (Jan 10 2022 at 14:42):

still just trying to crack on and deal with some ring of integers stuff, feel free to merge but stuff isn't quite at feature parity yet

Eric Rodriguez (Jan 10 2022 at 22:00):

ohhh, I see what the issue is, and how to get around ir

Eric Rodriguez (Jan 10 2022 at 22:01):

essentially, I wanted to define is_cyclotomic_extension (O K) (O L) for is_cyclotomic_extension K L, but this doesn't work

Eric Rodriguez (Jan 10 2022 at 22:01):

we instead have is_cyclotomic_extension (O K) (cyclotomic_ring blah O K), and it is a theorem of Q that cyclotomic_ring O K is O L

Eric Rodriguez (Jan 10 2022 at 22:02):

which is what you're proving right now riccardo

Eric Rodriguez (Jan 10 2022 at 22:02):

so i'm just going to try to get the current stuff building somehow and then work from there

Riccardo Brasca (Jan 10 2022 at 22:11):

Yes, currently the definition of cyclotomic_ring is the ring obtained adjoining the roots of the cyclotomic polynomials. In particular the proof that it is a cyclotomic extension should be easy (maybe it's even already there). The difficult part is that in the case of Q it is also the integral closure of Z.

Riccardo Brasca (Jan 10 2022 at 22:19):

If your new definition works don't hesitate to merge into master!

Riccardo Brasca (Jan 10 2022 at 22:19):

Don't worry if you add some more sorry

Riccardo Brasca (Jan 11 2022 at 15:57):

I've merged master in zeta_refactor

Riccardo Brasca (Jan 11 2022 at 16:00):

And I am trying to fix the errors

Riccardo Brasca (Jan 11 2022 at 16:30):

@Eric Rodriguez It now compiles (I just had to add some sorry, we will fix them sooner or later). I think having zeta instead of zeta' is better. If you are satisfied with the definition you can merge into master.

Riccardo Brasca (Jan 11 2022 at 16:31):

We are now quite close to the computation of the ring of integers of the cyclotomic extension of the rationals, that is already a non trivial result, so I would like to PR all the stuff leading to it quite soon.

Eric Rodriguez (Jan 11 2022 at 17:07):

sure, argh sorry didn't want to break people's stuff but will merge then

Eric Rodriguez (Jan 11 2022 at 17:16):

oki, done, i'll now add docstrings and things will build again

Last updated: Dec 20 2023 at 11:08 UTC