Support for cyclotomic units

Stream: maths

[Dimitar Jetchev]

Hello, I am new to Lean but would like to potentially add some support for cyclotomic units. I'd appreciate if someone can help with the existing support for cyclotomic fields. If you are an expert on that, feel free to DM me or post here the relevant references. Thanks!

[Kevin Buzzard]

In what generality should the definition be made? I'm asking a mathematical question

[Riccardo Brasca]

Dimitar Jetchev said:

Hello, I am new to Lean but would like to potentially add some support for cyclotomic units. I'd appreciate if someone can help with the existing support for cyclotomic fields. If you are an expert on that, feel free to DM me or post here the relevant references. Thanks!

Just feel free to ask any question here!

[Dimitar Jetchev]

Kevin Buzzard said:

In what generality should the definition be made? I'm asking a mathematical question

@Kevin Buzzard - that's a good question - still need to flesh this out - I see that the basic support for cyclotomic rings is quite general - it supports rings of any characteristic and infinite extensions (adding primitive $n$th roots for multiple $n$'s), but it is mainly used for integral domains and a single $n$. One of the future objectives with this would be adding support for the cyclotomic units Euler system (which you suggested as potentially useful for other projects) - it can be useful to keep this in mind. @Riccardo Brasca - do you have any thoughts here?

[Riccardo Brasca]

The first suggestion is to avoid docs#CyclotomicRing : it was a mistake and sooner or later we will remove it.

[Riccardo Brasca]

Then it really depends on what you want to do. The very basics are there, but the theory has been introduced to prove Fermat last theorem for regular primes, so for example we don't even know the ring of integers for a general n (only for prime powers)

[Riccardo Brasca]

In my opinion a good start would be to define the subgroup of cyclotomic units in this case.

[Dimitar Jetchev]

Riccardo Brasca said:

In my opinion a good start would be to define the subgroup of cyclotomic units in this case.

Thank you - that makes sense as a first mini-project for a beginner like me :)

[Riccardo Brasca]

also keep in mind the writing definitions is usually harder than proving theorems, so it's a good idea to discuss the implementation here!

[Dimitar Jetchev]

Riccardo Brasca said:

also keep in mind the writing definitions is usually harder than proving theorems, so it's a good idea to discuss the implementation here!

will do!

[Kevin Buzzard]

I doubt we will need the unproved-in-lean theorem that the integers of $\mathbb{Q}(\zeta_n)$ are $\Z[\zeta_n]$ for the definition. Dimitar I ask again: can you post the mathematics behind the definition you want to formalise? You can write Latex here if you enclose it in double $ signs. After you've done that, a lean expert can then do the "definition" part of the job leaving you with only theorems to prove.

[Dimitar Jetchev]

Kevin Buzzard said:

I doubt we will need the unproved-in-lean theorem that the integers of $\mathbb{Q}(\zeta_n)$ are $\Z[\zeta_n]$ for the definition. Dimitar I ask again: can you post the mathematics behind the definition you want to formalise? You can write Latex here if you enclose it in double $ signs. After you've done that, a lean expert can then do the "definition" part of the job leaving you with only theorems to prove.

Kevin, thanks, I will post directly the latex here.

[Kevin Buzzard]

I think it's fine to stick to cyclotomic fields rather than general rings with roots of unity added or whatever -- but I'm a bit unclear for which $n$ the theory is useful.

[Dimitar Jetchev]

Kevin Buzzard said:

I think it's fine to stick to cyclotomic fields rather than general rings with roots of unity added or whatever -- but I'm a bit unclear for which $n$ the theory is useful.

It depends on how one envisions to use this in the future: It is clearly easier to prove that the index of the cyclotomic units in the full group of units for the real subfield is the class number of that subfield in the case $n = p^k$ compared to the general case. But if one wants, e.g., Kronecker-Weber and more advanced applications such as Thaine's theorem, or the Euler system of cyclotomic units, then one most likely needs general $n$. @Kevin Buzzard : you mentioned a longer-term project you in mind to make use of that - I assume this may require support for the Euler systems of cyclotomic units?

[Kevin Buzzard]

I had this vague memory that the definition was different for general $n$ than for prime powers, because $1-\zeta_n$ was sometimes a unit if $n$ had two prime factors or something?

[Dimitar Jetchev]

Kevin Buzzard said:

I had this vague memory that the definition was different for general $n$ than for prime powers, because $1-\zeta_n$ was sometimes a unit if $n$ had two prime factors or something?

Yes, the difference is that for prime powers, the cyclotomic units for $\mathbb{Q}(\zeta_{p^m})$ are generated by units of the form $\frac{1 - \zeta_{p^m}^a}{1 - \zeta_{p^m}}$'s for various $(a, p) = 1$ and roots of unity. If $n$ is not a prime power, this is not necessarily the case: for example, one can show that $1 - \zeta_n$ is a unit, but it is not in the group generated by roots of unity and the above units. Yet, one can show that this subgroup is of index two when $n$ is not a prime power.

[Kevin Buzzard]

So do you have a conceptual definition of the cyclotomic units? Oh -- is it simply the intersection of $\mathcal{O}_K^\times$ and the subgroup of $K^\times$ generated by things of the form $1-\zeta$?

[Dimitar Jetchev]

Kevin Buzzard said:

So do you have a conceptual definition of the cyclotomic units? Oh -- is it simply the intersection of $\mathcal{O}_K^\times$ and the subgroup of $K^\times$ generated by things of the form $1-\zeta$?

Yes, the subgroup is generated by $\pm \zeta_n$ and $1 - \zeta_n^k$ for $k = 1, \dots, n-1$. At least when $n$ is not 2 mod 4.

[Kevin Buzzard]

So what is the definition when $n$ is 2 mod 4? We can't formalise the definition until we know the maths.

[David Loeffler]

Kevin Buzzard said:

So do you have a conceptual definition of the cyclotomic units? Oh -- is it simply the intersection of $\mathcal{O}_K^\times$ and the subgroup of $K^\times$ generated by things of the form $1-\zeta$?

This is the definition, in all cases. Dimitar’s last msg gives an equivalent formulation for certain n, but the def which works for all n is this one.

[Dimitar Jetchev]

Yes, indeed - I should have been more clear in my previous message - this equivalent formulation (when $n$ is not 2 mod 4) is convenient for proving some statements, but we should take the general definition and prove the equivalence in the particular case whenever it is needed.

[Filippo A. E. Nuccio]

I am not really sure that this might be the right level of generality if we want to have some more advanced Iwasawa theory. If you start with an arbitrary abelian extension, the definition of circular units is the right one (and reduces to the above when the extension is $\mathbb{Q}(\zeta_n)$ for some $n$). Also for this, there is the "classical" difference between Sinnott's and Washinton's definition of circular units, that "asymptotically" coincide in the limit but are different at finite levels, see this paper (here a free version) by Belliard.

[Filippo A. E. Nuccio]

IMHO, as long as we cannot do more advanced class field theory, we can stick with defining cyclotomic units for $\mathbb{Q}(\zeta_{p^k})$ ($p$ a prime, and $k\geq 1$) and prove for those that the index coincides with the class number of the plus-part, as in Washington's theorem 8.2.