Bounding the regulator by heights

Hadamard's inequality bounds the regulator of any family of units by the product of twice their relative logarithmic heights. For a fundamental system this bounds the field regulator. In absolute logarithmic height the constant is (2 * [K : ℚ]) ^ rank K, as in Bugeaud–Győry, Lemma 1. In particular, the product of the heights of any fundamental system is positive, including in rank zero, when the product is empty and equals one.

The estimates combine the determinant bounds in Regulator.Basic with the comparison between height and the ℓ¹ norm of the logarithmic embedding in Units.Log.Embedding.

In unit rank one the comparison is an identity. The two infinite places contribute equally to the height of a unit, so the relative logarithmic height of a fundamental unit is the regulator, and its absolute logarithmic height is regulator K / [K : ℚ]. Hence, at rank K = 1, the constant (r!)² / (2 ^ (r - 1) d ^ r) = 1 / d of Bugeaud–Győry's lower bound for the regulator by the heights of a reduced fundamental system is attained by every fundamental unit.

For Mathlib's canonical fundSystem K, positivity specializes to prod_absLogHeight₁_pos (closure_fundSystem_sup_torsion_eq_top (K := K)). Both this specialization and the regulator bounds are available from the present module.

References

• Y. Bugeaud and K. Győry, Bounds for the solutions of unit equations, Acta Arith. 74 (1996), 67–80, §3, Lemma 1 (the case of the infinite places).

theorem TauCeti.NumberField.Units.regOfFamily_le_prod_logHeight₁ {K : Type u_1} [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) : NumberField.Units.regOfFamily u ≤ 2 ^ NumberField.Units.rank K * ∏ i : Fin (NumberField.Units.rank K), Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u i))

Hadamard's bound for any family of units, in relative logarithmic height. No generation or independence hypothesis is needed.

theorem TauCeti.NumberField.Units.regOfFamily_le_prod_absLogHeight₁ {K : Type u_1} [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) : NumberField.Units.regOfFamily u ≤ (2 * ↑(Module.finrank ℚ K)) ^ NumberField.Units.rank K * ∏ i : Fin (NumberField.Units.rank K), NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u i))

Hadamard's bound for any family of units, in absolute logarithmic height. The degree factor converts each relative height into an absolute height.

theorem TauCeti.NumberField.Units.regulator_le_prod_logHeight₁ {K : Type u_1} [Field K] [NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) : NumberField.Units.regulator K ≤ 2 ^ NumberField.Units.rank K * ∏ i : Fin (NumberField.Units.rank K), Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i))

Every fundamental system bounds the field regulator by 2 ^ rank K times the product of its relative logarithmic heights.

theorem TauCeti.NumberField.Units.regulator_le_prod_absLogHeight₁ {K : Type u_1} [Field K] [NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) : NumberField.Units.regulator K ≤ (2 * ↑(Module.finrank ℚ K)) ^ NumberField.Units.rank K * ∏ i : Fin (NumberField.Units.rank K), NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i))

Every fundamental system bounds the field regulator by (2d) ^ r times the product of its absolute logarithmic heights, where d is the degree and r the unit rank.

theorem TauCeti.NumberField.Units.prod_absLogHeight₁_pos {K : Type u_1} [Field K] [NumberField K] {ε : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hε : Subgroup.closure (Set.range ε) ⊔ NumberField.Units.torsion K = ⊤) : 0 < ∏ i : Fin (NumberField.Units.rank K), NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑(ε i))

The product of the absolute logarithmic heights of any fundamental system is positive. This includes rank zero, when the product is one.

Unit rank one

theorem TauCeti.NumberField.Units.logHeight₁_eq_index_mul_regulator {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) (u : (NumberField.RingOfIntegers K)ˣ) : Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) = ↑(Subgroup.closure {u} ⊔ NumberField.Units.torsion K).index * NumberField.Units.regulator K

In unit rank one, the relative logarithmic height of a unit is the index of the subgroup it generates together with the torsion, times the regulator.

theorem TauCeti.NumberField.Units.absLogHeight₁_eq_index_mul_regulator_div_finrank {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) (u : (NumberField.RingOfIntegers K)ˣ) : NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) = ↑(Subgroup.closure {u} ⊔ NumberField.Units.torsion K).index * NumberField.Units.regulator K / ↑(Module.finrank ℚ K)

In unit rank one, the absolute logarithmic height of a unit is its index times the regulator, divided by the degree.

theorem TauCeti.NumberField.Units.logHeight₁_eq_regulator_of_rank_eq_one {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) {ε : (NumberField.RingOfIntegers K)ˣ} (hε : Subgroup.closure {ε} ⊔ NumberField.Units.torsion K = ⊤) : Height.logHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε) = NumberField.Units.regulator K

In unit rank one, the relative logarithmic height of a fundamental unit is the regulator.

theorem TauCeti.NumberField.Units.absLogHeight₁_eq_regulator_div_finrank_of_rank_eq_one {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) {ε : (NumberField.RingOfIntegers K)ˣ} (hε : Subgroup.closure {ε} ⊔ NumberField.Units.torsion K = ⊤) : NumberField.absLogHeight₁ ((algebraMap (NumberField.RingOfIntegers K) K) ↑ε) = NumberField.Units.regulator K / ↑(Module.finrank ℚ K)

In unit rank one, the absolute logarithmic height of a fundamental unit is the regulator divided by the degree.