ne_zero again

Stream: FLT-regular

[Riccardo Brasca]

Is ne_zero ((n : ℕ) : K) really needed in docs#cyclotomic_field.is_cyclotomic_extension? I am maybe confused, but let p the characteristic of K. If p = 0 or p does not divide n, then there are no problems (since ne_zero ((n : ℕ) : K) holds). Otherwise, write n=p^k * m with ¬p ∣ m. We need to prove adjoin_roots in the definition of docs#is_cyclotomic_extension. Now, x^n = 1 if and only if x^m = 1 (since the Frobenius is injective), and the roots of cyclotomic n K are the m-th primitive roots of unity by docs#polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p.

Does someone see a problem in this proof? I don't have the time to formalize it today since I have to prepare a talk, but I will try to do it this week. (I would like to have an opinion since if it holds I will remove the assumption in my talk).

[Alex J. Best]

I think this works, just nobody got round to this? At least that's my vague recollection from before

[Riccardo Brasca]

I've the same feeling. I will try to remove as much ne_zero assumptions as possible.

[Michael Stoll]

The way cylcotomic_field and is_cyclotomic_extension are defined, the condition is unnecessary (adjoining p-power roots of unity in characteristic p gives a trivial extension). The condition is needed, e.g., if you want to show that there are exactly n nth roots of unity; basically, you'll need at as soon as you want to work with cyclotomic fields in a meaningful way.

[Riccardo Brasca]

I totally agree

[Eric Rodriguez]

it's not quite that simple, the 15th cyclotomic extension in char3 is the 5th cyclotomic extension I think is the really obvious example

[Eric Rodriguez]

so I think it allows a lot of uniformity and also this is covered by the (very large) family of theorems like docs#polynomial.is_root_cyclotomic_iff

[Riccardo Brasca]

I've finally found some time to remove the unneeded ne_zero in #14392. I guess there are more instances of this, I will see.

[Riccardo Brasca]

@Alex J. Best You linter can check useless haveI/letI?

[Riccardo Brasca]

#14446 For more cleanup

[Riccardo Brasca]

I am wondering whether it is worth to refactor the definition of is_cyclotomic_extension as follows

@[mk_iff] class is_cyclotomic_extension : Prop :=
(exists_root {a : ℕ+} (ha : a ∈ S) : ∃ r : B, is_primitive_root r a )
(adjoin_roots : ∀ (x : B), x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })

[Riccardo Brasca]

The difference is that we require the existence of a primitive root rather than a root of the cyclotomic polynomial. In such a way, almost all the ne_zero should disappear (we will need ne_zero to construct a cyclotomic extension, and only there)

[Riccardo Brasca]

With this new definition it's impossible to have a p-th cyclotomic extension of $\mathbb{F}_p$, but this is the only drawback.

[Kevin Buzzard]

I'm not sure that a number theorist would be able to give a coherent answer if you asked them what they thought the pth cyclotomic extension of Fp was supposed to be

[Eric Rodriguez]

does this definition still work for ℤₚ? this is the only thing I find mentioned in the original thread that is relevant, I think

[Eric Rodriguez]

(I don't know much about p-adics...)

[Riccardo Brasca]

Yes, it is equivalent to the current one plus ne_zero, so in particular it is the same for characteristic 0 rings.

[Kevin Buzzard]

I have only ever heard the concept of cyclotomic extension being applied to p-adic fields and number fields, so I don't think this is a huge loss at all.

[Xavier Roblot]

I agree with Kevin. The important point is that it still works for p-adic fields (and of course number fields).

[Riccardo Brasca]

OK, I will go for the refactor. It should solve once and for all the various ne_zero annoyances.

[Riccardo Brasca]

I started the refactor at #14463. It is still WIP, but number_theory.cyclotomic.basic is done.

[Riccardo Brasca]

It's ready for review. It was much easier than I thought, and the proof are really much less painful.

[Riccardo Brasca]

Now that #14463 is merged, a lot of uses ofne_zero are gone. I think it can also be removed from docs#cyclotomic_ring.cyclotomic_field.is_fraction_ring, but that's not so important.

[Riccardo Brasca]

Is ne_zero ((n : ℕ) : K) really needed in docs#cyclotomic_field.is_cyclotomic_extension? I am maybe confused, but let p the characteristic of K. If p = 0 or p does not divide n, then there are no problems (since ne_zero ((n : ℕ) : K) holds). Otherwise, write n=p^k * m with ¬p ∣ m. We need to prove adjoin_roots in the definition of docs#is_cyclotomic_extension. Now, x^n = 1 if and only if x^m = 1 (since the Frobenius is injective), and the roots of cyclotomic n K are the m-th primitive roots of unity by docs#polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p.

Does someone see a problem in this proof? I don't have the time to formalize it today since I have to prepare a talk, but I will try to do it this week. (I would like to have an opinion since if it holds I will remove the assumption in my talk).

[Alex J. Best]

I think this works, just nobody got round to this? At least that's my vague recollection from before

[Riccardo Brasca]

I've the same feeling. I will try to remove as much ne_zero assumptions as possible.

[Michael Stoll]

The way cylcotomic_field and is_cyclotomic_extension are defined, the condition is unnecessary (adjoining p-power roots of unity in characteristic p gives a trivial extension). The condition is needed, e.g., if you want to show that there are exactly n nth roots of unity; basically, you'll need it as soon as you want to work with cyclotomic fields in a meaningful way.

[Riccardo Brasca]

I totally agree

[Eric Rodriguez]

it's not quite that simple, the 15th cyclotomic extension in char3 is the 5th cyclotomic extension I think is the really obvious example

[Eric Rodriguez]

so I think it allows a lot of uniformity and also this is covered by the (very large) family of theorems like docs#polynomial.is_root_cyclotomic_iff

[Riccardo Brasca]

I've finally found some time to remove the unneeded ne_zero in #14392. I guess there are more instances of this, I will see.

[Riccardo Brasca]

@Alex J. Best You linter can check useless haveI/letI?

[Riccardo Brasca]

#14446 For more cleanup

[Riccardo Brasca]

I am wondering whether it is worth to refactor the definition of is_cyclotomic_extension as follows

@[mk_iff] class is_cyclotomic_extension : Prop :=
(exists_root {a : ℕ+} (ha : a ∈ S) : ∃ r : B, is_primitive_root r a )
(adjoin_roots : ∀ (x : B), x ∈ adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 })

[Riccardo Brasca]

The difference is that we require the existence of a primitive root rather than a root of the cyclotomic polynomial. In such a way, almost all the ne_zero should disappear (we will need ne_zero to construct a cyclotomic extension, and only there)

[Riccardo Brasca]

With this new definition it's impossible to have a p-th cyclotomic extension of $\mathbb{F}_p$, but this is the only drawback.

[Kevin Buzzard]

I'm not sure that a number theorist would be able to give a coherent answer if you asked them what they thought the pth cyclotomic extension of Fp was supposed to be

[Eric Rodriguez]

does this definition still work for ℤₚ? this is the only thing I find mentioned in the original thread that is relevant, I think

[Eric Rodriguez]

(I don't know much about p-adics...)

[Riccardo Brasca]

Yes, it is equivalent to the current one plus ne_zero, so in particular it is the same for characteristic 0 rings.

[Kevin Buzzard]

I have only ever heard the concept of cyclotomic extension being applied to p-adic fields and number fields, so I don't think this is a huge loss at all.

[Xavier Roblot]

I agree with Kevin. The important point is that it still works for p-adic fields (and of course number fields).

[Riccardo Brasca]

OK, I will go for the refactor. It should solve once and for all the various ne_zero annoyances.

[Riccardo Brasca]

I started the refactor at #14463. It is still WIP, but number_theory.cyclotomic.basic is done.

[Riccardo Brasca]

It's ready for review. It was much easier than I thought, and the proof are really much less painful.

[Riccardo Brasca]

Now that #14463 is merged, a lot of uses ofne_zero are gone. I think it can also be removed from docs#cyclotomic_ring.cyclotomic_field.is_fraction_ring, but that's not so important.