# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Unit lemma

#### Chris Birkbeck (Nov 05 2021 at 19:09):

Ok so I split this lemma off from the `rat.lean`

file since it was causing excessive RAM usage. I made some simple "coe lemmas" to at least deal with the annoying bits in the proof. But its now at the stage where we need to know what the roots of unity in a cyclotomic field are `roots_of_unity_in_cyclo`

and some related results (e.g. `unit_inv_conj_not_neg_zeta`

) which seem annoying.

#### Chris Birkbeck (Nov 05 2021 at 19:11):

At some point we will probably have to do proofs which involve writing an element in the power basis and then proving something about its coefficients, so there might not be much escape from the annoyingness.

#### Riccardo Brasca (Nov 05 2021 at 20:47):

Chris Birkbeck said:

Ok so I split this lemma off from the

`rat.lean`

file since it was causing excessive RAM usage. I made some simple "coe lemmas" to at least deal with the annoying bits in the proof. But its now at the stage where we need to know what the roots of unity in a cyclotomic field are`roots_of_unity_in_cyclo`

and some related results (e.g.`unit_inv_conj_not_neg_zeta`

) which seem annoying.

We know that all the roots of unity are there, don't we?

#### Chris Birkbeck (Nov 05 2021 at 20:48):

Do we know there aren't any more?

#### Kevin Buzzard (Nov 05 2021 at 20:49):

if n is odd then mu_{2n} is in Q(zeta_n)

#### Chris Birkbeck (Nov 05 2021 at 20:50):

Yeah, it's checking that other than that there aren't any more.

#### Riccardo Brasca (Nov 05 2021 at 20:52):

Ah, that's more delicate, I agree

#### Chris Birkbeck (Nov 05 2021 at 21:07):

The easiest way is probably to argue via the degree of the field extension. But I've not searched enough of mathlib to check if all the required tools are there for this.

#### Kevin Buzzard (Nov 05 2021 at 21:11):

Your idea is that if mu_d and mu_e are in K then so is mu_{lcm(d,e)}, and then some lemma that says that if phi(an)<=phi(n) and a>0 then either a=1 or n is odd and a=2.

#### Chris Birkbeck (Nov 05 2021 at 21:15):

Yep that was the plan. Although I don't know how much about phi we have.

#### Kevin Buzzard (Nov 05 2021 at 21:44):

I claim phi is "super-multiplicative": phi(ab)>=phi(a)phi(b). Given this, we must have phi(a)=1 and I'm guessing it's not hard to go from this to a<=2 (I'm working always with positive naturals here, nothing makes sense for 0) and then one can prove that phi(2n)=phi(n) iff n is odd.

#### Kevin Buzzard (Nov 05 2021 at 21:45):

this looks like a not-too-bad route through

#### Chris Birkbeck (Feb 04 2022 at 09:42):

Ok so I'm back looking at this, I noticed that I sort of abandoned the Unit_Lemmas file, so I'm going to work on that.

#### Chris Birkbeck (Feb 11 2022 at 13:18):

Ok so the proofs of this are working again. For the moment I just did something simple and turned `zeta p ℚ (cyclotomic_field p ℚ)`

into a unit in the ring of integers, that way it coerces "back up" how one expects.

#### Chris Birkbeck (Nov 05 2021 at 19:09):

Ok so I split this lemma off from the `rat.lean`

file since it was causing excessive RAM usage. I made some simple "coe lemmas" to at least deal with the annoying bits in the proof. But its now at the stage where we need to know what the roots of unity in a cyclotomic field are `roots_of_unity_in_cyclo`

and some related results (e.g. `unit_inv_conj_not_neg_zeta`

) which seem annoying.

#### Chris Birkbeck (Nov 05 2021 at 19:11):

At some point we will probably have to do proofs which involve writing an element in the power basis and then proving something about its coefficients, so there might not be much escape from the annoyingness.

#### Riccardo Brasca (Nov 05 2021 at 20:47):

Chris Birkbeck said:

`rat.lean`

file since it was causing excessive RAM usage. I made some simple "coe lemmas" to at least deal with the annoying bits in the proof. But its now at the stage where we need to know what the roots of unity in a cyclotomic field are`roots_of_unity_in_cyclo`

and some related results (e.g.`unit_inv_conj_not_neg_zeta`

) which seem annoying.

We know that all the roots of unity are there, don't we?

#### Chris Birkbeck (Nov 05 2021 at 20:48):

Do we know there aren't any more?

#### Kevin Buzzard (Nov 05 2021 at 20:49):

if n is odd then mu_{2n} is in Q(zeta_n)

#### Chris Birkbeck (Nov 05 2021 at 20:50):

Yeah, it's checking that other than that there aren't any more.

#### Riccardo Brasca (Nov 05 2021 at 20:52):

Ah, that's more delicate, I agree

#### Chris Birkbeck (Nov 05 2021 at 21:07):

The easiest way is probably to argue via the degree of the field extension. But I've not searched enough of mathlib to check if all the required tools are there for this.

#### Kevin Buzzard (Nov 05 2021 at 21:11):

Your idea is that if mu_d and mu_e are in K then so is mu_{lcm(d,e)}, and then some lemma that says that if phi(an)<=phi(n) and a>0 then either a=1 or n is odd and a=2.

#### Chris Birkbeck (Nov 05 2021 at 21:15):

Yep that was the plan. Although I don't know how much about phi we have.

#### Kevin Buzzard (Nov 05 2021 at 21:44):

I claim phi is "super-multiplicative": phi(ab)>=phi(a)phi(b). Given this, we must have phi(a)=1 and I'm guessing it's not hard to go from this to a<=2 (I'm working always with positive naturals here, nothing makes sense for 0) and then one can prove that phi(2n)=phi(n) iff n is odd.

#### Kevin Buzzard (Nov 05 2021 at 21:45):

this looks like a not-too-bad route through

#### Chris Birkbeck (Feb 04 2022 at 09:42):

Ok so I'm back looking at this, I noticed that I sort of abandoned the Unit_Lemmas file, so I'm going to work on that.

#### Chris Birkbeck (Feb 11 2022 at 13:18):

Ok so the proofs of this are working again. For the moment I just did something simple and turned `zeta p ℚ (cyclotomic_field p ℚ)`

into a unit in the ring of integers, that way it coerces "back up" how one expects.

Last updated: Dec 20 2023 at 11:08 UTC