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.

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

The distinguished infinite place.

Equations

• NumberField.Units.dirichletUnitTheorem.w₀ = ⋯.some

def NumberField.Units.logEmbedding (K : Type u_1) [Field K] [NumberField K] : Additive (NumberField.RingOfIntegers K)ˣ →+ { w : NumberField.InfinitePlace K // 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.

@[simp]

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

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

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

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

theorem NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le {K : Type u_1} [Field K] [NumberField K] {r : ℝ} {x : (NumberField.RingOfIntegers K)ˣ} (hr : 0 ≤ r) (h : ‖(NumberField.Units.logEmbedding K) x‖ ≤ r) (w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : |(NumberField.Units.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 : (NumberField.RingOfIntegers K)ˣ} (hr : 0 ≤ r) (h : ‖(NumberField.Units.logEmbedding K) (Additive.ofMul x)‖ ≤ r) (w : NumberField.InfinitePlace K) : |Real.log (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x))| ≤ ↑(Fintype.card (NumberField.InfinitePlace K)) * r

noncomputable def NumberField.Units.unitLattice (K : Type u_1) [Field K] [NumberField K] : Submodule ℤ ({ w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℝ)

The lattice formed by the image of the logarithmic embedding.

Equations

• NumberField.Units.unitLattice K = Submodule.map (NumberField.Units.logEmbedding K).toIntLinearMap ⊤

theorem NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite (K : Type u_1) [Field K] [NumberField K] (r : ℝ) : (↑(NumberField.Units.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₁ : NumberField.InfinitePlace K) {B : ℕ} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) {x : NumberField.RingOfIntegers K} (hx : x ≠ 0) : ∃ (y : NumberField.RingOfIntegers K), y ≠ 0 ∧ (∀ (w : NumberField.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₁ : NumberField.InfinitePlace K) {B : ℕ} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) : ℕ → { x : NumberField.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.

Equations

• NumberField.Units.dirichletUnitTheorem.seq K w₁ hB 0 = ⟨1, ⋯⟩
• NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n.succ = ⟨⋯.choose, ⋯⟩

theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero (K : Type u_1) [Field K] [NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : ℕ) : (algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.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₁ : NumberField.InfinitePlace K) {B : ℕ} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) {n m : ℕ} (h : n < m) (w : NumberField.InfinitePlace K) (hw : w ≠ w₁) : w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB m)) < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.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₁ : NumberField.InfinitePlace K) {B : ℕ} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) (n : ℕ) : ((Algebra.norm ℤ) ↑(NumberField.Units.dirichletUnitTheorem.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₁ : NumberField.InfinitePlace K) : ∃ (u : (NumberField.RingOfIntegers K)ˣ), ∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (NumberField.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 ℝ ↑(NumberField.Units.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.

Equations

• NumberField.Units.rank K = Fintype.card (NumberField.InfinitePlace K) - 1

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem NumberField.Units.finrank_eq_rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℝ ({ w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℝ) = NumberField.Units.rank K

@[simp]

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

def NumberField.Units.logEmbeddingQuot (K : Type u_1) [Field K] [NumberField K] : Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K) →+ { w : NumberField.InfinitePlace K // 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.

@[simp]

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

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

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

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

Equations

• NumberField.Units.logEmbeddingEquiv K = LinearEquiv.ofBijective ((NumberField.Units.logEmbeddingQuot K).codRestrict (NumberField.Units.unitLattice K) ⋯).toIntLinearMap ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• NumberField.Units.basisModTorsion K = (Module.Free.chooseBasis ℤ (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))).reindex (Fintype.equivOfCardEq ⋯)

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

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

Equations

• NumberField.Units.basisUnitLattice K = (NumberField.Units.basisModTorsion K).map (NumberField.Units.logEmbeddingEquiv K)

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

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

Equations

• NumberField.Units.fundSystem K i = Quotient.out (Additive.toMul ((NumberField.Units.basisModTorsion K) i))

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

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

theorem NumberField.Units.fun_eq_repr (K : Type u_1) [Field K] [NumberField K] {x ζ : (NumberField.RingOfIntegers K)ˣ} {f : Fin (NumberField.Units.rank K) → ℤ} (hζ : ζ ∈ NumberField.Units.torsion K) (h : x = ζ * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ f i) : f = ⇑((NumberField.Units.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 : (NumberField.RingOfIntegers K)ˣ) : ∃! ζe : ↥(NumberField.Units.torsion K) × (Fin (NumberField.Units.rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.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.