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 fieldK.NumberField.Units.fundSystem: a fundamental system of units ofK.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 tocard (InfinitePlace K) - 1.NumberField.Units.exist_unique_eq_mul_prod: Dirichlet Unit Theorem. Any unit ofπ Kcan be written uniquely as the product of a root of unity and powers of the units of the fundamental systemfundSystem.
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
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
The lattice formed by the image of the logarithmic embedding.
Equations
- NumberField.Units.unitLattice K = Submodule.map (NumberField.Units.logEmbedding K).toIntLinearMap β€
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).
This result shows that there always exists a next term in the sequence.
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, β―β©
Instances For
The terms of the sequence are nonzero.
The sequence is strictly decreasing at infinite places distinct from wβ.
The terms of the sequence have norm bounded by B.
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.
The unit rank of the number field K, it is equal to card (InfinitePlace K) - 1.
Equations
Instances For
Equations
- β― = β―
Equations
- β― = β―
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
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 β―
Instances For
Equations
- β― = β―
Equations
- β― = β―
Equations
- β― = β―
Equations
- β― = β―
A basis of the quotient (π K)Λ£ β§Έ (torsion K) seen as an additive β€-module.
Equations
Instances For
The basis of the unitLattice obtained by mapping basisModTorsion via logEmbedding.
Equations
Instances For
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))
Instances For
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.