Units of number fields

Stream: general

[Xavier Roblot]

What is the best way to define the group of units of a number field K? I have tried to use (number_field.ring_of_integers K)ˣ but there are some issues when I want to coerce the units into K, for example:

import number_theory.number_field.basic

variables {K : Type*} [field K] [number_field K]

example (x : (number_field.ring_of_integers K)ˣ) : (x : number_field.ring_of_integers K) ≠ 0 :=
   units.ne_zero x -- works

example (x : (number_field.ring_of_integers K)ˣ) : (x : K) ≠ 0 :=
   units.ne_zero x -- fails

[Junyan Xu]

You can do

example (x : (number_field.ring_of_integers K)ˣ) : (x : K) ≠ 0 :=
mt (by { rw subtype.ext_iff, exact id }) (units.ne_zero x)

[Junyan Xu]

You can also define it as a subgroup of units K via docs#set.unit since we have docs#number_field.ring_of_integers.is_fraction_ring and docs#number_field.ring_of_integers.is_dedekind_domain

[Adam Topaz]

There must be a general lemma saying that when A is a domain and K is any localization of A, that the units of A are nonzero in K. I suppose mathlib knows that the number field is a localization of its ring of integers?

[Anne Baanen]

I think you should be able to do this a bit more concisely with docs#map_ne_zero_iff, something like (untested) (map_ne_zero_iff (is_localization.injective _ _)).mpr x.ne_zero

[Xavier Roblot]

Junyan Xu said:

You can also define it as a subgroup of units K via docs#set.unit since we have docs#number_field.ring_of_integers.is_fraction_ring and docs#number_field.ring_of_integers.is_dedekind_domain

Yes, that looks like a good idea. I'll try that.

[Anne Baanen]

Adam Topaz said:

There must be a general lemma saying that when A is a domain and K is any localization of A, that the units of A are nonzero in K. I suppose mathlib knows that the number field is a localization of its ring of integers?

The last one yes: docs#number_field.ring_of_integers.is_fraction_ring

[Junyan Xu]

But maybe docs#set.unit isn't usable yet because it lacks some API; for example this hasn't been PR'd yet.

[Riccardo Brasca]

If you have a look in the flt-regular project we have some results about units.

[Riccardo Brasca]

In number_theory/cyclotomic/Unit_lemmas.lean

[Riccardo Brasca]

(the file is a little mess)

[Xavier Roblot]

Riccardo Brasca said:

If you have a look in the flt-regular project we have some results about units.

It seems that the idea there is that (𝓞 K)ˣ is the right object which I quite agree. I also see a lot of things there that could be very useful for me. Is there any plan to PR these soon?

[Xavier Roblot]

I now have all the tools to define the logarithmic embedding of units of a number field but we need to decide first what is the right way to look at units of number fields...

[Riccardo Brasca]

Not really, but feel free to use/PR anything you want!

[David Ang]

(deleted)

[Xavier Roblot]

After different trials, I think the following definition is the most convenient (at least for my needs).

variables (K : Type*) [field K]

def number_field.group_of_units : subgroup Kˣ :=
{ carrier := { x : Kˣ | is_integral ℤ (x : K) ∧ is_integral ℤ (x⁻¹ : K) },

[Riccardo Brasca]

Are you sure? Of course it depends on what you want to do, but maybe if the API for units is not good enough for (𝓞 K)ˣ we should improve it.

[Xavier Roblot]

Well, I have not committed to anything yet. I agree that (𝓞 K)ˣ is also a valid choice and I am willing to develop the necessary API for it if we decide that it is the best choice. I guess seeing the units as a subgroup Kˣ(as above) is easier for me because I want to define the log embedding on Kˣ as it might have other applications outside of the study of units, but maybe it is a bad design choice and I should just define it only on (𝓞 K)ˣ.

[Riccardo Brasca]

I agree it's useful to be able to see (𝓞 K)ˣ as a subgroup of Kˣ, but maybe a coercion is enough. I think @Chris Birkbeck , @Eric Rodriguez and @Alex J. Best wrote most of the work about units in flt-regular, maybe they have an opinion.

[Filippo A. E. Nuccio]

I somewhat agree with @Riccardo Brasca that (𝓞 K)ˣ seems a better choice, especiallly if you will need to speak about S-units or units in algebraic fields that are not finite over $\mathbb{Q}$.

[Chris Birkbeck]

Riccardo Brasca said:

I agree it's useful to be able to see (𝓞 K)ˣ as a subgroup of Kˣ, but maybe a coercion is enough. I think Chris Birkbeck , Eric Rodriguez and Alex J. Best wrote most of the work about units in flt-regular, maybe they have an opinion.

I remember it being a pain to use, but I'd also vote for working with (𝓞 K)ˣ.

[Kevin Buzzard]

Why not just have both?

[Kevin Buzzard]

One is a type, one is a term, probably the type is the thing to use in general but if the term is useful in one file then just make the term and a little API for it. But if you want a type (and you certainly will in many cases), you probably don't want to make the term as the primary object and then coerce it to a type because this just adds a layer of confusion. So the type (𝓞 K)ˣ should probably be the primary thing but if the term of type subgroup Kˣ is useful in some places, use the term.

[Xavier Roblot]

Yes, this is what I am doing at the moment. I mainly use (𝓞 K)ˣ as the group of units of a number field and I plan to use the subgroup Kˣ only when it is more convenient (mainly when dealing with the logarithmic embedding). For the moment, I am using an equiv between the two but I might also add a coercion at some point.

[Eric Rodriguez]

units (𝓞 K) is still a term - there should probably be a thing that makes it into a subgroup of K*, but that in general, as opposed to just "the units subgroup" - I wonder if it's just subgroup.map or whatever.

[Eric Rodriguez]

You're never sad to have more information, though, because having lemmas proving that things are integral quickly does get annoying, in my experience.

[Eric Wieser]

I imagine it's something like (units.map $ algebra_map (𝒪 K) K).range?

[Xavier Roblot]

Yes, that is what I am using at the moment.

[Anne Baanen]

I think that's a fine idea. It might have to be docs#has_coe_t because it has the potential to loop: the target _ˣ has the same shape as the source (𝓞 _)ˣ so depending on implementation details that I don't quite remember you could get an infinite loop of (𝓞 (𝓞 (𝓞 (𝓞 (𝓞 ...)))))ˣ → K.

[Anne Baanen]

If you can write (↑(units.mk _ _) : Kˣ and you don't get a timeout, everything should be fine.

[Xavier Roblot]

There does not seem to be an infinite loop for the time being. I can write (↑(units.mk _ _) : Kˣ) without any timeout... But I'll keep an eye on it and might get back to you if things get nasty.