Heights of S-units and the kernel of the S-logarithmic embedding #
Let S be a finite set of finite places of a number field K. The S-logarithmic embedding
TauCeti.NumberField.SUnit.logEmbedding S records the weighted logarithms of an S-unit at the
infinite places other than Mathlib's distinguished place w₀, and its logarithms at the places
of S. The vector of all weighted logarithms of an S-unit, over S and every infinite place,
has ℓ¹ norm twice the logarithmic height, and the product formula recovers the omitted
coordinate at w₀ as minus the sum of the kept ones. Hence
2 * logHeight₁ x = ∑ i, |logEmbedding S x i| + |∑ i, logEmbedding S x i|,
which compares the height of an S-unit with the ℓ¹ and supremum norms of its image.
As a consequence the kernel of the S-logarithmic embedding is the torsion subgroup of the
S-units: an S-unit with vanishing image has height zero, and by Kronecker's theorem an element
of height zero is a root of unity. This is the S-analogue of Mathlib's
NumberField.Units.dirichletUnitTheorem.logEmbedding_ker. By the first isomorphism theorem, the
S-logarithmic embedding is therefore injective on the quotient of the S-units by torsion.
Main results #
TauCeti.NumberField.SUnit.two_mul_logHeight₁_eq_sum_abs_logEmbedding: the height of anS-unit in terms of itsS-logarithmic embedding.TauCeti.NumberField.SUnit.sum_abs_logEmbedding_le_two_mul_logHeight₁andTauCeti.NumberField.SUnit.logHeight₁_le_sum_abs_logEmbedding: the two-sidedℓ¹comparison.TauCeti.NumberField.SUnit.norm_logEmbedding_le_logHeight₁andTauCeti.NumberField.SUnit.logHeight₁_le_mul_norm_logEmbedding: the supremum-norm comparison.TauCeti.NumberField.SUnit.logHeight₁_eq_zero_iff: anS-unit has height zero exactly when it is torsion.TauCeti.NumberField.SUnit.logEmbedding_eq_zero_iffandTauCeti.NumberField.SUnit.logEmbedding_ker: the kernel of theS-logarithmic embedding is the torsion subgroup of theS-units.TauCeti.NumberField.SUnit.mul_prod_zpow_ne_zero_and_adicAbv_eq_one: a root of unity times a product of integer powers of elements with absolute value1outsideSis nonzero and has absolute value1outsideS.
References #
- E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press, 2006,
§1.5 (Kronecker's theorem 1.5.9 and the
S-unit theorem 1.5.13). - Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, formula (12).
Height zero and torsion #
An S-unit has multiplicative height one exactly when it is torsion.
An S-unit has logarithmic height zero exactly when it is torsion.
Closure under torsion and integer powers #
A root of unity times a product of integer powers of nonzero elements γ i that have absolute
value 1 at every finite place outside S is nonzero and has absolute value 1 at every finite
place outside S.
The height in S-logarithmic coordinates #
Twice the logarithmic height of an S-unit is the ℓ¹ norm of its S-logarithmic
embedding plus the absolute value of the omitted coordinate, which is the absolute value of the
sum of the kept coordinates.
The ℓ¹ norm of the S-logarithmic embedding of an S-unit is at most twice its
logarithmic height.
The logarithmic height of an S-unit is at most the ℓ¹ norm of its S-logarithmic
embedding.
The supremum norm of the S-logarithmic embedding of an S-unit is at most its logarithmic
height.
The logarithmic height of an S-unit is at most rank K + #S, the dimension of the
S-logarithmic space, times the supremum norm of its S-logarithmic embedding.
The kernel #
The logarithmic height of an S-unit vanishes exactly when its S-logarithmic embedding
does.
An S-unit lies in the kernel of the S-logarithmic embedding exactly when it is torsion.
This is the S-analogue of NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff.
The S-logarithmic image of ζ * ∏ j, γ j ^ z j, for ζ torsion, is
∑ j, z j • ℓ(γ j).
The kernel of the S-logarithmic embedding is the torsion subgroup of the S-units. This is
the S-analogue of NumberField.Units.dirichletUnitTheorem.logEmbedding_ker.