Relative and absolute heights in extensions of number fields

The multiplicative height Height.mulHeight x of a tuple x over a number field K is relative to K: it is computed from the places of K. This file compares it across fields.

For an extension of number fields L / K and a finite tuple x over K, H_L(x) = H_K(x) ^ [L : K], including the zero tuple, where both sides are 1. Consequently a ring isomorphism of number fields preserves relative heights, and the absolute height NumberField.absMulHeight₁ x, which Mathlib defines through the number field ℚ(x), may be computed in any number field K containing x as H_K(x) ^ (1 / [K : ℚ]). Elements of possibly different characteristic-zero fields with the same rational minimal polynomial have the same absolute height; in particular the absolute height is invariant under field embeddings.

For a nonzero tuple of algebraic integers the finite places contribute at most one to the height, so archimedean bounds on the coordinates bound the height.

Main results

• NumberField.mulHeight_algebraMap: H_L(x) = H_K(x) ^ [L : K], together with the scalar and logarithmic versions.
• NumberField.mulHeight₁_natCast: a positive natural number n has height n ^ [K : ℚ] over K.
• NumberField.mulHeight_ringEquiv: a ring isomorphism of number fields preserves relative height, together with the scalar and logarithmic versions.
• NumberField.absMulHeight₁_eq_rpow: for x in a number field K, the absolute height of x is H_K(x) ^ (1 / [K : ℚ]).
• NumberField.absMulHeight₁_eq_of_minpoly_eq: equal rational minimal polynomials give equal absolute heights.
• NumberField.absMulHeight₁_ratCast: the absolute height of a rational number is its height over ℚ.
• NumberField.absMulHeight₁_pow: H(x ^ n) = H(x) ^ n.
• NumberField.absMulHeight₁_inv: H(x⁻¹) = H(x).
• NumberField.mulHeight_le_pow_finrank_of_forall_le: a nonzero tuple of algebraic integers whose coordinates are at most c at every infinite place has height at most c ^ [K : ℚ].

References

• X. Wu, Diophantine geometry, week 08: arithmetic heights (2023), §2, Lemma 2.5 and Definition 2.7.
• C. Smyth, The Mahler measure of algebraic numbers: a survey (2008), §1.

theorem NumberField.mulHeight_mul_absNorm_span_range {K : Type u_1} [Field K] [NumberField K] {ι : Type u_3} [Finite ι] (y : ι → RingOfIntegers K) : (Height.mulHeight fun (i : ι) => ↑(y i)) * ↑(Ideal.absNorm (Ideal.span (Set.range y))) = ∏ v : InfinitePlace K, (⨆ (i : ι), v ↑(y i)) ^ v.mult

For a tuple y of algebraic integers, the multiplicative height times the absolute norm of the ideal generated by the coordinates is the archimedean part of the height. For the zero tuple both sides are 0.

theorem NumberField.finprod_iSup_finitePlace_le_one {K : Type u_1} [Field K] [NumberField K] {ι : Type u_3} (y : ι → RingOfIntegers K) : ∏ᶠ (v : FinitePlace K), ⨆ (i : ι), v ↑(y i) ≤ 1

For a tuple of algebraic integers, the finite part of the multiplicative height is at most one.

theorem NumberField.mulHeight_le_pow_finrank_of_forall_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_3} {y : ι → RingOfIntegers K} (hy : y ≠ 0) {c : ℝ} (hc : ∀ (i : ι) (w : InfinitePlace K), w ↑(y i) ≤ c) : (Height.mulHeight fun (i : ι) => ↑(y i)) ≤ c ^ Module.finrank ℚ K

A nonzero tuple of algebraic integers whose coordinates have absolute value at most c at every infinite place has multiplicative height at most c ^ [K : ℚ].

@[simp]

theorem NumberField.mulHeight_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] {ι : Type u_3} [Finite ι] (x : ι → K) : Height.mulHeight (⇑(algebraMap K L) ∘ x) = Height.mulHeight x ^ Module.finrank K L

Relative heights in an extension. For an extension of number fields L / K and a finite tuple x over K, the multiplicative height of x over L is its height over K raised to the degree [L : K].

@[simp]

theorem NumberField.logHeight_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] {ι : Type u_3} [Finite ι] (x : ι → K) : Height.logHeight (⇑(algebraMap K L) ∘ x) = ↑(Module.finrank K L) * Height.logHeight x

The logarithmic height of a tuple over L / K is [L : K] times its height over K.

@[simp]

theorem NumberField.mulHeight₁_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (x : K) : Height.mulHeight₁ ((algebraMap K L) x) = Height.mulHeight₁ x ^ Module.finrank K L

The multiplicative height of x ∈ K over L / K is its height over K raised to the degree [L : K].

@[simp]

theorem NumberField.logHeight₁_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (x : K) : Height.logHeight₁ ((algebraMap K L) x) = ↑(Module.finrank K L) * Height.logHeight₁ x

The logarithmic height of x ∈ K over L / K is [L : K] times its height over K.

theorem NumberField.mulHeight₁_natCast {K : Type u_1} [Field K] [NumberField K] (n : ℕ) [NeZero n] : Height.mulHeight₁ ↑n = ↑n ^ Module.finrank ℚ K

The multiplicative height of a positive natural number n over a number field K is n ^ [K : ℚ]. Relative heights are not invariant under extension: over ℚ(i) the height of 2 is 4.

theorem NumberField.logHeight₁_natCast {K : Type u_1} [Field K] [NumberField K] (n : ℕ) : Height.logHeight₁ ↑n = ↑(Module.finrank ℚ K) * Real.log ↑n

The logarithmic height of a natural number n over a number field K is [K : ℚ] * log n; both sides are 0 for n = 0.

@[simp]

theorem NumberField.mulHeight_ringEquiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_3} [Finite ι] {K' : Type u_4} [Field K'] [NumberField K'] (e : K ≃+* K') (x : ι → K) : Height.mulHeight (⇑e ∘ x) = Height.mulHeight x

A ring isomorphism of number fields preserves the multiplicative height of tuples.

@[simp]

theorem NumberField.mulHeight₁_ringEquiv {K : Type u_1} [Field K] [NumberField K] {K' : Type u_4} [Field K'] [NumberField K'] (e : K ≃+* K') (x : K) : Height.mulHeight₁ (e x) = Height.mulHeight₁ x

A ring isomorphism of number fields preserves the multiplicative height of elements.

@[simp]

theorem NumberField.logHeight_ringEquiv {K : Type u_1} [Field K] [NumberField K] {ι : Type u_3} [Finite ι] {K' : Type u_4} [Field K'] [NumberField K'] (e : K ≃+* K') (x : ι → K) : Height.logHeight (⇑e ∘ x) = Height.logHeight x

A ring isomorphism of number fields preserves the logarithmic height of tuples.

@[simp]

theorem NumberField.logHeight₁_ringEquiv {K : Type u_1} [Field K] [NumberField K] {K' : Type u_4} [Field K'] [NumberField K'] (e : K ≃+* K') (x : K) : Height.logHeight₁ (e x) = Height.logHeight₁ x

A ring isomorphism of number fields preserves the logarithmic height of elements.

theorem NumberField.absMulHeight₁_eq_rpow {K : Type u_1} [Field K] [NumberField K] (x : K) : absMulHeight₁ x = Height.mulHeight₁ x ^ (↑(Module.finrank ℚ K))⁻¹

The absolute height of an element x of a number field K is its height relative to K raised to the power 1 / [K : ℚ].

theorem NumberField.absLogHeight₁_eq_div {K : Type u_1} [Field K] [NumberField K] (x : K) : absLogHeight₁ x = Height.logHeight₁ x / ↑(Module.finrank ℚ K)

The absolute logarithmic height of an element x of a number field K is its logarithmic height relative to K divided by [K : ℚ].

theorem NumberField.absMulHeight₁_eq_of_minpoly_eq {F : Type u_4} {F' : Type u_5} [Field F] [CharZero F] [Field F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : absMulHeight₁ x = absMulHeight₁ y

Elements of characteristic-zero fields with the same minimal polynomial over ℚ have the same absolute height. This includes transcendental elements, whose minimal polynomial is 0 and whose absolute height is the junk value 1.

theorem NumberField.absLogHeight₁_eq_of_minpoly_eq {F : Type u_4} {F' : Type u_5} [Field F] [CharZero F] [Field F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : absLogHeight₁ x = absLogHeight₁ y

Elements of characteristic-zero fields with the same minimal polynomial over ℚ have the same absolute logarithmic height.

@[simp]

theorem NumberField.absMulHeight₁_map {F : Type u_4} {F' : Type u_5} [Field F] [CharZero F] [Field F'] [CharZero F'] (f : F →+* F') (x : F) : absMulHeight₁ (f x) = absMulHeight₁ x

The absolute height is invariant under ring homomorphisms of characteristic-zero fields.

@[simp]

theorem NumberField.absLogHeight₁_map {F : Type u_4} {F' : Type u_5} [Field F] [CharZero F] [Field F'] [CharZero F'] (f : F →+* F') (x : F) : absLogHeight₁ (f x) = absLogHeight₁ x

The absolute logarithmic height is invariant under ring homomorphisms of characteristic-zero fields.

@[simp]

theorem NumberField.absMulHeight₁_ratCast {F : Type u_4} [Field F] [CharZero F] (q : ℚ) : absMulHeight₁ ↑q = Height.mulHeight₁ q

The absolute height of a rational number in a characteristic-zero field is its height over ℚ.

@[simp]

theorem NumberField.absLogHeight₁_ratCast {F : Type u_4} [Field F] [CharZero F] (q : ℚ) : absLogHeight₁ ↑q = Height.logHeight₁ q

The absolute logarithmic height of a rational number in a characteristic-zero field is its logarithmic height over ℚ.

@[simp]

theorem NumberField.absMulHeight₁_zero {F : Type u_4} [Field F] [CharZero F] : absMulHeight₁ 0 = 1

The absolute height of 0 is 1.

@[simp]

theorem NumberField.absLogHeight₁_zero {F : Type u_4} [Field F] [CharZero F] : absLogHeight₁ 0 = 0

The absolute logarithmic height of 0 is 0.

@[simp]

theorem NumberField.absMulHeight₁_one {F : Type u_4} [Field F] [CharZero F] : absMulHeight₁ 1 = 1

The absolute height of 1 is 1.

@[simp]

theorem NumberField.absLogHeight₁_one {F : Type u_4} [Field F] [CharZero F] : absLogHeight₁ 1 = 0

The absolute logarithmic height of 1 is 0.

theorem NumberField.absMulHeight₁_natCast {F : Type u_4} [Field F] [CharZero F] (n : ℕ) [NeZero n] : absMulHeight₁ ↑n = ↑n

The absolute height of a positive natural number n is n.

theorem NumberField.absLogHeight₁_natCast {F : Type u_4} [Field F] [CharZero F] (n : ℕ) : absLogHeight₁ ↑n = Real.log ↑n

The absolute logarithmic height of a natural number n is log n; both sides are 0 for n = 0.

theorem NumberField.absMulHeight₁_pow {F : Type u_4} [Field F] [CharZero F] (x : F) (n : ℕ) : absMulHeight₁ (x ^ n) = absMulHeight₁ x ^ n

The absolute height of a power is the power of the absolute height. This includes transcendental elements, whose positive powers are transcendental and all have the junk height 1.

theorem NumberField.absLogHeight₁_pow {F : Type u_4} [Field F] [CharZero F] (x : F) (n : ℕ) : absLogHeight₁ (x ^ n) = ↑n * absLogHeight₁ x

The absolute logarithmic height of x ^ n is n times that of x.

@[simp]

theorem NumberField.absMulHeight₁_inv {F : Type u_4} [Field F] [CharZero F] (x : F) : absMulHeight₁ x⁻¹ = absMulHeight₁ x

The absolute height of x⁻¹ is the absolute height of x. This includes x = 0, where 0⁻¹ = 0, and transcendental elements, whose inverses are transcendental.

@[simp]

theorem NumberField.absLogHeight₁_inv {F : Type u_4} [Field F] [CharZero F] (x : F) : absLogHeight₁ x⁻¹ = absLogHeight₁ x

The absolute logarithmic height of x⁻¹ is the absolute logarithmic height of x.