Instances of AdmissibleAbsValues

We provide instances of Height.AdmissibleAbsValues for

• algebraic number fields.

TODO

• Fields of rational functions in n variables.

• Finite extensions of fields with Height.AdmissibleAbsValues.

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

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