Heights over number fields

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

TODO

Prove that the height of (x₀ : x₁ : ··· : xₙ) ∈ ℙⁿ(ℚ) equals the maximum of the absolute values of the xᵢ when they are chosen to be coprime integers. This should then be split off into a separate Mathlib.NumberTheory.Height.Rat file.

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 of rational numbers

Since ℚ has a unique infinite place (the usual absolute value) and every finite place satisfies v n ≤ 1 for n : ℕ, the height simplifies to mulHeight₁ (n : ℚ) = n and logHeight₁ (n : ℚ) = Real.log n for 1 ≤ n.

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

The multiplicative height of a positive natural number 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 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.