[Merged by Bors] - feat(NumberTheory.NumberField.Units): proof of Dirichlet's unit theorem #5960
Conversation
xroblot
added
WIP
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
merge-conflict
…_mem_ringOfIntegers_lt (#5650) This PR proves the following result: ```lean theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) : ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w ``` where `f : InfinitePlace K → ℝ≥0` and `convex_body_lt K f` is the set of points `x` such that `‖x w‖ < f w` for all infinite places `w`. This is a key result in the proof of Dirichlet's unit theorem #5960
|
This is a really nice milestone! It's been quite a journey, but now all the prerequisites are in you're really on the home straight! |
Thanks! It was a very interesting project to work on. And now I have to find something new to work on ;) |
|
One final comment: we can add instance : Module.Finite ℤ (Additive (𝓞 K)ˣ)but I don't know if it is easy with current mathlib or it's better to wait for another PR. In any case thanks a lot!! bors d+ |
|
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
It is not so difficult to prove but there is some API missing for things like |
|
bors r+ |
…em (#5960) We prove Dirichlet's unit theorem. More precisely, the main results are: ```lean def basisModTorsion : Basis (Fin (Units.rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsion K))) ``` where `Units.rank := Fintype.card (InfinitePlace K) - 1` and ```lean theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! (ζ : torsion K) (e : Fin (Units.rank K) → ℤ), x = ζ * ∏ i, (fundSystem K i) ^ (e i) ``` where `fundSystem : Fin (rank K) → (𝓞 K)ˣ` is a fundamental system of units. The exponents in `exist_unique_eq_mul_prod` can be computed via the following result: ```lean theorem fun_eq_repr {x ζ : (𝓞 K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K) (h : x = ζ * ∏ i, (fundSystem K i) ^ (f i)) : f = (basisModTorsion K).repr (Additive.ofMul ↑x) ```
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
We prove Dirichlet's unit theorem. More precisely, the main results are:
where
Units.rank := Fintype.card (InfinitePlace K) - 1andwhere
fundSystem : Fin (rank K) → (𝓞 K)ˣis a fundamental system of units.The exponents in
exist_unique_eq_mul_prodcan be computed via the following result: