Evaluating and bounding the regulator #
In unit rank zero the regulator is evaluated exactly. When the unit rank is zero (equivalently,
there is a single infinite place, so the field is ℚ or imaginary quadratic), the unit lattice
lives in the zero-dimensional log space, and its covolume is the empty determinant 1
(NumberField.Units.regulator_eq_one_of_rank_eq_zero). Mathlib defines the regulator and proves
it positive (NumberField.Units.regulator_pos) but does not evaluate it in the rank-zero case.
For a number field of unit rank one, a unit generating the units modulo torsion computes the
regulator at any infinite place w as w.mult * |Real.log (w u)|. In particular, at a place
where 1 < w u, the absolute value can be removed. The multiplicity is essential at a complex
place.
The more general index formula also applies to a unit which does not generate modulo torsion.
It compares its weighted logarithm with the regulator times the subgroup index, using Mathlib's
NumberField.Units.regOfFamily_div_regulator and NumberField.Units.regOfFamily_eq_det.
In rank one, the norm of a unit's logarithmic embedding equals its weighted absolute logarithm at any infinite place. This identifies norm comparisons with logarithm comparisons at a chosen place. The product formula over the two infinite places also forces a unit expanding at one of them to contract at the other, which controls the remaining conjugates of a unit bounded at a chosen place.
In every rank, Hadamard's ℓ¹ bound Matrix.abs_det_le_prod_sum_abs bounds the regulator of a
family of units by the product of the ℓ¹ norms of their logarithmic embeddings
(TauCeti.NumberField.Units.regOfFamily_le_prod_sum_abs_logEmbedding), and hence by the product
of the full sums ∑ w, mult w * |log (w u)| over all infinite places
(TauCeti.NumberField.Units.regOfFamily_le_prod_sum_mult_mul_abs_log). A family has the
regulator of K as its regulator exactly when it generates the units modulo torsion
(TauCeti.NumberField.Units.regOfFamily_eq_regulator_iff), so the same products bound
regulator K for every fundamental system. By the product formula, the full sum for a unit is
twice its logarithmic height, so these bounds are the input to the upper bound of the regulator
by the heights of a fundamental system (Bugeaud–Győry, Lemma 1).
For a family u of maximal rank, the exponents of x = ζ * ∏ j, u j ^ e j with ζ a root of
unity are the coordinates of the logarithmic embedding of x on the basis basisOfIsMaxRank
(TauCeti.NumberField.Units.basisOfIsMaxRank_repr_logEmbedding). This extends Mathlib's
NumberField.Units.fun_eq_repr from the fundamental system to any family of maximal rank.
References #
- H. Cohen, A Course in Computational Algebraic Number Theory, §5.7.
- Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, Lemma 1.
The regulator of a number field of unit rank zero is 1. When the unit rank is zero,
the unit lattice sits inside the zero-dimensional log space, and the regulator, its covolume,
is the determinant of an empty matrix.
The regulator of ℚ is 1. The rational field has rank zero, so its regulator is the
empty determinant.
The regulator of an imaginary quadratic field is 1, the rank-zero case on a
degree-two totally complex field.
At unit rank one, the regulator of the constant one-unit family is its weighted absolute logarithm at any infinite place. This includes torsion units, for which both sides vanish.
In unit rank one, the weighted absolute logarithm of a unit is the regulator multiplied by the index of the subgroup generated by that unit and torsion.
In unit rank one, the norm of a unit's logarithmic embedding equals its weighted absolute logarithm at every infinite place. This evaluates an intrinsic norm at any chosen place.
In unit rank one, a unit whose absolute value exceeds one at an infinite place has absolute value less than one at the other infinite place.
In unit rank one, a positive real value of a unit in (1, B] bounds the norm of its
logarithmic embedding by log B.
At a place where u has absolute value greater than one, comparing log-embedding norms
amounts to comparing the absolute logarithm of v with the logarithm of u at that place.
A generator modulo torsion in unit rank one evaluates the regulator at any infinite place. No choice of a sign or of an inverse for the generator is needed.
At a place where a generator modulo torsion has absolute value greater than one, its weighted logarithm is the rank-one regulator.
A family of units has the regulator of K as its regulator if and only if it generates the
units modulo torsion.
If u has maximal rank and x = ζ * ∏ j, u j ^ e j with ζ a root of unity, then the
exponents e j are the coordinates of the logarithmic embedding of x on the basis
basisOfIsMaxRank.
Hadamard's bound for the regulator of a family. The regulator of a family of units is at
most the product of the ℓ¹ norms of their logarithmic embeddings.
Hadamard's bound for the regulator of a family, over all places. The regulator of a family of units is at most the product, over the family, of the sums of the weighted absolute logarithms at all infinite places.
Hadamard's bound for the regulator. For every fundamental system of units ε, the
regulator of K is at most the product of the ℓ¹ norms of their logarithmic embeddings.
Hadamard's bound for the regulator, over all places. For every fundamental system of
units ε, the regulator of K is at most the product, over the system, of the sums of the
weighted absolute logarithms at all infinite places.
In a number field of unit rank one, the norm of the logarithmic embedding of a unit v is the
index of ⟨v⟩ ⊔ torsion in the unit group times the regulator.