## Stream: FLT-regular

### Topic: ne_zero again

#### Riccardo Brasca (May 09 2022 at 10:17):

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 (May 09 2022 at 10:31):

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

#### Riccardo Brasca (May 09 2022 at 10:33):

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

#### Michael Stoll (May 21 2022 at 18:38):

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.

I totally agree

#### Eric Rodriguez (May 21 2022 at 19:27):

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 (May 21 2022 at 19:28):

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 (May 26 2022 at 12:09):

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 (May 26 2022 at 12:09):

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

#### Riccardo Brasca (May 29 2022 at 10:58):

#14446 For more cleanup

#### Riccardo Brasca (May 29 2022 at 12:09):

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 (May 29 2022 at 12:10):

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 (May 29 2022 at 12:12):

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 (May 29 2022 at 12:55):

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 (May 29 2022 at 13:12):

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

#### Riccardo Brasca (May 29 2022 at 13:14):

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

#### Kevin Buzzard (May 29 2022 at 13:57):

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 (May 29 2022 at 14:34):

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

#### Riccardo Brasca (May 30 2022 at 14:04):

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

#### Riccardo Brasca (May 30 2022 at 16:02):

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

#### Riccardo Brasca (May 30 2022 at 17:18):

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

#### Riccardo Brasca (Jun 20 2022 at 07:51):

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 (May 09 2022 at 10:17):

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 (May 09 2022 at 10:31):

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

#### Riccardo Brasca (May 09 2022 at 10:33):

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

#### Michael Stoll (May 21 2022 at 18:38):

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.

I totally agree

#### Eric Rodriguez (May 21 2022 at 19:27):

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 (May 21 2022 at 19:28):

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 (May 26 2022 at 12:09):

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 (May 26 2022 at 12:09):

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

#### Riccardo Brasca (May 29 2022 at 10:58):

#14446 For more cleanup

#### Riccardo Brasca (May 29 2022 at 12:09):

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 (May 29 2022 at 12:10):

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 (May 29 2022 at 12:12):

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 (May 29 2022 at 12:55):

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 (May 29 2022 at 13:12):

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

#### Riccardo Brasca (May 29 2022 at 13:14):

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

#### Kevin Buzzard (May 29 2022 at 13:57):

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 (May 29 2022 at 14:34):

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

#### Riccardo Brasca (May 30 2022 at 14:04):

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

#### Riccardo Brasca (May 30 2022 at 16:02):

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

#### Riccardo Brasca (May 30 2022 at 17:18):

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

#### Riccardo Brasca (Jun 20 2022 at 07:51):

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.

Last updated: Dec 20 2023 at 11:08 UTC