The S-unit lattice #
Let S be a finite set of finite places of a number field K. The image of the S-logarithmic
embedding TauCeti.NumberField.SUnit.logEmbedding S is the S-unit lattice
TauCeti.NumberField.SUnit.unitLattice S. This file proves that it is a full ℤ-lattice in the
S-logarithmic space, of rank NumberField.Units.rank K + #S, and identifies it with the
S-units modulo torsion. This is the S-analogue of Mathlib's NumberField.Units.unitLattice;
the covolume of this lattice is what one calls the S-regulator.
- Discreteness. A bounded
S-logarithmic image forces a bounded height, and a number field has only finitely many elements of bounded height (Northcott's theorem,NumberField.finite_setOfPred_logHeight₁_le). - Spanning. The ordinary units fill the infinite coordinates, by Mathlib's
NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top. For eachv ∈ S, raisingvto the class number gives a principal ideal, and a generator is anS-unit whose finite coordinates vanish except atv. - The quotient. The kernel of the
S-logarithmic embedding is the torsion (TauCeti.NumberField.SUnit.logEmbedding_ker), so the embedding induces aℤ-linear equivalence from theS-units modulo torsion onto the lattice.
Main definitions and results #
TauCeti.NumberField.SUnit.unitLattice: the image of theS-logarithmic embedding.TauCeti.NumberField.SUnit.unitLattice_inter_ball_finite: the lattice meets every ball in a finite set.TauCeti.NumberField.SUnit.unitLattice_span_eq_top: the lattice spans theS-logarithmic space.TauCeti.NumberField.SUnit.unitLattice_rank: the lattice has rankNumberField.Units.rank K + #S.TauCeti.NumberField.SUnit.logEmbeddingEquiv: the equivalence from theS-units modulo torsion onto the lattice.TauCeti.NumberField.SUnit.unitLattice_rank_eq_finrank_unit: the lattice has the same rank as the group ofS-units.TauCeti.NumberField.SUnit.basisUnitLattice: the basis of the lattice given by theS-logarithmic images of the chosen fundamental system ofS-units.TauCeti.NumberField.SUnit.isFundSystem_iff_exists_basis: a family ofS-units is a fundamental system exactly when itsS-logarithmic images form a basis of the lattice, andTauCeti.NumberField.SUnit.basisOfIsFundSystemis that basis.TauCeti.NumberField.SUnit.exists_forall_abs_log_sub_le: every vector of logarithms at the infinite places and the places ofSsumming to0lies within a bounded distance, depending only onKandS, of the logarithms of anS-unit.
References #
- E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006, Theorem 1.5.13.
The S-unit lattice: the image of the S-logarithmic embedding, as a ℤ-submodule of the
S-logarithmic space.
Instances For
A vector lies in the S-unit lattice exactly when it is the S-logarithmic image of an
S-unit.
The S-logarithmic image of an S-unit lies in the S-unit lattice.
Discreteness #
The S-unit lattice meets every closed ball in a finite set.
The S-unit lattice is discrete.
Spanning #
The S-unit lattice spans the S-logarithmic space over ℝ.
The S-unit lattice is a full ℤ-lattice in the S-logarithmic space.
The S-logarithmic space has dimension NumberField.Units.rank K + #S.
The S-unit lattice has rank NumberField.Units.rank K + #S.
The S-units modulo torsion #
The kernel of the S-logarithmic embedding, as a ℤ-linear map, is the torsion submodule of
the S-units.
The S-logarithmic embedding induces a ℤ-linear equivalence from the S-units modulo
torsion onto the S-unit lattice. This is the S-analogue of Mathlib's
NumberField.Units.logEmbeddingEquiv.
Instances For
The class of an S-unit modulo torsion is sent to its S-logarithmic image.
The S-unit lattice has the same rank as the group of S-units: quotienting by torsion keeps
the ℤ-rank, and logEmbeddingEquiv identifies the quotient with the lattice. With
unitLattice_rank this computes the rank of the S-units through the lattice, in agreement with
Dirichlet's S-unit theorem TauCeti.finrank_sUnits_numberField.
The basis of the S-unit lattice formed by the S-logarithmic images of the fundamental
system TauCeti.NumberField.SUnit.fundSystem. This is the S-analogue of Mathlib's
NumberField.Units.basisUnitLattice.
Instances For
The S-logarithmic image of the i-th fundamental S-unit is the i-th vector of
basisUnitLattice S. This is the S-analogue of Mathlib's
NumberField.Units.logEmbedding_fundSystem.
Fundamental systems and bases of the lattice #
The basis of the S-unit lattice formed by the S-logarithmic images of a fundamental
system of S-units. This is the S-analogue of Mathlib's NumberField.Units.basisOfIsMaxRank,
with ℤ in place of ℝ.
Instances For
The i-th vector of basisOfIsFundSystem hε is the S-logarithmic image of ε i.
A family of S-units is a fundamental system exactly when its S-logarithmic images form a
ℤ-basis of the S-unit lattice.
Approximating a sum-zero vector by the logarithms of an S-unit #
Every sum-zero vector of logarithms lies within bounded distance of the logarithms of an
S-unit. There is R ≥ 0, depending only on K and S, such that for all real numbers
z w at the infinite places and z' v at the places v ∈ S with total sum 0, some S-unit
u has |mult w * log (w u) - z w| ≤ R at every infinite place w and
|log ‖u‖_v - z' v| ≤ R at every v ∈ S.
This is the cocompactness of the S-unit lattice: the vector of the z with the coordinate at
w₀ omitted is within the diameter of a fundamental parallelepiped of a lattice vector, and the
omitted coordinates agree up to the sum of the others because both vectors sum to 0. The
sum-zero hypothesis is needed, since the weighted logarithms of an S-unit always sum to 0
(TauCeti.NumberField.SUnit.sum_mult_mul_log_add_sum_log_finitePlace).