The house of an algebraic number

The house ⌈x⌉ of an element x of a field of characteristic zero is the largest absolute value of a complex root of minpoly ℚ x, that is, the largest modulus of a complex conjugate of x. The value at a transcendental element is 0.

Mathlib's NumberField.house is the same quantity for an element of a fixed number field, computed through its complex embeddings. The version here needs neither a number field nor a complex embedding of the ambient field: only minpoly ℚ x is mapped to ℂ. It is therefore constant on conjugacy classes and invariant under field embeddings, and it agrees with NumberField.house on number fields (TauCeti.house_eq_numberField_house). The sub-multiplicativity and sub-additivity of the house for algebraic elements are obtained by computing in the number field generated by the elements involved.

Together with the naive height and the Mahler measure, the house controls the size of the conjugates of an algebraic number. It enters Liouville-type lower bounds, the bound of the naive height of an algebraic integer by a power of its house, and the finiteness of algebraic integers of bounded degree and bounded house.

Main definitions

• TauCeti.house x: the largest modulus of a complex root of minpoly ℚ x.

Main results

• TauCeti.norm_le_house_of_mem_rootSet, TauCeti.house_le_iff, TauCeti.exists_mem_rootSet_norm_eq_house: the house is the maximum of the moduli of the complex conjugates; in particular ‖x‖ ≤ ⌈x⌉ for algebraic x ∈ ℂ (TauCeti.norm_le_house).
• TauCeti.house_eq_numberField_house: on a number field the house is NumberField.house.
• NumberField.house_le_exp_logHeight₁, NumberField.logHeight₁_le_finrank_mul_posLog_house: house x ≤ exp h(x) for the relative height h over a number field K, and conversely h(x) ≤ [K : ℚ] log⁺ (house x) for an algebraic integer x of K.
• TauCeti.house_map, TauCeti.house_eq_of_minpoly_eq: invariance under field embeddings and conjugation.
• TauCeti.house_mul_le, TauCeti.house_add_le, TauCeti.house_pow: the house is sub-multiplicative, sub-additive and multiplicative on powers.
• TauCeti.one_le_house, TauCeti.house_eq_one_iff: a nonzero algebraic integer has house at least 1, and Kronecker's theorem, an algebraic integer has house 1 exactly when it is a root of unity.
• TauCeti.exists_algEquiv_one_le_norm: a nonzero algebraic integer of a finite normal subfield L of ℂ has a Galois conjugate over ℚ of modulus at least 1.
• TauCeti.house_le_mahlerMeasure, TauCeti.mahlerMeasure_le_leadingCoeff_mul_max_one_house_pow: the comparisons ⌈x⌉ ≤ M(x) ≤ a₀ max(1, ⌈x⌉)ᵈ with the Mahler measure.
• TauCeti.naiveHeight_le_two_mul_pow_of_house_le, TauCeti.naiveHeight_le_two_mul_house_pow: an algebraic integer of degree d has naive height at most (2B)ᵈ whenever its house is at most B with 1 ≤ B; in particular a nonzero algebraic integer satisfies H(x) ≤ (2 ⌈x⌉)ᵈ.
• TauCeti.exists_numberField_of_isIntegral_natCast_mul: an element α with b α integral lies in the number field ℚ(α) of degree deg α, with the same house.
• NumberField.house_natCast_mul_pow_mul_pow_le: the house of c bⁿ αʲ in a number field is at most (2 b max(1, ⌈α⌉))ⁿ when c ≤ 2ⁿ and j ≤ n.
• NumberField.one_le_norm_mul_house_pow: Liouville's inequality, a nonzero algebraic integer x of a number field of degree d satisfies 1 ≤ ‖σ x‖ ⌈x⌉ᵈ⁻¹ for every complex embedding σ.
• NumberField.eq_zero_of_norm_le_exp_of_house_le_exp: Liouville's inequality in exponential form, an element y of a number field with m ^ N y integral is zero once ‖σ y‖, ⌈y⌉ and |m| ^ N are small enough.
• TauCeti.inv_norm_le_pow_mul_house_pow_of_mem_rootSet, TauCeti.inv_norm_le_natDenominator_pow_mul_house_pow_of_mem_rootSet, TauCeti.inv_norm_le_natDenominator_pow_mul_house_pow: every complex conjugate z of a nonzero algebraic number x of degree d satisfies ‖z‖ ≥ den(x)⁻ᵈ ⌈x⌉¹⁻ᵈ, and more generally ‖z‖ ≥ b⁻ᵈ ⌈x⌉¹⁻ᵈ whenever b x is integral for some positive integer b.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 3, §3.4 and Exercises 3.5, 3.6; ch. 3, Lemma 3.6, p. 42, for the Galois conjugate of modulus at least 1; ch. 3, Exercise 3.7, p. 60, for the lower bound ‖z‖ ≥ den(z)⁻ᵈ ⌈z⌉¹⁻ᵈ.
• C. Smyth, The Mahler measure of algebraic numbers: a survey (2008), §3.

noncomputable def TauCeti.house {F : Type u_1} [Field F] [CharZero F] (x : F) : ℝ

The house ⌈x⌉ of x: the largest modulus of a complex root of minpoly ℚ x, that is, of a complex conjugate of x. For transcendental x the minimal polynomial is 0, it has no roots, and the house is 0.

theorem TauCeti.house_def {F : Type u_1} [Field F] [CharZero F] (x : F) : house x = ⨆ (z : ↑((minpoly ℚ x).rootSet ℂ)), ‖↑z‖

The house of x is the supremum of the moduli of the complex roots of minpoly ℚ x.

theorem TauCeti.house_nonneg {F : Type u_1} [Field F] [CharZero F] (x : F) : 0 ≤ house x

The house is nonnegative.

theorem TauCeti.norm_le_house_of_mem_rootSet {F : Type u_1} [Field F] [CharZero F] {x : F} {z : ℂ} (hz : z ∈ (minpoly ℚ x).rootSet ℂ) : ‖z‖ ≤ house x

Every complex conjugate of x has modulus at most the house of x.

theorem TauCeti.norm_le_house {x : ℂ} (hx : IsAlgebraic ℚ x) : ‖x‖ ≤ house x

An algebraic complex number has modulus at most its house.

theorem TauCeti.house_le_iff {F : Type u_1} [Field F] [CharZero F] {x : F} {C : ℝ} (hC : 0 ≤ C) : house x ≤ C ↔ ∀ z ∈ (minpoly ℚ x).rootSet ℂ, ‖z‖ ≤ C

For C ≥ 0, the house of x is at most C exactly when every complex conjugate of x has modulus at most C.

theorem TauCeti.exists_mem_rootSet_norm_eq_house {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : ∃ z ∈ (minpoly ℚ x).rootSet ℂ, ‖z‖ = house x

The house of an algebraic element is attained: it is the modulus of some complex conjugate.

theorem TauCeti.house_eq_numberField_house {K : Type u_3} [Field K] [NumberField K] (x : K) : house x = NumberField.house x

On a number field, the house is Mathlib's NumberField.house: the largest modulus of the image of x under a complex embedding.

theorem NumberField.house_le_exp_logHeight₁ {K : Type u_3} [Field K] [NumberField K] (x : K) : house x ≤ Real.exp (Height.logHeight₁ x)

Every conjugate of a number-field element has modulus at most the exponential of its relative logarithmic height.

theorem NumberField.logHeight₁_le_finrank_mul_posLog_house {K : Type u_3} [Field K] [NumberField K] {x : K} (hx : IsIntegral ℤ x) : Height.logHeight₁ x ≤ ↑(Module.finrank ℚ K) * (house x).posLog

The relative logarithmic height of an algebraic integer x of a number field K is at most [K : ℚ] * log⁺ (house x). This is a converse to NumberField.house_le_exp_logHeight₁; the integrality hypothesis is needed, since 1 / 2 has house 1 / 2 but positive height.

theorem TauCeti.house_eq_of_minpoly_eq {F : Type u_1} [Field F] [CharZero F] {F' : Type u_2} [Field F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : house x = house y

The house depends only on minpoly ℚ x: conjugates, possibly lying in different fields, have equal house.

@[simp]

theorem TauCeti.house_map {F : Type u_1} [Field F] [CharZero F] {F' : Type u_2} [Field F'] [CharZero F'] (f : F →+* F') (x : F) : house (f x) = house x

Field embeddings preserve the house.

@[simp]

theorem TauCeti.house_of_not_isAlgebraic {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : ¬IsAlgebraic ℚ x) : house x = 0

Transcendental elements have house 0.

@[simp]

theorem TauCeti.house_ratCast {F : Type u_1} [Field F] [CharZero F] (q : ℚ) : house ↑q = |↑q|

The house of a rational number is its absolute value, independently of the field containing it.

@[simp]

theorem TauCeti.house_intCast {F : Type u_1} [Field F] [CharZero F] (n : ℤ) : house ↑n = |↑n|

The house of an integer is its absolute value.

@[simp]

theorem TauCeti.house_natCast {F : Type u_1} [Field F] [CharZero F] (n : ℕ) : house ↑n = ↑n

The house of a natural number is itself.

@[simp]

theorem TauCeti.house_zero {F : Type u_1} [Field F] [CharZero F] : house 0 = 0

The house of 0 is 0.

@[simp]

theorem TauCeti.house_one {F : Type u_1} [Field F] [CharZero F] : house 1 = 1

The house of 1 is 1.

theorem TauCeti.house_mul_le {F : Type u_1} [Field F] [CharZero F] {x y : F} (hx : IsAlgebraic ℚ x) (hy : IsAlgebraic ℚ y) : house (x * y) ≤ house x * house y

The house of a product of algebraic elements is at most the product of their houses.

theorem TauCeti.house_add_le {F : Type u_1} [Field F] [CharZero F] {x y : F} (hx : IsAlgebraic ℚ x) (hy : IsAlgebraic ℚ y) : house (x + y) ≤ house x + house y

The house of a sum of algebraic elements is at most the sum of their houses.

@[simp]

theorem TauCeti.house_pow {F : Type u_1} [Field F] [CharZero F] (x : F) (n : ℕ) : house (x ^ n) = house x ^ n

The house is multiplicative on powers. For transcendental x and n ≠ 0 both sides are 0.

theorem TauCeti.one_le_house {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) (h0 : x ≠ 0) : 1 ≤ house x

A nonzero algebraic integer has house at least 1.

theorem TauCeti.exists_algEquiv_one_le_norm {L : IntermediateField ℚ ℂ} [FiniteDimensional ℚ ↥L] [Normal ℚ ↥L] {x : ↥L} (hx : IsIntegral ℤ x) (h0 : x ≠ 0) : ∃ (τ : Gal(↥L/ℚ)), 1 ≤ ‖↑(τ x)‖

A Galois conjugate of modulus at least 1. A nonzero algebraic integer x of a finite normal subfield L of ℂ has a Galois conjugate τ x, for some τ ∈ Gal(L/ℚ), of modulus at least 1. This is the form of NumberField.exists_conjugate_one_le_norm for a field embedded in ℂ, with its complex embeddings replaced by its automorphisms.

theorem TauCeti.house_eq_one_iff {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) : house x = 1 ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Kronecker's theorem. An algebraic integer has house 1 exactly when it is a root of unity.

theorem TauCeti.house_le_mahlerMeasure {F : Type u_1} [Field F] [CharZero F] (x : F) : house x ≤ mahlerMeasure x

The house is at most the Mahler measure. For an algebraic x the largest conjugate modulus |z| is bounded by its factor max(1, |z|) of M(x) = a₀ ∏ max(1, |z|), and the other factors are at least 1; for transcendental x this reads 0 ≤ 1.

theorem TauCeti.mahlerMeasure_le_leadingCoeff_mul_max_one_house_pow {F : Type u_1} [Field F] [CharZero F] (x : F) : mahlerMeasure x ≤ ↑(primitiveMinpoly x).leadingCoeff * max 1 (house x) ^ (minpoly ℚ x).natDegree

The Mahler measure is at most a₀ max(1, ⌈x⌉)ᵈ, where a₀ is the leading coefficient of the primitive minimal polynomial and d the degree of x.

theorem TauCeti.naiveHeight_le_two_mul_pow_of_house_le {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) {B : ℝ} (hB : 1 ≤ B) (hxB : house x ≤ B) : naiveHeight x ≤ (2 * B) ^ (minpoly ℚ x).natDegree

An algebraic integer of degree d whose house is at most B, with 1 ≤ B, has naive height at most (2B)ᵈ.

theorem TauCeti.naiveHeight_le_two_mul_house_pow {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) (h0 : x ≠ 0) : naiveHeight x ≤ (2 * house x) ^ (minpoly ℚ x).natDegree

A nonzero algebraic integer x of degree d has naive height at most (2 ⌈x⌉)ᵈ.

theorem TauCeti.exists_numberField_of_isIntegral_natCast_mul {F : Type u_1} [Field F] [CharZero F] {α : F} {b : ℕ} (hb : b ≠ 0) (hbα : IsIntegral ℤ (↑b * α)) : ∃ (K : IntermediateField ℚ F) (x : NumberField ↥K) (α' : ↥K), (algebraMap (↥K) F) α' = α ∧ Module.finrank ℚ ↥K = (minpoly ℚ α).natDegree ∧ IsIntegral ℤ (↑b * α') ∧ NumberField.house α' = house α

An element α of F such that b α is integral over ℤ for some b ≠ 0 lies in an intermediate number field K of degree deg α, namely ℚ(α): there is α' ∈ K mapping to α such that b α' is integral and house α' = house α. This reduces the construction of auxiliary polynomials for such α to Siegel's lemma over a number field.

theorem NumberField.one_le_norm_mul_house_pow {K : Type u_3} [Field K] [NumberField K] {x : K} (hx : IsIntegral ℤ x) (h0 : x ≠ 0) (σ : K →+* ℂ) : 1 ≤ ‖σ x‖ * house x ^ (Module.finrank ℚ K - 1)

Liouville's inequality in a number field K of degree d: a nonzero algebraic integer x ∈ K satisfies 1 ≤ ‖σ x‖ ⌈x⌉ᵈ⁻¹ for every embedding σ : K →+* ℂ, since its norm is a nonzero integer.

theorem NumberField.eq_zero_of_norm_le_exp_of_house_le_exp {K : Type u_3} [Field K] [NumberField K] (σ : K →+* ℂ) {y : K} {m : ℤ} (hm : m ≠ 0) {N : ℕ} (hint : IsIntegral ℤ (↑m ^ N * y)) {A B C : ℝ} (hσ : ‖σ y‖ ≤ Real.exp A) (hy : house y ≤ Real.exp B) (hmC : |↑m| ^ N ≤ Real.exp C) (h : C + A + ↑(Module.finrank ℚ K - 1) * (C + B) < 0) : y = 0

Liouville's inequality in exponential form. Let K be a number field of degree d, σ : K →+* ℂ, y ∈ K and m ≠ 0 an integer with m ^ N y an algebraic integer. If ‖σ y‖ ≤ exp A, ⌈y⌉ ≤ exp B and |m| ^ N ≤ exp C with C + A + (d - 1) (C + B) < 0, then y = 0.

theorem TauCeti.inv_norm_le_pow_mul_house_pow_of_mem_rootSet {F : Type u_1} [Field F] [CharZero F] {x : F} {b : ℕ} (hb : b ≠ 0) (hbx : IsIntegral ℤ (↑b * x)) (h0 : x ≠ 0) {z : ℂ} (hz : z ∈ (minpoly ℚ x).rootSet ℂ) : ‖z‖⁻¹ ≤ ↑b ^ (minpoly ℚ x).natDegree * house x ^ ((minpoly ℚ x).natDegree - 1)

A Liouville-type lower bound for the conjugates of a nonzero algebraic number: if b ≠ 0 and b x is integral over ℤ, then every complex conjugate z of x satisfies ‖z‖⁻¹ ≤ bᵈ ⌈x⌉ᵈ⁻¹, that is, ‖z‖ ≥ b⁻ᵈ ⌈x⌉¹⁻ᵈ, where d is the degree of x. For an algebraic integer x one may take b = 1.

theorem TauCeti.inv_norm_le_natDenominator_pow_mul_house_pow_of_mem_rootSet {F : Type u_1} [Field F] [CharZero F] {x : F} (h0 : x ≠ 0) {z : ℂ} (hz : z ∈ (minpoly ℚ x).rootSet ℂ) : ‖z‖⁻¹ ≤ ↑(Algebra.natDenominator x) ^ (minpoly ℚ x).natDegree * house x ^ ((minpoly ℚ x).natDegree - 1)

The lower bound ‖z‖⁻¹ ≤ den(x)ᵈ ⌈x⌉ᵈ⁻¹ for every complex conjugate z of a nonzero algebraic number x of degree d, where den(x) is its natural-number denominator. Equivalently, ‖z‖ ≥ den(x)⁻ᵈ ⌈x⌉¹⁻ᵈ.

theorem TauCeti.inv_norm_le_natDenominator_pow_mul_house_pow {z : ℂ} (hz : IsAlgebraic ℚ z) (h0 : z ≠ 0) : ‖z‖⁻¹ ≤ ↑(Algebra.natDenominator z) ^ (minpoly ℚ z).natDegree * house z ^ ((minpoly ℚ z).natDegree - 1)

A nonzero algebraic complex number z of degree d satisfies ‖z‖⁻¹ ≤ den(z)ᵈ ⌈z⌉ᵈ⁻¹, that is, ‖z‖ ≥ den(z)⁻ᵈ ⌈z⌉¹⁻ᵈ.

theorem NumberField.house_natCast_mul_pow_mul_pow_le {K : Type u_3} [Field K] [NumberField K] (α : K) {b c j n : ℕ} (hc : c ≤ 2 ^ n) (hj : j ≤ n) : house (↑c * (↑b ^ n * α ^ j)) ≤ (2 * ↑b * max 1 (house α)) ^ n

In a number field, the house of c b ^ n α ^ j is at most (2 b max(1, ⌈α⌉)) ^ n when c ≤ 2 ^ n and j ≤ n.

Examples