Unit lemma

Stream: FLT-regular

[Chris Birkbeck]

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]

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]

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]

Do we know there aren't any more?

[Kevin Buzzard]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

Ah, that's more delicate, I agree

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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]

this looks like a not-too-bad route through

[Chris Birkbeck]

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]

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]

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]

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]

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]

Do we know there aren't any more?

[Kevin Buzzard]

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

[Chris Birkbeck]

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

[Riccardo Brasca]

Ah, that's more delicate, I agree

[Chris Birkbeck]

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]

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]

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

[Kevin Buzzard]

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]

this looks like a not-too-bad route through

[Chris Birkbeck]

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]

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.