Zulip Chat Archive
Stream: FLT-regular
Topic: zeta PR
Riccardo Brasca (Jan 27 2022 at 12:51):
I've opened #11695 with the definition of zeta. I've added @Alex J. Best and @Eric Rodriguez as authors of the file, so you may want to have a look at it.
Eric Rodriguez (Jan 27 2022 at 13:01):
let me see if I can toy with ne_zero so we can stop writing this ((n:nat):B) stuff and we can just write (n:B)
Chris Birkbeck (Feb 08 2022 at 19:33):
If K is a cyclotomic_field p β and R is π (cyclotomic_field p β). Is there a way to link zeta p β€ R and zeta β K? I wanted to say that when I coerce the first into K it becomes the second, but since they are defined by some then I guess this isn't true. How do we deal with cases when we need to use both? Or do we just try and avoid these cases?
Eric Rodriguez (Feb 08 2022 at 19:49):
aaah this is not fun, you raise a good point
Eric Rodriguez (Feb 08 2022 at 19:50):
I think this really hammers home what Riccardo was saying about proving things about primitive roots as much as possible
Eric Rodriguez (Feb 08 2022 at 19:51):
and only specialize to ΞΆ when needed
Chris Birkbeck (Feb 08 2022 at 19:54):
Yeah, the reason I'm running into this is that I want to use the Galois action on zeta and some of the results we have are currently stated for zeta β K. So I guess we could either define the induced Galois action on the units or sort out some coes into fields.
Riccardo Brasca (Feb 08 2022 at 20:05):
Yes, we need to prove stuff for any primitive root. In practice we already have is_zeta aka is_primitive_root. We should use it as much as possible
Eric Rodriguez (Feb 08 2022 at 20:32):
BTW, there's already docs#polynomial.gal.gal_action_hom,so that may be useful as a bssus for the mkre general gal stuff @Chris Birkbeck
Kevin Buzzard (Feb 09 2022 at 07:02):
Kenny Lau in his perfectoid talk last Thurs reminded me of the idea that instead of taking a ring of integers one can instead have an is_ring_of_integers predicate on rings equipped with a map to the field
Johan Commelin (Feb 09 2022 at 07:05):
I'm quite sure it's good to have such a predicate
Johan Commelin (Feb 09 2022 at 07:06):
After all, β€ is not ring_of_integers β, and we want that example to work smoothly.
Kevin Buzzard (Feb 09 2022 at 07:07):
And then you can ask for a zeta-compatible one maybe? What is this zeta? A classical.some?
Riccardo Brasca (Feb 09 2022 at 08:12):
We have docs#is_integral_closure
Riccardo Brasca (Feb 09 2022 at 08:12):
And I am already using it
Eric Rodriguez (Feb 09 2022 at 20:05):
I've done the required mathlib-side PR as #11941!
Riccardo Brasca (Jan 27 2022 at 12:51):
I've opened #11695 with the definition of zeta. I've added @Alex J. Best and @Eric Rodriguez as authors of the file, so you may want to have a look at it.
Eric Rodriguez (Jan 27 2022 at 13:01):
let me see if I can toy with ne_zero so we can stop writing this ((n:nat):B) stuff and we can just write (n:B)
Chris Birkbeck (Feb 08 2022 at 19:33):
If K is a cyclotomic_field p β and R is π (cyclotomic_field p β). Is there a way to link zeta p β€ R and zeta β K? I wanted to say that when I coerce the first into K it becomes the second, but since they are defined by some then I guess this isn't true. How do we deal with cases when we need to use both? Or do we just try and avoid these cases?
Eric Rodriguez (Feb 08 2022 at 19:49):
aaah this is not fun, you raise a good point
Eric Rodriguez (Feb 08 2022 at 19:50):
I think this really hammers home what Riccardo was saying about proving things about primitive roots as much as possible
Eric Rodriguez (Feb 08 2022 at 19:51):
and only specialize to ΞΆ when needed
Chris Birkbeck (Feb 08 2022 at 19:54):
Yeah, the reason I'm running into this is that I want to use the Galois action on zeta and some of the results we have are currently stated for zeta β K. So I guess we could either define the induced Galois action on the units or sort out some coes into fields.
Riccardo Brasca (Feb 08 2022 at 20:05):
Yes, we need to prove stuff for any primitive root. In practice we already have is_zeta aka is_primitive_root. We should use it as much as possible
Eric Rodriguez (Feb 08 2022 at 20:32):
BTW, there's already docs#polynomial.gal.gal_action_hom,so that may be useful as a bssus for the mkre general gal stuff @Chris Birkbeck
Kevin Buzzard (Feb 09 2022 at 07:02):
Kenny Lau in his perfectoid talk last Thurs reminded me of the idea that instead of taking a ring of integers one can instead have an is_ring_of_integers predicate on rings equipped with a map to the field
Johan Commelin (Feb 09 2022 at 07:05):
I'm quite sure it's good to have such a predicate
Johan Commelin (Feb 09 2022 at 07:06):
After all, β€ is not ring_of_integers β, and we want that example to work smoothly.
Kevin Buzzard (Feb 09 2022 at 07:07):
And then you can ask for a zeta-compatible one maybe? What is this zeta? A classical.some?
Riccardo Brasca (Feb 09 2022 at 08:12):
We have docs#is_integral_closure
Riccardo Brasca (Feb 09 2022 at 08:12):
And I am already using it
Eric Rodriguez (Feb 09 2022 at 20:05):
I've done the required mathlib-side PR as #11941!
Last updated: Dec 20 2023 at 11:08 UTC