# Dirichlet theorem on the group of units of a number field #

This file is devoted to the proof of Dirichlet unit theorem that states that the group of units (π K)Λ£ of units of the ring of integers π K of a number field K modulo its torsion subgroup is a free β€-module of rank card (InfinitePlace K) - 1.

## 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.Units.rank_modTorsion: the β€-rank of (π K)Λ£ β§Έ (torsion K) is equal to card (InfinitePlace K) - 1.

• 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, Dirichlet unit theorem

### Dirichlet 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β = β―.some
Instances For
def NumberField.Units.logEmbedding (K : Type u_1) [] [] :
β+ { 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β }) :
= β(βw).mult * Real.log (βw (() βx))
theorem NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component {K : Type u_1} [] [] (x : ) :
β w : { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ }, = -βNumberField.Units.dirichletUnitTheorem.wβ.mult * Real.log (NumberField.Units.dirichletUnitTheorem.wβ (() βx))
theorem NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero {K : Type u_1} [] {x : } {w : } :
βw.mult * Real.log (w (() βx)) = 0 β w (() βx) = 1
theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le {K : Type u_1} [] [] {r : β} {x : } (hr : 0 β€ r) (h : ) (w : { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ }) :
|| β€ r
theorem NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le {K : Type u_1} [] [] {r : β} {x : } (hr : 0 β€ r) (h : ) (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
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 : β) :
( β()).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) [] [] :
def NumberField.Units.logEmbeddingQuot (K : Type u_1) [] [] :
β+ { w : // w β  NumberField.Units.dirichletUnitTheorem.wβ } β β

The map obtained by quotienting by the kernel of logEmbedding.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem NumberField.Units.logEmbeddingQuot_apply (K : Type u_1) [] [] (x : ) :
β¦xβ§ =

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

Equations
Instances For
@[simp]
theorem NumberField.Units.logEmbeddingEquiv_apply (K : Type u_1) [] [] (x : ) :
β( β¦xβ§) =
Equations
• β― = β―
Equations
• β― = β―
Equations
• β― = β―
Equations
• β― = β―

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

Equations
• = .reindex ()
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.fundSystem_mk (K : Type u_1) [] [] (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.