Stream: FLT-regular

Topic: zeta and primitive roots

Riccardo Brasca (Feb 03 2022 at 17:23):

I've just realized that theorem like docs#is_cyclotomic_extension.norm_zeta_sub_one_eq_eval_cyclotomic are not good enough. It is stated for zeta, but of course it works for any primitive root of unity, for the very good reason that zeta is any such a root. But in Lean this choice is done once and for all, so it's not exactly the same.

Having zeta is in any case useful when we want to pick one root, but we should prove the results in general and then specialize to zeta (essentially the same proof should work). Just another annoying aspect of formalization :grinning:

Yaël Dillies (Feb 03 2022 at 17:24):

Same deal as between docs#localization and docs#is_localization, I assume?

Eric Rodriguez (Feb 03 2022 at 17:26):

yes, I realised this for a couple of results -- note that the original Galois group aut is about primitive roots, and even the fact that 1 - ζ^k is associated to 1 - ζ^n. It does make the results a lot easier to use, especially when you need to juggle the 50 different versions of ζ (half of the Galois proof is juggling whether I want just the normal ζ, or the root-of-unity coe because you can do group things in there...)

Riccardo Brasca (Feb 03 2022 at 17:27):

@Yaël Dillies Not exactly, here zeta is an element produced by classical.some, so in some sense things are less serious. The only problem is that for a mathematician classical.some means "for all x such that", but Lean choose one element once and for all.

Ah I see!

Riccardo Brasca (Feb 03 2022 at 17:36):

@Eric Rodriguez Maybe we can avoid to multiply the efforts using you Galois stuff: for example I want to prove that norm K (ζ - 1) = p, and we already know this for ζ = zeta. Know, ζ - 1 and zeta - 1 are Galois conjugate by what you proved, and the norm of conjugates elements is the same (something not difficult and worth to have in any case). We can probably do the same for all the results we need.

Riccardo Brasca (Feb 03 2022 at 17:40):

(Speaking of classical.some, the fact that the axiom of choice means that the choice is done once and for all, "at the platonic level", is something that really blows my mind and makes me suspicious about it, much more than Banach-Tarski.)

Riccardo Brasca (Feb 03 2022 at 17:42):

(Look at docs#function.extend, it's crazy we can reason about extend f g e' for a non injective f. I mean, there is one and only one extend f g e'!)

Riccardo Brasca (Feb 03 2022 at 17:23):

I've just realized that theorem like docs#is_cyclotomic_extension.norm_zeta_sub_one_eq_eval_cyclotomic are not good enough. It is stated for zeta, but of course it works for any primitive root of unity, for the very good reason that zeta is any such a root. But in Lean this choice is done once and for all, so it's not exactly the same.

Having zeta is in any case useful when we want to pick one root, but we should prove the results in general and then specialize to zeta (essentially the same proof should work). Just another annoying aspect of formalization :grinning:

Yaël Dillies (Feb 03 2022 at 17:24):

Same deal as between docs#localization and docs#is_localization, I assume?

Eric Rodriguez (Feb 03 2022 at 17:26):

yes, I realised this for a couple of results -- note that the original Galois group aut is about primitive roots, and even the fact that 1 - ζ^k is associated to 1 - ζ^n. It does make the results a lot easier to use, especially when you need to juggle the 50 different versions of ζ (half of the Galois proof is juggling whether I want just the normal ζ, or the root-of-unity coe because you can do group things in there...)

Riccardo Brasca (Feb 03 2022 at 17:27):

@Yaël Dillies Not exactly, here zeta is an element produced by classical.some, so in some sense things are less serious. The only problem is that for a mathematician classical.some means "for all x such that", but Lean choose one element once and for all.

Ah I see!

Riccardo Brasca (Feb 03 2022 at 17:36):

@Eric Rodriguez Maybe we can avoid to multiply the efforts using you Galois stuff: for example I want to prove that norm K (ζ - 1) = p, and we already know this for ζ = zeta. Know, ζ - 1 and zeta - 1 are Galois conjugate by what you proved, and the norm of conjugates elements is the same (something not difficult and worth to have in any case). We can probably do the same for all the results we need.

Riccardo Brasca (Feb 03 2022 at 17:40):

(Speaking of classical.some, the fact that the axiom of choice means that the choice is done once and for all, "at the platonic level", is something that really blows my mind and makes me suspicious about it, much more than Banach-Tarski.)

Riccardo Brasca (Feb 03 2022 at 17:42):

(Look at docs#function.extend, it's crazy we can reason about extend f g e' for a non injective f. I mean, there is one and only one extend f g e'!)

Last updated: Dec 20 2023 at 11:08 UTC