Dirichlet's unit theorem

Stream: maths

[Xavier Roblot]

I am very happy to announce that I have completed the proof of Dirichlet's unit theorem.

Well, there is still a lot of work left to put things into something that can be merged into Mathlib. At the moment, the proofs are
not optimized and there is probably some reorganizing that should be done but at least the proof is sorry-free.

If you want to have a look the PR is #18478. It relies on a series of 8 other PRs (including #2819 for the proofs of
Blichfeldt and Minkowski theorems) so I am not sure if it is reasonable to expect it to be
merged into Mathlib before the transition to Lean 4.

[Filippo A. E. Nuccio]

Congratulations, @Xavier Roblot !

[Xavier Roblot]

Now, let me say a few words about what is actually proved since I would like some feedback on the best way to state the theorem.

For K a number field, let 𝓤 K := (number_field.ring_of_integers K)ˣ denote the group of units
and define the log_embedding as the map

def log_embedding : (𝓤 K) → (number_field.infinite_place K → ℝ) := λ x w, real.log (w x)

The image of the log_embedding is the ℤ-submodule called unit_lattice K.

The first result is that the kernel of this map is the subgroup of roots_of_unity of 𝓤 K:

lemma unit_lattice_kernel (x : 𝓤 K) :
  log_embedding K x = 0 ↔ x ∈ roots_of_unity K

where roots_of_unity := comm_group.torsion (𝓤 K).

Then, the main part is to prove that unit_lattice K is a free ℤ-module of rank
unit_rank K with unit_rank := fintype.card (infinite_place K) - 1.

The result is stated by first constructing the basis:

def unit_lattice.basis : Σ (n : ℕ), basis (fin n) ℤ (unit_lattice K)

and then proving it has the right cardinality

lemma unit_lattice.dim : (unit_lattice.basis K).1 = unit_rank K

This is probably not the most elegant way to state the result so I am open to suggestion for a better way to express that.

Also, I am not sure on how to state the result for the group of units 𝓤 K. There is first the problem
that log_embedding is not a monoid_hom since it goes from a multiplicative
group to an additive group. I am aware that there are ways to deal with this situation using the tools
developed in number_theory.legendre_symbol.add_character but I am not sure what is the right way to do
that. One option would be to work with multiplicative (number_field.infinite_place K → ℝ) or something like that.

In any case, I'd like to get some feedbacks on what would be the best way to state the result for 𝓤 K.

[Johan Commelin]

Very nice!

[Johan Commelin]

I think #2819 is very very close to being mergeable

[Johan Commelin]

But it depends on a PR that is currently somewhat in limbo.

[Yaël Dillies]

Yeah sorry about that! I'm trying to find time for it but it's hard during term-time.

[Johan Commelin]

If we get this whole stack merged, we can tick off two more items on 100.yaml :smiley:

[Kevin Buzzard]

This is great! This was the only ingredient that David Ang was missing for his proof of weak Mordell-Weil (E{K)/n is finite if K is a number field)

[Riccardo Brasca]

Congratulations, this is really great!! As a trivial remark, can you replace number_field.ring_of_integers by anything such that is_integral_closure...? :innocent:

[Xavier Roblot]

There are certainly results that should be stated in terms of is_integral_closure like for example the ones about integral basis. But I have the feeling what you want is a bit more general. In any case, I would think that most (and maybe even all) of the results of this proof are also true for anything that satisfy is_integral_closure using docs#is_integral_closure.equiv? Am I missing something?

[Riccardo Brasca]

My remark is mathematically totally irrelevant and as you say the two are trivially equivalent. The advantage of is_integral_closure is that if someone ends up somehow with R that morally is 𝓞 K, but not literally they can use your results.

[Xavier Roblot]

I see your point. I’ll see what can be done but I think it shouldn’t be too much of a problem. It depends also on what would be the optimal statement for the final result.

[Johan Commelin]

Another comment/question: mathlib already has a notion of roots_of_unity. Do I understand correctly that you are not using that version?

[Xavier Roblot]

Yes, I am using a different definition for roots_of_unity for the moment, but that is typically the kind of things that could be changed. I just used what was more practical at the time.

[Xavier Roblot]

Two PRs for this project #18266 and #18473 are ready for review. (Eric left some reviews already on #18266). #17783 is also ready for review but it depends on #18473.

@Riccardo Brasca I changed #17783 so that it uses is_integral_closure instead of 𝓞 K. Can you check that it is indeed what you had in mind?

[Riccardo Brasca]

Hmm, I meant to use it for results about the ring of integers (for example we should know the rank of any R such that is_integral_closure rather than just the norm of 𝓞 K). Using R to define integer_lattice seems a little strange, since I would say it is something only depends on K.

[Xavier Roblot]

I see. I guess I got a little bit too enthusiastic :smile: