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.

Instance for number fields #

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

Instances For
    source
    📐 coverage
    @[simp]
    theorem NumberField.mem_multisetInfinitePlace {K : Type u_1} [Field K] [NumberField K] {v : AbsoluteValue K ℝ} :
    v ∈ multisetInfinitePlace K ↔ IsInfinitePlace v
    source
    📐 coverage
    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
    🔸 coverage
    @[implicit_reducible]
    noncomputable instance NumberField.instAdmissibleAbsValues {K : Type u_1} [Field K] [NumberField K] :
    Height.AdmissibleAbsValues K
    source
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    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
    📐 coverage
    theorem NumberField.totalWeight_eq_sum_mult (K : Type u_1) [Field K] [NumberField K] :
    Height.totalWeight K = ∑ v : InfinitePlace K, v.mult
    source
    📐 coverage
    theorem NumberField.totalWeight_eq_finrank (K : Type u_1) [Field K] [NumberField K] :
    Height.totalWeight K = Module.finrank ℚ K
    source
    📐 coverage
    theorem NumberField.totalWeight_pos (K : Type u_1) [Field K] [NumberField K] :
    0 < Height.totalWeight K

    Positivity extension for totalWeight on number fields #

    source
    🔸 coverage
    def Mathlib.Meta.Positivity.evalHeightTotalWeight :
    PositivityExt

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

    Instances For