Fundamental systems of units of bounded height #
A family of units ε of a number field K is a fundamental system when, together with the
torsion subgroup, it generates the units: Subgroup.closure (Set.range ε) ⊔ torsion K = ⊤. This
happens exactly when the logarithmic embeddings of the ε i span the unit lattice over ℤ, so
every ℤ-basis of the unit lattice lifts to a fundamental system.
A family u of rank K units with linearly independent logarithmic embeddings need not be a
fundamental system: it may generate a subgroup of finite index greater than one. Cassels' basis
lemma, applied to the unit lattice and the ℓ¹ unit ball of the logarithmic space, replaces u
by a fundamental system ε whose logarithmic embeddings are almost as short in the ℓ¹ norm.
When the ℓ¹ norms of the u j increase with j, the j-th member of ε is at most
max 1 ((j + 1) / 2) times as long as u j (ZLattice.exists_basis_gauge_le_max_one_mul), so
the product of the norms grows at most by r! / 2 ^ (r - 1), where r = rank K. The height of a
unit is bounded by the ℓ¹ norm of its logarithmic embedding, so this bounds the product of the
heights of ε by r! / 2 ^ (r - 1) times the product of the ℓ¹ norms of the u j. That
product does not depend on the order of the u j, so after sorting u by ℓ¹ norm the product
bounds hold for every independent family.
Units realizing the successive minima of the unit lattice with respect to the ℓ¹ ball are
independent, and Minkowski's second theorem bounds the product of their ℓ¹ norms by
r! * regulator K, since the ℓ¹ ball has volume 2 ^ r / r!. For such u the product bound
becomes Bugeaud and Győry's reduced fundamental system,
∏ i, absLogHeight₁ (ε i) ≤ (r!) ^ 2 / (2 ^ (r - 1) * [K : ℚ] ^ r) * regulator K. Hadamard's
bound TauCeti.NumberField.Units.regulator_le_prod_absLogHeight₁ holds for every fundamental
system, so this ε satisfies both bounds.
Main results #
TauCeti.NumberField.Units.span_logEmbedding_eq_unitLattice_iff: a family of units is a fundamental system exactly when its logarithmic embeddings span the unit lattice.TauCeti.NumberField.Units.closure_sup_torsion_eq_top_of_basis: units whose logarithmic embeddings form aℤ-basis of the unit lattice are a fundamental system.TauCeti.NumberField.Units.exists_fundSystem_sum_abs_logEmbedding_le_max_one_mul: a fundamental system whosej-th member hasℓ¹norm at mostmax 1 ((j + 1) / 2)times that of thej-th member of a given independent family with increasingℓ¹norms.TauCeti.NumberField.Units.exists_fundSystem_prod_logHeight₁_le_of_isMaxRankandTauCeti.NumberField.Units.exists_fundSystem_prod_absLogHeight₁_le_of_isMaxRank: the resulting bounds for the product of the heights of the fundamental system.TauCeti.NumberField.Units.exists_isMaxRank_prod_sum_abs_logEmbedding_le: Minkowski's second theorem for the unit lattice and theℓ¹ball, giving independent units whoseℓ¹norms have product at mostr! * regulator K.TauCeti.NumberField.Units.exists_fundSystem_prod_logHeight₁_leandTauCeti.NumberField.Units.exists_fundSystem_prod_absLogHeight₁_le: a reduced fundamental system, whose product of heights is bounded by the regulator.
References #
- J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter V, Lemma 8.
- Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, Lemma 1.
- J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter VIII (Minkowski's second theorem).
The construction follows Ralf Stephan's Apache-2.0 formalization in rwst/Subspace-Theorems
(ArithmeticHeights/Regulator.lean, the lemma closure_sup_torsion_eq_top_of_span and the proof
of exists_fundSystem_prod_absLogHeight₁_le).
Fundamental systems and bases of the unit lattice #
A family of units generates the units together with the torsion subgroup exactly when the
logarithmic embeddings of its members span the unit lattice over ℤ.
Units whose logarithmic embeddings form a ℤ-basis of the unit lattice generate the units
together with the torsion subgroup.
Fundamental systems of controlled ℓ¹ norm #
A fundamental system from an increasing independent family of units. If the logarithmic
embeddings of u 0, …, u (r - 1) are linearly independent and their ℓ¹ norms increase, as
they do for units realizing the successive minima of the unit lattice with respect to the ℓ¹
ball, some fundamental system ε satisfies ‖log ε j‖₁ ≤ max 1 ((j + 1) / 2) * ‖log u j‖₁ for
every j.
Fundamental systems of controlled height #
A fundamental system of controlled height. If the logarithmic embeddings of
u 0, …, u (r - 1) are linearly independent, where r = rank K, some fundamental system ε has
∏ i, logHeight₁ (ε i) ≤ r! / 2 ^ (r - 1) * ∏ i, ‖log u i‖₁, where ‖log x‖₁ is the ℓ¹ norm
of the logarithmic embedding of x.
A fundamental system of controlled absolute height. If the logarithmic embeddings of
u 0, …, u (r - 1) are linearly independent, where r = rank K, some fundamental system ε
has ∏ i, absLogHeight₁ (ε i) ≤ r! / (2 ^ (r - 1) * [K : ℚ] ^ r) * ∏ i, ‖log u i‖₁, where
‖log x‖₁ is the ℓ¹ norm of the logarithmic embedding of x.
Reduced fundamental systems #
Minkowski's second theorem for the unit lattice. There are units u 0, …, u (r - 1), where
r = rank K, with linearly independent logarithmic embeddings and
∏ i, ‖log u i‖₁ ≤ r! * regulator K, where ‖log x‖₁ is the ℓ¹ norm of the logarithmic
embedding of x. This is Minkowski's second theorem for the unit lattice and the ℓ¹ unit ball
logBall K, whose volume is 2 ^ r / r!.
A reduced fundamental system (Bugeaud–Győry). Some fundamental system ε of units has
∏ i, logHeight₁ (ε i) ≤ (r!) ^ 2 / 2 ^ (r - 1) * regulator K, where r = rank K.
A reduced fundamental system (Bugeaud–Győry, Lemma 1). Some fundamental system ε of
units has ∏ i, absLogHeight₁ (ε i) ≤ (r!) ^ 2 / (2 ^ (r - 1) * [K : ℚ] ^ r) * regulator K, where
r = rank K. The constant is attained for ℚ(√2). By Hadamard's bound
regulator_le_prod_absLogHeight₁, every fundamental system also has
regulator K ≤ (2 * [K : ℚ]) ^ r * ∏ i, absLogHeight₁ (ε i).