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 logSpace K, defined as {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.

def NumberField.Units.dirichletUnitTheorem.w₀ {K : Type u_1} [Field K] [NumberField K] : InfinitePlace K

The distinguished infinite place.

@[reducible, inline]

abbrev NumberField.Units.dirichletUnitTheorem.logSpace (K : Type u_1) [Field K] [NumberField K] : Type u_1

The logSpace is defined as {w : InfinitePlace K // w ≠ w₀} → ℝ where w₀ is the distinguished infinite place.

def NumberField.Units.logEmbedding (K : Type u_1) [Field K] [NumberField K] : Additive (RingOfIntegers K)ˣ →+ dirichletUnitTheorem.logSpace K

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

@[simp]

theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) (w : { w : InfinitePlace K // w ≠ w₀ }) : (logEmbedding K) (Additive.ofMul x) w = ↑(↑w).mult * Real.log (↑w ((algebraMap (RingOfIntegers K) K) ↑x))

theorem NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component {K : Type u_1} [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) : ∑ w : { w : InfinitePlace K // w ≠ w₀ }, (logEmbedding K) (Additive.ofMul x) w = -↑w₀.mult * Real.log (w₀ ((algebraMap (RingOfIntegers K) K) ↑x))

theorem NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero {K : Type u_1} [Field K] {x : (RingOfIntegers K)ˣ} {w : InfinitePlace K} : ↑w.mult * Real.log (w ((algebraMap (RingOfIntegers K) K) ↑x)) = 0 ↔ w ((algebraMap (RingOfIntegers K) K) ↑x) = 1

theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] {x : (RingOfIntegers K)ˣ} : (logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ torsion K

theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le {K : Type u_1} [Field K] [NumberField K] {r : ℝ} {x : (RingOfIntegers K)ˣ} (hr : 0 ≤ r) (h : ‖(logEmbedding K) x‖ ≤ r) (w : { w : InfinitePlace K // w ≠ w₀ }) : |(logEmbedding K) (Additive.ofMul x) w| ≤ r

theorem NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le {K : Type u_1} [Field K] [NumberField K] {r : ℝ} {x : (RingOfIntegers K)ˣ} (hr : 0 ≤ r) (h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r) (w : InfinitePlace K) : |Real.log (w ((algebraMap (RingOfIntegers K) K) ↑x))| ≤ ↑(Fintype.card (InfinitePlace K)) * r

noncomputable def NumberField.Units.unitLattice (K : Type u_1) [Field K] [NumberField K] : Submodule ℤ (dirichletUnitTheorem.logSpace K)

The lattice formed by the image of the logarithmic embedding.

theorem NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite (K : Type u_1) [Field K] [NumberField K] (r : ℝ) : (↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite

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) [Field K] [NumberField K] (w₁ : InfinitePlace K) {B : ℕ} (hB : mixedEmbedding.minkowskiBound K 1 < ↑(mixedEmbedding.convexBodyLTFactor K) * ↑B) {x : RingOfIntegers K} (hx : x ≠ 0) : ∃ (y : RingOfIntegers K), y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B

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

def NumberField.Units.dirichletUnitTheorem.seq (K : Type u_1) [Field K] [NumberField K] (w₁ : InfinitePlace K) {B : ℕ} (hB : mixedEmbedding.minkowskiBound K 1 < ↑(mixedEmbedding.convexBodyLTFactor K) * ↑B) : ℕ → { x : RingOfIntegers K // 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.

theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero (K : Type u_1) [Field K] [NumberField K] (w₁ : InfinitePlace K) {B : ℕ} (hB : mixedEmbedding.minkowskiBound K 1 < ↑(mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : ℕ) : (algebraMap (RingOfIntegers K) K) ↑(seq K w₁ hB n) ≠ 0

The terms of the sequence are nonzero.

theorem NumberField.Units.dirichletUnitTheorem.seq_decreasing (K : Type u_1) [Field K] [NumberField K] (w₁ : InfinitePlace K) {B : ℕ} (hB : mixedEmbedding.minkowskiBound K 1 < ↑(mixedEmbedding.convexBodyLTFactor K) * ↑B) {n m : ℕ} (h : n < m) (w : InfinitePlace K) (hw : w ≠ w₁) : w ((algebraMap (RingOfIntegers K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (RingOfIntegers K) K) ↑(seq K w₁ hB n))

The sequence is strictly decreasing at infinite places distinct from w₁.

theorem NumberField.Units.dirichletUnitTheorem.seq_norm_le (K : Type u_1) [Field K] [NumberField K] (w₁ : InfinitePlace K) {B : ℕ} (hB : mixedEmbedding.minkowskiBound K 1 < ↑(mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : ℕ) : ((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B

The terms of the sequence have norm bounded by B.

theorem NumberField.Units.dirichletUnitTheorem.exists_unit (K : Type u_1) [Field K] [NumberField K] (w₁ : InfinitePlace K) : ∃ (u : (RingOfIntegers K)ˣ), ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (RingOfIntegers K) K) ↑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.

theorem NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top (K : Type u_1) [Field K] [NumberField K] : Submodule.span ℝ ↑(unitLattice K) = ⊤

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

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

instance NumberField.Units.instDiscrete_unitLattice (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(unitLattice K)

instance NumberField.Units.instZLattice_unitLattice (K : Type u_1) [Field K] [NumberField K] : IsZLattice ℝ (unitLattice K)

theorem NumberField.Units.finrank_eq_rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℝ (dirichletUnitTheorem.logSpace K) = rank K

@[simp]

theorem NumberField.Units.unitLattice_rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℤ ↥(unitLattice K) = rank K

def NumberField.Units.logEmbeddingQuot (K : Type u_1) [Field K] [NumberField K] : Additive ((RingOfIntegers K)ˣ ⧸ torsion K) →+ dirichletUnitTheorem.logSpace K

The map obtained by quotienting by the kernel of logEmbedding.

@[simp]

theorem NumberField.Units.logEmbeddingQuot_apply (K : Type u_1) [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) : (logEmbeddingQuot K) (Additive.ofMul ↑x) = (logEmbedding K) (Additive.ofMul x)

theorem NumberField.Units.logEmbeddingQuot_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ⇑(logEmbeddingQuot K)

def NumberField.Units.logEmbeddingEquiv (K : Type u_1) [Field K] [NumberField K] : Additive ((RingOfIntegers K)ˣ ⧸ torsion K) ≃ₗ[ℤ] ↥(unitLattice K)

The linear equivalence between (𝓞 K)ˣ ⧸ (torsion K) as an additive ℤ-module and unitLattice .

@[simp]

theorem NumberField.Units.logEmbeddingEquiv_apply (K : Type u_1) [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) : ↑((logEmbeddingEquiv K) (Additive.ofMul ↑x)) = (logEmbedding K) (Additive.ofMul x)

instance NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] : Module.Free ℤ (Additive ((RingOfIntegers K)ˣ ⧸ torsion K))

instance NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion (K : Type u_1) [Field K] [NumberField K] : Module.Finite ℤ (Additive ((RingOfIntegers K)ˣ ⧸ torsion K))

instance NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers (K : Type u_1) [Field K] [NumberField K] : Module.Finite ℤ (Additive (RingOfIntegers K)ˣ)

instance NumberField.Units.instFGUnitsRingOfIntegers (K : Type u_1) [Field K] [NumberField K] : Monoid.FG (RingOfIntegers K)ˣ

theorem NumberField.Units.rank_modTorsion (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℤ (Additive ((RingOfIntegers K)ˣ ⧸ torsion K)) = rank K

def NumberField.Units.basisModTorsion (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Fin (rank K)) ℤ (Additive ((RingOfIntegers K)ˣ ⧸ torsion K))

A basis of the quotient (𝓞 K)ˣ ⧸ (torsion K) seen as an additive ℤ-module.

def NumberField.Units.basisUnitLattice (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Fin (rank K)) ℤ ↥(unitLattice K)

The basis of the unitLattice obtained by mapping basisModTorsion via logEmbedding.

def NumberField.Units.fundSystem (K : Type u_1) [Field K] [NumberField K] : Fin (rank K) → (RingOfIntegers K)ˣ

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

theorem NumberField.Units.fundSystem_mk (K : Type u_1) [Field K] [NumberField K] (i : Fin (rank K)) : Additive.ofMul ↑(fundSystem K i) = (basisModTorsion K) i

theorem NumberField.Units.logEmbedding_fundSystem (K : Type u_1) [Field K] [NumberField K] (i : Fin (rank K)) : (logEmbedding K) (Additive.ofMul (fundSystem K i)) = ↑((basisUnitLattice K) i)

theorem NumberField.Units.fun_eq_repr (K : Type u_1) [Field K] [NumberField K] {x ζ : (RingOfIntegers K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K) (h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i) : f = ⇑((basisModTorsion K).repr (Additive.ofMul ↑x))

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.

theorem NumberField.Units.exist_unique_eq_mul_prod (K : Type u_1) [Field K] [NumberField K] (x : (RingOfIntegers K)ˣ) : ∃! ζe : ↥(torsion K) × (Fin (rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i

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.