# Zulip Chat Archive

## 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`

`n`

th roots of unity; basically, you'll need at as soon as you want to work with cyclotomic fields in a meaningful way.

#### Riccardo Brasca (May 21 2022 at 18:54):

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

#### Eric Rodriguez (May 29 2022 at 13:12):

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

#### 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 of`ne_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`

`n`

th roots of unity; basically, you'll need it as soon as you want to work with cyclotomic fields in a meaningful way.

#### Riccardo Brasca (May 21 2022 at 18:54):

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

#### Eric Rodriguez (May 29 2022 at 13:12):

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

#### 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 of`ne_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