Heights over number fields

We provide an instance of Height.AdmissibleAbsValues for algebraic number fields and set up some API.

Main results

• Heights on number fields satisfy the Northcott property: If K is a number field, then the set of elements of K of bounded (multiplicative or logarithmic) height is finite; see NumberField.finite_setOf_mulHeight₁_le and NumberField.finite_setOf_logHeight₁_le. We also provide instances for Northcott (mulHeight₁ (K := K)) (which automatically leads also to Northcott (logHeight₁ (K := K))).

TODO

When this file gets long, split the material on heights over ℚ off into a file Rat.lean.

Instance for number fields

noncomputable def NumberField.multisetInfinitePlace (K : Type u_1) [Field K] [NumberField K] : Multiset (AbsoluteValue K ℝ)

The infinite places of a number field K as a Multiset of absolute values on K, with multiplicity given by InfinitePlace.mult.

Equations

• NumberField.multisetInfinitePlace K = Finset.univ.val.bind fun (v : NumberField.InfinitePlace K) => Multiset.replicate v.mult ↑v

@[simp]

theorem NumberField.mem_multisetInfinitePlace {K : Type u_1} [Field K] [NumberField K] {v : AbsoluteValue K ℝ} : v ∈ multisetInfinitePlace K ↔ IsInfinitePlace v

theorem NumberField.count_multisetInfinitePlace_eq_mult {K : Type u_1} [Field K] [NumberField K] [DecidableEq (AbsoluteValue K ℝ)] (v : InfinitePlace K) : Multiset.count (↑v) (multisetInfinitePlace K) = v.mult

@[implicit_reducible]

noncomputable instance NumberField.instAdmissibleAbsValues {K : Type u_1} [Field K] [NumberField K] : Height.AdmissibleAbsValues K

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.prod_archAbsVal_eq {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [CommMonoid M] (f : AbsoluteValue K ℝ → M) : (Multiset.map f Height.AdmissibleAbsValues.archAbsVal).prod = ∏ v : InfinitePlace K, f ↑v ^ v.mult

theorem NumberField.prod_nonarchAbsVal_eq {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [CommMonoid M] (f : AbsoluteValue K ℝ → M) : ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), f ↑v = ∏ᶠ (v : FinitePlace K), f ↑v

theorem NumberField.sum_archAbsVal_eq {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddCommMonoid M] (f : AbsoluteValue K ℝ → M) : (Multiset.map f Height.AdmissibleAbsValues.archAbsVal).sum = ∑ v : InfinitePlace K, v.mult • f ↑v

theorem NumberField.sum_nonarchAbsVal_eq {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} [AddCommMonoid M] (f : AbsoluteValue K ℝ → M) : ∑ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), f ↑v = ∑ᶠ (v : FinitePlace K), f ↑v

theorem NumberField.mulHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) : Height.mulHeight₁ x = (∏ v : InfinitePlace K, max (v x) 1 ^ v.mult) * ∏ᶠ (v : FinitePlace K), max (v x) 1

This is the familiar definition of the multiplicative height on a number field.

theorem NumberField.logHeight₁_eq {K : Type u_1} [Field K] [NumberField K] (x : K) : Height.logHeight₁ x = ∑ v : InfinitePlace K, ↑v.mult * (v x).posLog + ∑ᶠ (v : FinitePlace K), (v x).posLog

This is the familiar definition of the logarithmic height on a number field.

theorem NumberField.mulHeight_eq {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {x : ι → K} (hx : x ≠ 0) : Height.mulHeight x = (∏ v : InfinitePlace K, (⨆ (i : ι), v (x i)) ^ v.mult) * ∏ᶠ (v : FinitePlace K), ⨆ (i : ι), v (x i)

This is the familiar definition of the multiplicative height on (nonzero) tuples of number field elements.

theorem NumberField.totalWeight_eq_sum_mult (K : Type u_1) [Field K] [NumberField K] : Height.totalWeight K = ∑ v : InfinitePlace K, v.mult

theorem NumberField.totalWeight_eq_finrank (K : Type u_1) [Field K] [NumberField K] : Height.totalWeight K = Module.finrank ℚ K

theorem NumberField.totalWeight_pos (K : Type u_1) [Field K] [NumberField K] : 0 < Height.totalWeight K

theorem NumberField.absNorm_mul_finprod_finitePlace_eq_one {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} [Finite ι] {x : ι → RingOfIntegers K} (hx : x ≠ 0) : ↑(Ideal.absNorm (Ideal.span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ (i : ι), v ↑(x i) = 1

This statement is equivalent to the fact that the "finite part" of the multiplicative height of a (non-zero) tuple x is the inverse of the absolute norm of the ideal generated by the values of x. We state it in a way that avoids taking an inverse.

The Northcott property for heights on number fields

We show that a number field K has the Northcott property with respect to the multiplicative and with respect to the logarithmic height, i.e., for any B : ℝ the set of elements x : K such that mulHeight₁ x ≤ B (resp., logHeight₁ x ≤ B) is finite. See NumberField.finite_setOf_mulHeight₁_le and NumberField.finite_setOf_logHeight₁_le.

The main idea of the proof is as follows. We show that for every x : K there is n : ℕ such that n * x is an algebraic integer and n ≤ mulHeight₁ x; see NumberField.exists_nat_le_mulHeight₁. We also show that the set of a : 𝓞 K such that mulHeight₁ (a / n) is bounded is finite; see NumberField.finite_setOf_prod_infinitePlace_iSup_le. The result for the multiplicative height follows by combining these two ingredients, and the result for the logarithmic height follows from that for any field with a family of admissible absolute values (see Mathlib.NumberTheory.Height.Northcott).

theorem NumberField.exists_nat_ne_zero_exists_integer_mul_eq_and_absNorm_span_eq_pow {K : Type u_1} [Field K] [NumberField K] (x : K) : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (a : RingOfIntegers K), ↑n * x = ↑a ∧ Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (Module.finrank ℚ K - 1)

theorem NumberField.exists_nat_le_mulHeight₁ {K : Type u_1} [Field K] [NumberField K] (x : K) : ∃ (n : ℕ), n ≠ 0 ∧ ↑n ≤ Height.mulHeight₁ x ∧ IsIntegral ℤ (↑n * x)

If x : K (for a number field K), then we can find a nonzero n : ℕ such that n ≤ mulHeight₁ x and n * x is integral. I.e., the denominator of x can be bounded by its multplicative height.

theorem NumberField.finite_setOf_prod_infinitePlace_iSup_le {K : Type u_1} [Field K] [NumberField K] {n : ℕ} (hn : n ≠ 0) (B : ℝ) : {x : RingOfIntegers K | ∏ v : InfinitePlace K, (⨆ (i : Fin (Nat.succ 0).succ), v (![↑x, ↑n] i)) ^ v.mult ≤ B}.Finite

theorem NumberField.finite_setOf_mulHeight_nat_le {K : Type u_1} [Field K] [NumberField K] {n : ℕ} (hn : n ≠ 0) (B : ℝ) : {a : RingOfIntegers K | Height.mulHeight ![↑a, ↑n] ≤ B}.Finite

The set of a : 𝓞 K such that mulHeight₁ (a / n) = mulHeight ![a, n] is bounded (for some given nonzero n : ℕ) is finite.

theorem NumberField.finite_setOf_mulHeight₁_le (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : {x : K | Height.mulHeight₁ x ≤ B}.Finite

A number field K satisfies the Northcott property: The set of elements of bounded multiplicative height is finite.

instance NumberField.instNorthcottRealMulHeight₁ {K : Type u_1} [Field K] [NumberField K] : Northcott Height.mulHeight₁

theorem NumberField.finite_setOf_logHeight₁_le (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : {x : K | Height.logHeight₁ x ≤ B}.Finite

A number field K satisfies the Northcott property: The set of elements of bounded logarithmic height is finite.

Positivity extension for totalWeight on number fields

def Mathlib.Meta.Positivity.evalHeightTotalWeight : PositivityExt

Extension for the positivity tactic: Height.totalWeight is positive for number fields.

Heights over the rational numbers

We show that the Height.mulHeight of a tuple of coprime integers (considered as rational numbers) equals the maximum of their absolute values and that the Height.mulHeight₁ of a rational number is the maximum of the absolute value of the numerator and the denominator. We add the corresponding results for logarithmic heights.

theorem Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_one {ι : Type u_1} [Fintype ι] [Nonempty ι] {x : ι → ℤ} (v : NumberField.FinitePlace ℚ) (hx : Finset.univ.gcd x = 1) : ⨆ (i : ι), v ↑(x i) = 1

The term corresponding to a finite place in the definition of the multiplicative height of a tuple of rational numbers equals 1 if the tuple consists of coprime integers.

theorem Rat.mulHeight_eq_max_abs_of_gcd_eq_one {ι : Type u_1} [Fintype ι] [Nonempty ι] {x : ι → ℤ} (hx : Finset.univ.gcd x = 1) : Height.mulHeight (Int.cast ∘ x) = ↑(⨆ (i : ι), |x i|)

The multiplicative height of a tuple of rational numbers that consists of coprime integers is the maximum of the absolute values of the entries.

theorem Rat.logHeight_eq_max_abs_of_gcd_eq_one {ι : Type u_1} [Fintype ι] [Nonempty ι] {x : ι → ℤ} (hx : Finset.univ.gcd x = 1) : Height.logHeight (Int.cast ∘ x) = Real.log ↑(⨆ (i : ι), |x i|)

The logarithmic height of a tuple of rational numbers that consists of coprime integers is the logarithm of the maximum of the absolute values of the entries.

theorem Rat.mulHeight_self_one_eq_mulHeight_num_den (q : ℚ) : Height.mulHeight ![q, 1] = Height.mulHeight ![↑q.num, ↑q.den]

theorem Rat.mulHeight₁_eq_max (q : ℚ) : Height.mulHeight₁ q = ↑(max q.num.natAbs q.den)

The multiplicative height of a rational number is the maximum of the absolute value of its numerator and its denominator.

theorem Rat.logHeight₁_eq_log_max (q : ℚ) : Height.logHeight₁ q = Real.log ↑(max q.num.natAbs q.den)

The logarithmic height of a rational number is the logarithm of the maximum of the absolute value of its numerator and its denominator.

theorem Rat.mulHeight₁_natCast (n : ℕ) [NeZero n] : Height.mulHeight₁ ↑n = ↑n

The multiplicative height of a positive natural number n cast to ℚ equals n.

theorem Rat.logHeight₁_natCast (n : ℕ) [NeZero n] : Height.logHeight₁ ↑n = Real.log ↑n

The logarithmic height of a positive natural number n cast to ℚ equals log n.