Heights over number fields

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

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

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.

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.