Zulip Chat Archive

Stream: FLT-regular

Topic: Cyclotomic units


Riccardo Brasca (Oct 28 2021 at 14:30):

We currently have

variables [field L] [algebra K L] [is_cyclotomic_extension {n} K L]

include K n
def zeta' : L :=
classical.some (exists_root_of_splits (algebra_map K L) (is_splitting_field.splits _ _)
  (degree_cyclotomic_pos n K n.pos).ne.symm)

Before working on the various sorry, we need to generalize the defintion to A B....

Riccardo Brasca (Oct 28 2021 at 15:22):

I've started doing this in branch cycl_units_ring (I just wrote the new def). If someone wants to write some code I won't work on this until tomorrow morning.

Filippo A. E. Nuccio (Oct 28 2021 at 16:54):

I just have a side-remark: do you really want to call them "cyclotomic units"? They are roots of unit, rather, I think. The cyclotomic units are normally meant to be the elements in the subgroup generated by the ratios

ζpn1ζpna1\frac{\zeta_{p^n}-1}{\zeta_{p^n}^a-1}

for varying aa (the definition when the order is not a power of pp is slightly different), see
https://en.wikipedia.org/wiki/Cyclotomic_unit
Or am I misunderstainding your code?

Alex J. Best (Oct 28 2021 at 16:55):

That's what https://github.com/leanprover-community/flt-regular/blob/master/src/number_theory/cyclotomic/cyclotomic_units.lean#L191 is meant to become eventually, except currently nothing is proved.

Alex J. Best (Oct 28 2021 at 16:56):

So the filename refers to that def rather than the zeta itself

Filippo A. E. Nuccio (Oct 28 2021 at 17:02):

I see; so it is the (finite) sets of all things of the form

(r,n)=1,r<n)ζnr?\sum_{(r,n)=1, r<n)}\zeta_n^r ?

Or am I misreading the definition of aux?

Alex J. Best (Oct 28 2021 at 17:03):

Yes aux is a hacky way to define the inverse mod n, probably its best to replace it with an actual inverse in zmod n but I was just hacking around.

Alex J. Best (Oct 28 2021 at 17:04):

The idea of using the finite sums rather than the quotient is just to stay in the ring of integers and not worry about division

Filippo A. E. Nuccio (Oct 28 2021 at 17:06):

OK; because I am still slightly sceptical about this definition. Normally the "cyclotomic units" are an infinite group generated by some explicitely-defined things of that sort (they are of finite index...).

Filippo A. E. Nuccio (Oct 28 2021 at 17:08):

I would rather use the definition given in Theorem 8.3 of Washington's book Introduction to Cyclotomic Fields

Alex J. Best (Oct 28 2021 at 17:10):

Maybe basic_cyclotomic_unit is a better name? The point is just to define these generators yes.

Filippo A. E. Nuccio (Oct 28 2021 at 17:11):

Sounds much better! Just because otherwise there would be "usual" cyclotomic units which would not be mathlib ones.

Alex J. Best (Oct 28 2021 at 17:13):

I think for the purpose of this file I was (implicitly) assuming that the n was prime in what I was doing also, so I definitely didn't try and formulate the right general definition yet.

Riccardo Brasca (Oct 28 2021 at 17:18):

We can define it as a subgroup of the group of units, like primitive roots

Riccardo Brasca (Oct 28 2021 at 17:20):

And I really suggest we make the effort to give the most general definition

Riccardo Brasca (Oct 28 2021 at 17:21):

No problem in adding assumptions in theorems of course

Filippo A. E. Nuccio (Oct 28 2021 at 17:21):

Ok, so I would rather suggest to follow Washington's approach for general nn, personally.

Riccardo Brasca (Oct 29 2021 at 12:01):

zeta' and zeta are now defined for rings (mathematically they are the same thing, a primitive root of unity). @Chris Birkbeck do you think we really need the subgroup of cyclotomic units or for us it's enough to work with some specific element?

Chris Birkbeck (Oct 29 2021 at 12:05):

Well I don't think we need the whole subgroup (but I could be wrong). I think its enough to know that they are units.

Riccardo Brasca (Oct 29 2021 at 14:05):

OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is enough for us, right? We don't need ζpr\zeta_{p^r} I think

Riccardo Brasca (Oct 29 2021 at 14:06):

And even less ζn\zeta_n

Chris Birkbeck (Oct 29 2021 at 14:06):

Riccardo Brasca said:

OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is enough for us, right? We don't need ζpr\zeta_{p^r} I think

Yes that is enough

Riccardo Brasca (Oct 29 2021 at 14:37):

Unfortunately this does not seem to really simplify the problem compared to ζpr\zeta_{p^r}.

I am not sure what is the best approach here. In my opinion we should concentrate on proving this (I mean the description of the ring of integers), and go back to FLT once we have this.

Chris Birkbeck (Oct 29 2021 at 14:41):

Yes this is the first big hurdle, I guess we just need to make sure that if we prove this without using, say, embeddings, then we can do the same for the FLT. Otherwise we may end up having to do more work than needed.

Chris Birkbeck (Oct 29 2021 at 14:45):

Riccardo Brasca said:

Unfortunately this does not seem to really simplify the problem compared to ζpr\zeta_{p^r}.

I am not sure what is the best approach here. In my opinion we should concentrate on proving this (I mean the description of the ring of integers), and go back to FLT once we have this.

I think ζn\zeta_n it is actually more annoying, but pp vs prp^r is probably about the same.

Riccardo Brasca (Oct 29 2021 at 15:02):

The question is if we want to prove the final theorem as fast as possible or do we prefer doing things following mathlib style.

For example for the discriminant, I am quite sure it should be defined in general, without embeddings. A lot of elementary results are true for algebras that are finite and free over the base (for example what happens when you multiply the family by a matrix). Using embeddings from the start can make our life easier, but I think it's not the "right" way. I know, perfect is the enemy of good, and we have to make some compromise, but maybe not immediately.

Note that a good thing about OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is that this is a precise statement (it is already in the repo), so if someone prefers working on FLT he can do it immediately, a sorried lemma is as as good as a proved lemma. My suggestion is that we concentrate on this fact, but we can very well work on the two subprojects at the same time.

Riccardo Brasca (Oct 29 2021 at 15:03):

What we really have to do, in any case, is producing a lot of small sorried lemmas, and people will start proving them, even if they are not really interested in the whole project.

Chris Birkbeck (Oct 29 2021 at 15:06):

Ah sure I see what you mean about the discriminant. I was thinking only of the definition for number fields. But yes we may as well define them very generally. Using that we can probably give some enough sorried lemmas to get the ring of integers theorem going.

Riccardo Brasca (Oct 29 2021 at 15:14):

instance : is_integral_closure (cyclotomic_ring n  )  (cyclotomic_field n ) := sorry

is already there, in number_theory/cyclotomic/rat, so if someone needs it there are no problems.

Chris Birkbeck (Oct 29 2021 at 15:21):

Sorry I guess I meant get the proof going.

Chris Birkbeck (Oct 29 2021 at 15:23):

Riccardo Brasca said:

What we really have to do, in any case, is producing a lot of small sorried lemmas, and people will start proving them, even if they are not really interested in the whole project.

But should we do this first for the proof of the ring of integers or start from flt_regular and go down?

Riccardo Brasca (Oct 29 2021 at 15:26):

Well, this is exactly my question :smile:

Riccardo Brasca (Oct 29 2021 at 15:26):

We can do both ways of course

Chris Birkbeck (Oct 29 2021 at 15:26):

Riccardo Brasca said:

Well, this is exactly my question :smile:

Haha ok I see :)

Chris Birkbeck (Oct 29 2021 at 15:28):

Well I'd be partial to starting from flt_regular and going down. I was thinking about this, but then was scratching my head about how to do "An algebraic integer all of whose conjugates have absolute value one is a root of unity"

Riccardo Brasca (Oct 29 2021 at 15:28):

I personally suggest we concentrate on proving the instance, that means to develop a good theory of the discriminant (I've just pushed number_theory/discriminant/basic containing a definition). But if someone prefers working on the other part of the project there are no problem in using a sorried instance like that (since it is a proposition).

Chris Birkbeck (Oct 29 2021 at 15:31):

Oh well then I'm happy to do that. I have no real intuition as to what is best and since you've been doing this for longer I'm happy to follow your suggestion :)

Alex J. Best (Oct 29 2021 at 16:02):

It definitely seems some of the top-down steps can be done independently, thats what I've been idly thinking about with the may_assume tactic I was working on, how to make the outline of the proof quite readable.

Riccardo Brasca (Nov 02 2021 at 23:29):

@Alex J. Best Just for fun I've slightly golfed your submodule.span_singleton_eq_span_singleton. It is surprisingly annoying!

Alex J. Best (Nov 02 2021 at 23:30):

Haha I'm glad I'm not alone!

Alex J. Best (Nov 02 2021 at 23:31):

Do you think there are some simp lemmas or something missing? Or anything we can extract from it in the end?

Riccardo Brasca (Nov 02 2021 at 23:38):

Maybe span R ({u * x} : set M) = span R ({x} : set M) deserves to be a simp lemma, but the rest is really what has to be done: the casesx=0 or y=0 have to treated separately (one is easier because u • x = y is not symmetric in x and y), and then R is non commutative, so one has to find both inverses.

Riccardo Brasca (Nov 10 2021 at 14:48):

@Alex J. Best @Chris Birkbeck I didn't follow all you have done. Have we decided the standard way of taking a primitive n-th roof of unity in K where (K : Type u) [field K] [char_zero K] (n : ℕ+) [is_cyclotomic_extension {n} ℚ K]? Is it zeta'?

Chris Birkbeck (Nov 10 2021 at 15:04):

I've been using zeta' for fields and zeta for rings (as is done in the cyclotomic units file)(if I remember correctly)

Riccardo Brasca (Nov 10 2021 at 15:12):

OK, I will use zeta'. I am wondering if zeta'_mem_base should become the definition of zeta', but maybe at some point someone will want to work with extension of fields without a reasonable base ring.

Riccardo Brasca (Oct 28 2021 at 14:30):

We currently have

variables [field L] [algebra K L] [is_cyclotomic_extension {n} K L]

include K n
def zeta' : L :=
classical.some (exists_root_of_splits (algebra_map K L) (is_splitting_field.splits _ _)
  (degree_cyclotomic_pos n K n.pos).ne.symm)

Before working on the various sorry, we need to generalize the defintion to A B....

Riccardo Brasca (Oct 28 2021 at 15:22):

I've started doing this in branch cycl_units_ring (I just wrote the new def). If someone wants to write some code I won't work on this until tomorrow morning.

Filippo A. E. Nuccio (Oct 28 2021 at 16:54):

I just have a side-remark: do you really want to call them "cyclotomic units"? They are roots of unit, rather, I think. The cyclotomic units are normally meant to be the elements in the subgroup generated by the ratios

ζpn1ζpna1\frac{\zeta_{p^n}-1}{\zeta_{p^n}^a-1}

for varying aa (the definition when the order is not a power of pp is slightly different), see
https://en.wikipedia.org/wiki/Cyclotomic_unit
Or am I misunderstainding your code?

Alex J. Best (Oct 28 2021 at 16:55):

That's what https://github.com/leanprover-community/flt-regular/blob/master/src/number_theory/cyclotomic/cyclotomic_units.lean#L191 is meant to become eventually, except currently nothing is proved.

Alex J. Best (Oct 28 2021 at 16:56):

So the filename refers to that def rather than the zeta itself

Filippo A. E. Nuccio (Oct 28 2021 at 17:02):

I see; so it is the (finite) sets of all things of the form

(r,n)=1,r<n)ζnr?\sum_{(r,n)=1, r<n)}\zeta_n^r ?

Or am I misreading the definition of aux?

Alex J. Best (Oct 28 2021 at 17:03):

Yes aux is a hacky way to define the inverse mod n, probably its best to replace it with an actual inverse in zmod n but I was just hacking around.

Alex J. Best (Oct 28 2021 at 17:04):

The idea of using the finite sums rather than the quotient is just to stay in the ring of integers and not worry about division

Filippo A. E. Nuccio (Oct 28 2021 at 17:06):

OK; because I am still slightly sceptical about this definition. Normally the "cyclotomic units" are an infinite group generated by some explicitely-defined things of that sort (they are of finite index...).

Filippo A. E. Nuccio (Oct 28 2021 at 17:08):

I would rather use the definition given in Theorem 8.3 of Washington's book Introduction to Cyclotomic Fields

Alex J. Best (Oct 28 2021 at 17:10):

Maybe basic_cyclotomic_unit is a better name? The point is just to define these generators yes.

Filippo A. E. Nuccio (Oct 28 2021 at 17:11):

Sounds much better! Just because otherwise there would be "usual" cyclotomic units which would not be mathlib ones.

Alex J. Best (Oct 28 2021 at 17:13):

I think for the purpose of this file I was (implicitly) assuming that the n was prime in what I was doing also, so I definitely didn't try and formulate the right general definition yet.

Riccardo Brasca (Oct 28 2021 at 17:18):

We can define it as a subgroup of the group of units, like primitive roots

Riccardo Brasca (Oct 28 2021 at 17:20):

And I really suggest we make the effort to give the most general definition

Riccardo Brasca (Oct 28 2021 at 17:21):

No problem in adding assumptions in theorems of course

Filippo A. E. Nuccio (Oct 28 2021 at 17:21):

Ok, so I would rather suggest to follow Washington's approach for general nn, personally.

Riccardo Brasca (Oct 29 2021 at 12:01):

zeta' and zeta are now defined for rings (mathematically they are the same thing, a primitive root of unity). @Chris Birkbeck do you think we really need the subgroup of cyclotomic units or for us it's enough to work with some specific element?

Chris Birkbeck (Oct 29 2021 at 12:05):

Well I don't think we need the whole subgroup (but I could be wrong). I think its enough to know that they are units.

Riccardo Brasca (Oct 29 2021 at 14:05):

OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is enough for us, right? We don't need ζpr\zeta_{p^r} I think

Riccardo Brasca (Oct 29 2021 at 14:06):

And even less ζn\zeta_n

Chris Birkbeck (Oct 29 2021 at 14:06):

Riccardo Brasca said:

OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is enough for us, right? We don't need ζpr\zeta_{p^r} I think

Yes that is enough

Riccardo Brasca (Oct 29 2021 at 14:37):

Unfortunately this does not seem to really simplify the problem compared to ζpr\zeta_{p^r}.

I am not sure what is the best approach here. In my opinion we should concentrate on proving this (I mean the description of the ring of integers), and go back to FLT once we have this.

Chris Birkbeck (Oct 29 2021 at 14:41):

Yes this is the first big hurdle, I guess we just need to make sure that if we prove this without using, say, embeddings, then we can do the same for the FLT. Otherwise we may end up having to do more work than needed.

Chris Birkbeck (Oct 29 2021 at 14:45):

Riccardo Brasca said:

Unfortunately this does not seem to really simplify the problem compared to ζpr\zeta_{p^r}.

I am not sure what is the best approach here. In my opinion we should concentrate on proving this (I mean the description of the ring of integers), and go back to FLT once we have this.

I think ζn\zeta_n it is actually more annoying, but pp vs prp^r is probably about the same.

Riccardo Brasca (Oct 29 2021 at 15:02):

The question is if we want to prove the final theorem as fast as possible or do we prefer doing things following mathlib style.

For example for the discriminant, I am quite sure it should be defined in general, without embeddings. A lot of elementary results are true for algebras that are finite and free over the base (for example what happens when you multiply the family by a matrix). Using embeddings from the start can make our life easier, but I think it's not the "right" way. I know, perfect is the enemy of good, and we have to make some compromise, but maybe not immediately.

Note that a good thing about OQ(ζp)=Z[ζp]\mathcal O_{\mathbb{Q}(\zeta_p)} = \mathbb{Z}[\zeta_p] is that this is a precise statement (it is already in the repo), so if someone prefers working on FLT he can do it immediately, a sorried lemma is as as good as a proved lemma. My suggestion is that we concentrate on this fact, but we can very well work on the two subprojects at the same time.

Riccardo Brasca (Oct 29 2021 at 15:03):

What we really have to do, in any case, is producing a lot of small sorried lemmas, and people will start proving them, even if they are not really interested in the whole project.

Chris Birkbeck (Oct 29 2021 at 15:06):

Ah sure I see what you mean about the discriminant. I was thinking only of the definition for number fields. But yes we may as well define them very generally. Using that we can probably give some enough sorried lemmas to get the ring of integers theorem going.

Riccardo Brasca (Oct 29 2021 at 15:14):

instance : is_integral_closure (cyclotomic_ring n  )  (cyclotomic_field n ) := sorry

is already there, in number_theory/cyclotomic/rat, so if someone needs it there are no problems.

Chris Birkbeck (Oct 29 2021 at 15:21):

Sorry I guess I meant get the proof going.

Chris Birkbeck (Oct 29 2021 at 15:23):

Riccardo Brasca said:

What we really have to do, in any case, is producing a lot of small sorried lemmas, and people will start proving them, even if they are not really interested in the whole project.

But should we do this first for the proof of the ring of integers or start from flt_regular and go down?

Riccardo Brasca (Oct 29 2021 at 15:26):

Well, this is exactly my question :smile:

Riccardo Brasca (Oct 29 2021 at 15:26):

We can do both ways of course

Chris Birkbeck (Oct 29 2021 at 15:26):

Riccardo Brasca said:

Well, this is exactly my question :smile:

Haha ok I see :)

Chris Birkbeck (Oct 29 2021 at 15:28):

Well I'd be partial to starting from flt_regular and going down. I was thinking about this, but then was scratching my head about how to do "An algebraic integer all of whose conjugates have absolute value one is a root of unity"

Riccardo Brasca (Oct 29 2021 at 15:28):

I personally suggest we concentrate on proving the instance, that means to develop a good theory of the discriminant (I've just pushed number_theory/discriminant/basic containing a definition). But if someone prefers working on the other part of the project there are no problem in using a sorried instance like that (since it is a proposition).

Chris Birkbeck (Oct 29 2021 at 15:31):

Oh well then I'm happy to do that. I have no real intuition as to what is best and since you've been doing this for longer I'm happy to follow your suggestion :)

Alex J. Best (Oct 29 2021 at 16:02):

It definitely seems some of the top-down steps can be done independently, thats what I've been idly thinking about with the may_assume tactic I was working on, how to make the outline of the proof quite readable.

Riccardo Brasca (Nov 02 2021 at 23:29):

@Alex J. Best Just for fun I've slightly golfed your submodule.span_singleton_eq_span_singleton. It is surprisingly annoying!

Alex J. Best (Nov 02 2021 at 23:30):

Haha I'm glad I'm not alone!

Alex J. Best (Nov 02 2021 at 23:31):

Do you think there are some simp lemmas or something missing? Or anything we can extract from it in the end?

Riccardo Brasca (Nov 02 2021 at 23:38):

Maybe span R ({u * x} : set M) = span R ({x} : set M) deserves to be a simp lemma, but the rest is really what has to be done: the casesx=0 or y=0 have to treated separately (one is easier because u • x = y is not symmetric in x and y), and then R is non commutative, so one has to find both inverses.

Riccardo Brasca (Nov 10 2021 at 14:48):

@Alex J. Best @Chris Birkbeck I didn't follow all you have done. Have we decided the standard way of taking a primitive n-th roof of unity in K where (K : Type u) [field K] [char_zero K] (n : ℕ+) [is_cyclotomic_extension {n} ℚ K]? Is it zeta'?

Chris Birkbeck (Nov 10 2021 at 15:04):

I've been using zeta' for fields and zeta for rings (as is done in the cyclotomic units file)(if I remember correctly)

Riccardo Brasca (Nov 10 2021 at 15:12):

OK, I will use zeta'. I am wondering if zeta'_mem_base should become the definition of zeta', but maybe at some point someone will want to work with extension of fields without a reasonable base ring.


Last updated: Dec 20 2023 at 11:08 UTC