Cyclotomic units

Stream: FLT-regular

[Riccardo Brasca]

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]

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]

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

$$\frac{\zeta_{p^n}-1}{\zeta_{p^n}^a-1}$$

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

[Alex J. Best]

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]

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

[Filippo A. E. Nuccio]

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

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

Or am I misreading the definition of aux?

[Alex J. Best]

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]

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]

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]

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

[Alex J. Best]

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

[Filippo A. E. Nuccio]

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

[Alex J. Best]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

No problem in adding assumptions in theorems of course

[Filippo A. E. Nuccio]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

And even less $\zeta_n$

[Chris Birkbeck]

Riccardo Brasca said:

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

Yes that is enough

[Riccardo Brasca]

Unfortunately this does not seem to really simplify the problem compared to $\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]

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]

Riccardo Brasca said:

Unfortunately this does not seem to really simplify the problem compared to $\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 $\zeta_n$ it is actually more annoying, but $p$ vs $p^r$ is probably about the same.

[Riccardo Brasca]

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 $\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]

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]

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]

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]

Sorry I guess I meant get the proof going.

[Chris Birkbeck]

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]

Well, this is exactly my question :smile:

[Riccardo Brasca]

We can do both ways of course

[Chris Birkbeck]

Riccardo Brasca said:

Well, this is exactly my question :smile:

Haha ok I see :)

[Chris Birkbeck]

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]

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]

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]

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]

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

[Alex J. Best]

Haha I'm glad I'm not alone!

[Alex J. Best]

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

[Riccardo Brasca]

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]

@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]

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]

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]

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]

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]

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

$$\frac{\zeta_{p^n}-1}{\zeta_{p^n}^a-1}$$

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

[Alex J. Best]

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]

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

[Filippo A. E. Nuccio]

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

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

Or am I misreading the definition of aux?

[Alex J. Best]

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]

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]

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]

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

[Alex J. Best]

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

[Filippo A. E. Nuccio]

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

[Alex J. Best]

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]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

No problem in adding assumptions in theorems of course

[Filippo A. E. Nuccio]

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

[Riccardo Brasca]

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]

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]

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

[Riccardo Brasca]

And even less $\zeta_n$

[Chris Birkbeck]

Riccardo Brasca said:

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

Yes that is enough

[Riccardo Brasca]

Unfortunately this does not seem to really simplify the problem compared to $\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]

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]

Riccardo Brasca said:

Unfortunately this does not seem to really simplify the problem compared to $\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 $\zeta_n$ it is actually more annoying, but $p$ vs $p^r$ is probably about the same.

[Riccardo Brasca]

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 $\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]

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]

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]

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]

Sorry I guess I meant get the proof going.

[Chris Birkbeck]

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]

Well, this is exactly my question :smile:

[Riccardo Brasca]

We can do both ways of course

[Chris Birkbeck]

Riccardo Brasca said:

Well, this is exactly my question :smile:

Haha ok I see :)

[Chris Birkbeck]

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]

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]

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]

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]

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

[Alex J. Best]

Haha I'm glad I'm not alone!

[Alex J. Best]

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

[Riccardo Brasca]

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]

@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]

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]

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.