Documentation

Mathlib.NumberTheory.Height.NumberField

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 #

source
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
Instances For
    source
    @[simp]
    theorem NumberField.mem_multisetInfinitePlace {K : Type u_1} [Field K] [NumberField K] {v : AbsoluteValue K ℝ} :
    v ∈ multisetInfinitePlace K ↔ IsInfinitePlace v
    source
    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
    source
    @[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.
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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.

    source
    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.

    source
    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.

    source
    theorem NumberField.totalWeight_eq_sum_mult (K : Type u_1) [Field K] [NumberField K] :
    Height.totalWeight K = ∑ v : InfinitePlace K, v.mult
    source
    theorem NumberField.totalWeight_eq_finrank (K : Type u_1) [Field K] [NumberField K] :
    Height.totalWeight K = Module.finrank ℚ K
    source
    theorem NumberField.totalWeight_pos (K : Type u_1) [Field K] [NumberField K] :
    0 < Height.totalWeight K
    source
    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.

    Positivity extension for totalWeight on number fields #

    source
    def Mathlib.Meta.Positivity.evalHeightTotalWeight :
    PositivityExt

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

    Instances For

      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.

      source
      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.

      source
      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.

      source
      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.

      source
      theorem Rat.mulHeight_self_one_eq_mulHeight_num_den (q : ℚ) :
      Height.mulHeight ![q, 1] = Height.mulHeight ![↑q.num, ↑q.den]
      source
      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.

      source
      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.

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

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

      source
      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.