# Units of a number field #

We prove results about the group (π K)Λ£ of units of the ring of integers π K of a number field K.

## Main definitions #

• NumberField.Units.rank: the unit rank of the number field K.

• NumberField.Units.fundSystem: a fundamental system of units of K.

• NumberField.Units.basisModTorsion: a β€-basis of (π K)Λ£ β§Έ (torsion K) as an additive β€-module.

## Main results #

• NumberField.isUnit_iff_norm: an algebraic integer x : π K is a unit if and only if |norm β x| = 1.

• NumberField.Units.mem_torsion: a unit x : (π K)Λ£ is torsion iff w x = 1 for all infinite places w of K.

• NumberField.Units.exist_unique_eq_mul_prod: Dirichlet Unit Theorem. Any unit of π K can be written uniquely as the product of a root of unity and powers of the units of the fundamental system fundSystem.

## Tags #

number field, units

theorem Rat.RingOfIntegers.isUnit_iff {x : } :
β βx = 1 β¨ βx = -1
theorem NumberField.isUnit_iff_norm {K : Type u_1} [] [] {x : β₯} :
β |β()| = 1
theorem NumberField.Units.coe_injective (K : Type u_1) [] :
Function.Injective fun (x : (β₯)Λ£) => ββx
theorem NumberField.Units.coe_mul {K : Type u_1} [] (x : (β₯)Λ£) (y : (β₯)Λ£) :
ββ(x * y) = ββx * ββy
theorem NumberField.Units.coe_pow {K : Type u_1} [] (x : (β₯)Λ£) (n : β) :
ββ(x ^ n) = ββx ^ n
theorem NumberField.Units.coe_zpow {K : Type u_1} [] (x : (β₯)Λ£) (n : β€) :
ββ(x ^ n) = ββx ^ n
theorem NumberField.Units.coe_one {K : Type u_1} [] :
ββ1 = 1
theorem NumberField.Units.coe_neg_one {K : Type u_1} [] :
ββ(-1) = -1
theorem NumberField.Units.coe_ne_zero {K : Type u_1} [] (x : (β₯)Λ£) :
ββx β  0
def NumberField.Units.torsion (K : Type u_1) [] :
Subgroup (β₯)Λ£

The torsion subgroup of the group of units.

Equations
Instances For
theorem NumberField.Units.mem_torsion (K : Type u_1) [] {x : (β₯)Λ£} [] :
β β (w : ), w ββx = 1

Shortcut instance because Lean tends to time out before finding the general instance.

Equations
• β― = β―

The torsion subgroup is finite.

Equations
• One or more equations did not get rendered due to their size.

The order of the torsion subgroup as a positive integer.

Equations
• = { val := , property := β― }
Instances For
theorem NumberField.Units.rootsOfUnity_eq_one (K : Type u_1) [] [] {k : β+} (hc : Nat.Coprime βk ) {ΞΆ : (β₯)Λ£} :
ΞΆ β β ΞΆ = 1

If k does not divide torsionOrder then there are no nontrivial roots of unity of order dividing k.

The group of roots of unity of order dividing torsionOrder is equal to the torsion group.

### Dirichlet Unit Theorem #

This section is devoted to the proof of Dirichlet's unit theorem.

We define a group morphism from (π K)Λ£ to {w : InfinitePlace K // w β  wβ} β β where wβ is a distinguished (arbitrary) infinite place, prove that its kernel is the torsion subgroup (see logEmbedding_eq_zero_iff) and that its image, called unitLattice, is a full β€-lattice. It follows that unitLattice is a free β€-module (see instModuleFree_unitLattice) of rank card (InfinitePlaces K) - 1 (see unitLattice_rank). To prove that the unitLattice is a full β€-lattice, we need to prove that it is discrete (see unitLattice_inter_ball_finite) and that it spans the full space over β (see unitLattice_span_eq_top); this is the main part of the proof, see the section span_top below for more details.

The distinguished infinite place.

Equations
• NumberField.Units.dirichletUnitTheorem.wβ =
Instances For
def NumberField.Units.dirichletUnitTheorem.logEmbedding (K : Type u_1) [] [] :
Additive (β₯)Λ£ β+ { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ } β β

The logarithmic embedding of the units (seen as an Additive group).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component {K : Type u_1} [] [] (x : (β₯)Λ£) (w : { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ }) :
= β * Real.log (βw ββx)
theorem NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component {K : Type u_1} [] [] (x : (β₯)Λ£) :
(Finset.sum Finset.univ fun (w : { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ }) => ) = -β(NumberField.InfinitePlace.mult NumberField.Units.dirichletUnitTheorem.wβ) * Real.log (NumberField.Units.dirichletUnitTheorem.wβ ββx)
theorem NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero {K : Type u_1} [] {x : (β₯)Λ£} {w : } :
* Real.log (w ββx) = 0 β w ββx = 1
theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le {K : Type u_1} [] [] {r : β} {x : (β₯)Λ£} (hr : 0 β€ r) (w : { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ }) :
theorem NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le {K : Type u_1} [] [] {r : β} {x : (β₯)Λ£} (hr : 0 β€ r) (w : ) :
|Real.log (w ββx)| β€ β * r
noncomputable def NumberField.Units.unitLattice (K : Type u_1) [] [] :
AddSubgroup ({ w : // w β  NumberField.Units.dirichletUnitTheorem.wβ } β β)

The lattice formed by the image of the logarithmic embedding.

Equations
Instances For

#### Section span_top#

In this section, we prove that the span over β of the unitLattice is equal to the full space. For this, we construct for each infinite place wβ β  wβ a unit u_wβ of K such that, for all infinite places w such that w β  wβ, we have Real.log w (u_wβ) < 0 (and thus Real.log wβ (u_wβ) > 0). It follows then from a determinant computation (using Matrix.det_ne_zero_of_sum_col_lt_diag) that the image by logEmbedding of these units is a β-linearly independent family. The unit u_wβ is obtained by constructing a sequence seq n of nonzero algebraic integers that is strictly decreasing at infinite places distinct from wβ and of norm β€ B. Since there are finitely many ideals of norm β€ B, there exists two term in the sequence defining the same ideal and their quotient is the desired unit u_wβ (see exists_unit).

theorem NumberField.Units.dirichletUnitTheorem.seq_next (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) {x : β₯} (hx : x β  0) :
β (y : β₯), y β  0 β§ (β (w : ), w β  wβ β w βy < w βx) β§ | βy| β€ βB

This result shows that there always exists a next term in the sequence.

def NumberField.Units.dirichletUnitTheorem.seq (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) :
β β { x : β₯ // x β  0 }

An infinite sequence of nonzero algebraic integers of K satisfying the following properties: β’ seq n is nonzero; β’ for w : InfinitePlace K, w β  wβ β w (seq n+1) < w (seq n); β’ β£norm (seq n)β£ β€ B.

Equations
• = { val := 1, property := β― }
• = { val := , property := β― }
Instances For
theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) (n : β) :
ββ() β  0

The terms of the sequence are nonzero.

theorem NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) (n : β) :
β() β  0

The terms of the sequence have nonzero norm.

theorem NumberField.Units.dirichletUnitTheorem.seq_decreasing (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) {n : β} {m : β} (h : n < m) (w : ) (hw : w β  wβ) :
w ββ() < w ββ()

The sequence is strictly decreasing at infinite places distinct from wβ.

theorem NumberField.Units.dirichletUnitTheorem.seq_norm_le (K : Type u_1) [] [] (wβ : ) {B : β} (hB : ) (n : β) :
Int.natAbs ( β()) β€ B

The terms of the sequence have norm bounded by B.

theorem NumberField.Units.dirichletUnitTheorem.exists_unit (K : Type u_1) [] [] (wβ : ) :
β (u : (β₯)Λ£), β (w : ), w β  wβ β Real.log (w ββu) < 0

Construct a unit associated to the place wβ. The family, for wβ β  wβ, formed by the image by the logEmbedding of these units is β-linearly independent, see unitLattice_span_eq_top.

def NumberField.Units.rank (K : Type u_1) [] [] :

The unit rank of the number field K, it is equal to card (InfinitePlace K) - 1.

Equations
Instances For
Equations
• β― = β―
Equations
• β― = β―
theorem NumberField.Units.finrank_eq_rank (K : Type u_1) [] [] :
FiniteDimensional.finrank β ({ w : // w β  NumberField.Units.dirichletUnitTheorem.wβ } β β) =
@[simp]
theorem NumberField.Units.unitLattice_rank (K : Type u_1) [] [] :

The linear equivalence between unitLattice and (π K)Λ£ β§Έ (torsion K) as an additive β€-module.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A basis of the quotient (π K)Λ£ β§Έ (torsion K) seen as an additive β€-module.

Equations
Instances For
def NumberField.Units.fundSystem (K : Type u_1) [] [] :
β (β₯)Λ£

A fundamental system of units of K. The units of fundSystem are arbitrary lifts of the units in basisModTorsion.

Equations
Instances For
theorem NumberField.Units.fun_eq_repr (K : Type u_1) [] [] {x : (β₯)Λ£} {ΞΆ : (β₯)Λ£} {f : β β€} (hΞΆ : ) (h : x = ΞΆ * Finset.prod Finset.univ fun (i : ) => ) :
The exponents that appear in the unique decomposition of a unit as the product of a root of unity and powers of the units of the fundamental system fundSystem (see exist_unique_eq_mul_prod) are given by the representation of the unit on basisModTorsion.
Dirichlet Unit Theorem. Any unit x of π K can be written uniquely as the product of a root of unity and powers of the units of the fundamental system fundSystem.