Certifying a generator of the units modulo torsion in rank one #
For a number field of unit rank one, a non-torsion unit generates the unit group modulo torsion exactly when no unit has a smaller nonzero logarithmic embedding. The statement uses Mathlib's logarithmic embedding and torsion subgroup. It turns the generation condition used in the rank-one regulator formula into a minimality test on units.
The criterion makes the abstract generation condition testable through logarithmic norms.
The placewise comparison in Units.Regulator.Basic expresses these norms as weighted logarithms
at a chosen infinite place.
Main results #
TauCeti.NumberField.Units.generates_mod_torsion_iff_no_smaller_logEmbedding: the rank-one generator criterion.
References #
- H. Cohen, A Course in Computational Algebraic Number Theory, §5.7.
theorem
TauCeti.NumberField.Units.generates_mod_torsion_iff_no_smaller_logEmbedding
{K : Type u_1}
[Field K]
[NumberField K]
(hr : NumberField.Units.rank K = 1)
(u : (NumberField.RingOfIntegers K)ˣ)
(hu : u ∉ NumberField.Units.torsion K)
:
Subgroup.closure {u} ⊔ NumberField.Units.torsion K = ⊤ ↔ ¬∃ (v : (NumberField.RingOfIntegers K)ˣ),
0 < ‖(NumberField.Units.logEmbedding K) (Additive.ofMul v)‖ ∧ ‖(NumberField.Units.logEmbedding K) (Additive.ofMul v)‖ < ‖(NumberField.Units.logEmbedding K) (Additive.ofMul u)‖
A non-torsion unit in a rank-one number field generates all units modulo torsion exactly when there is no unit with a strictly smaller nonzero logarithmic embedding.