zeta and primitive roots

Stream: FLT-regular

[Riccardo Brasca]

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]

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

[Eric Rodriguez]

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]

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

[Yaël Dillies]

Ah I see!

[Riccardo Brasca]

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

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

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

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]

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

[Eric Rodriguez]

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]

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

[Yaël Dillies]

Ah I see!

[Riccardo Brasca]

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

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

(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'!)