Documentation

TauCeti.NumberTheory.NumberField.Global.Places.Basic

Places of a number field and their normalized absolute values #

Mathlib indexes the two kinds of place of a number field K by two unrelated types: the finite places by IsDedekindDomain.HeightOneSpectrum (π“ž K) and the infinite places by NumberField.InfinitePlace K. Both carry an absolute value, but with different normalizations, and the product formula NumberField.prod_abs_eq_one is stated as a product over the finite places times a product over the infinite places.

This file introduces the single indexing type TauCeti.GlobalNumberFields.Place K for all places of K, together with the normalized absolute value β€–Β·β€–_v attached to a place v, and states the product formula as one finprod over that type.

The normalization is the one that makes the product formula hold with all exponents equal to one:

Because of the square at the complex places, β€–Β·β€–_v is not an AbsoluteValue β€” it does not satisfy the triangle inequality there β€” so it is bundled as a MonoidWithZeroHom. This is the standard normalization: β€–Β·β€–_v is the module of the local field at v, which is what the idele norm and the product formula require.

Heights in Diophantine approximation instead use the degree-normalized absolute value TauCeti.GlobalNumberFields.normAbs, written |Β·|_v, the [K : β„š]-th root of β€–Β·β€–_v, whose products over the places give absolute heights.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev TauCeti.GlobalNumberFields.Place (K : Type u_1) [Field K] :
Type u_1

A place of a number field K: either a finite place, indexed by a height one prime of π“ž K, or an infinite place. This is an abbreviation for the disjoint union of Mathlib's two indexing types; it is the uniform vocabulary in which statements ranging over all places of K (the product formula, the restricted product defining the adeles, the idele norm) are phrased.

Instances For
    source
    noncomputable def TauCeti.GlobalNumberFields.normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] :
    Place K β†’ K β†’*β‚€ ℝ

    The normalized absolute value at a place of a number field: the v-adic absolute value at a finite place v, and w x ^ w.mult at an infinite place w, so that a real place contributes |x| and a complex place contributes |x| ^ 2.

    At a complex place this is not subadditive, so it is bundled as a MonoidWithZeroHom rather than as an AbsoluteValue.

    Instances For
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :
      (normalizedAbsValue (Sum.inl v)) x = (NumberField.HeightOneSpectrum.adicAbv K v) x
      source
      @[simp]
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (x : K) :
      (normalizedAbsValue (Sum.inr w)) x = w x ^ w.mult
      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_of_isReal {K : Type u_1} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : K) :
      (normalizedAbsValue (Sum.inr w)) x = w x

      At a real place the normalized absolute value is the absolute value itself.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_of_isComplex {K : Type u_1} [Field K] [NumberField K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (x : K) :
      (normalizedAbsValue (Sum.inr w)) x = w x ^ 2

      At a complex place the normalized absolute value is the square of the absolute value.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inr_eq_norm_embedding {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (x : K) :
      (normalizedAbsValue (Sum.inr w)) x = β€–w.embedding xβ€– ^ w.mult

      The normalized absolute value at an infinite place, computed through a complex embedding defining the place.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_eq_norm_coe {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :
      (normalizedAbsValue (Sum.inl v)) x = β€–IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion ↑(WithVal.toVal (IsDedekindDomain.HeightOneSpectrum.valuation K v) x)β€–

      The normalized absolute value at a finite place v is the norm in the v-adic completion.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_nonneg {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) :
      0 ≀ (normalizedAbsValue v) x
      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_eq_zero {K : Type u_1} [Field K] [NumberField K] (v : Place K) {x : K} :
      (normalizedAbsValue v) x = 0 ↔ x = 0
      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_pos {K : Type u_1} [Field K] [NumberField K] (v : Place K) {x : K} (hx : x β‰  0) :
      0 < (normalizedAbsValue v) x
      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_le_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) :
      (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) ≀ 1

      An algebraic integer has normalized absolute value at most 1 at every finite place.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) :
      (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) = 1 ↔ x βˆ‰ v.asIdeal

      An algebraic integer has normalized absolute value exactly 1 at a finite place precisely when it avoids the corresponding prime.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_le_one_iff {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (y : K) :
      (normalizedAbsValue (Sum.inl v)) y ≀ 1 ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K v) y ≀ 1

      At a finite place, having normalized absolute value at most 1 is having v-adic valuation at most 1.

      source
      theorem TauCeti.GlobalNumberFields.forall_normalizedAbsValue_inl_le_one_iff {K : Type u_1} [Field K] [NumberField K] (y : K) :
      (βˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (normalizedAbsValue (Sum.inl v)) y ≀ 1) ↔ y ∈ (algebraMap (NumberField.RingOfIntegers K) K).range

      An element of a number field is an algebraic integer exactly when its normalized absolute value is at most 1 at every finite place.

      source
      theorem TauCeti.GlobalNumberFields.normalizedAbsValue_inl_algebraMap_eq_absNorm_zpow {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : NumberField.RingOfIntegers K) (hx : x β‰  0) :
      (normalizedAbsValue (Sum.inl v)) ((algebraMap (NumberField.RingOfIntegers K) K) x) = ↑(Ideal.absNorm v.asIdeal) ^ (-↑(multiplicity v.asIdeal (Ideal.span {x})))

      The normalized absolute value of a nonzero algebraic integer at a finite place, explicitly: the ideal norm of the prime, raised to minus the multiplicity of that prime in the principal ideal generated by the integer.

      source
      theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_adicAbv {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
      Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (NumberField.HeightOneSpectrum.adicAbv K v) x

      A nonzero element of a number field lies outside all but finitely many height one primes, so its v-adic absolute values are almost all 1.

      source
      theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
      Function.HasFiniteMulSupport fun (v : Place K) => (normalizedAbsValue v) x

      A nonzero element of a number field has normalized absolute value 1 at all but finitely many places.

      source
      theorem TauCeti.GlobalNumberFields.finprod_normalizedAbsValue_inl {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
      ∏ᢠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (normalizedAbsValue (Sum.inl v)) x = ↑|(Algebra.norm β„š) x|⁻¹

      The finite part of the product formula, indexed by the height one primes of π“ž K.

      source
      theorem TauCeti.GlobalNumberFields.finprod_normalizedAbsValue_eq_one {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
      ∏ᢠ (v : Place K), (normalizedAbsValue v) x = 1

      The product formula for a number field, as a single product over all of its places, finite and infinite, of the normalized absolute values.

      source
      theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_iSup_normalizedAbsValue {K : Type u_1} [Field K] [NumberField K] {ΞΉ : Type u_2} [Finite ΞΉ] {y : ΞΉ β†’ K} (hy : y β‰  0) :
      Function.HasFiniteMulSupport fun (v : Place K) => ⨆ (i : ΞΉ), (normalizedAbsValue v) (y i)

      A tuple of elements of a number field which is not identically zero has, at all but finitely many places, largest normalized absolute value 1.

      The degree-normalized absolute value #

      source
      noncomputable def TauCeti.GlobalNumberFields.normAbs {K : Type u_1} [Field K] [NumberField K] (v : Place K) :
      K β†’*β‚€ ℝ

      The degree-normalized absolute value |x|_v = normalizedAbsValue v x ^ (1 / [K : β„š]) at a place v of a number field K. At an infinite place w it is w x ^ (mult w / [K : β„š]) (normAbs_inr), and at a finite place it is the [K : β„š]-th root of the v-adic absolute value (normAbs_inl).

      This is the normalization of Evertse–Ferretti, in which the product of the local factors of a height is the absolute height: it does not change when K is replaced by a finite extension.

      Instances For
        source
        theorem TauCeti.GlobalNumberFields.normAbs_apply {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) :
        (normAbs v) x = (normalizedAbsValue v) x ^ (1 / ↑(Module.finrank β„š K))
        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.normAbs_inl {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :
        (normAbs (Sum.inl v)) x = (NumberField.HeightOneSpectrum.adicAbv K v) x ^ (1 / ↑(Module.finrank β„š K))

        At a finite place v, the degree-normalized absolute value is the [K : β„š]-th root of the v-adic absolute value.

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.normAbs_inr {K : Type u_1} [Field K] [NumberField K] (w : NumberField.InfinitePlace K) (x : K) :
        (normAbs (Sum.inr w)) x = w x ^ (↑w.mult / ↑(Module.finrank β„š K))

        At an infinite place w, the degree-normalized absolute value is w x ^ (mult w / [K : β„š]).

        source
        @[simp]
        theorem TauCeti.GlobalNumberFields.normAbs_neg {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) :
        (normAbs v) (-x) = (normAbs v) x

        Negation does not change a degree-normalized absolute value.

        source
        theorem TauCeti.GlobalNumberFields.normAbs_nonneg {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) :
        0 ≀ (normAbs v) x
        source
        theorem TauCeti.GlobalNumberFields.normAbs_pos {K : Type u_1} [Field K] [NumberField K] (v : Place K) {x : K} (hx : x β‰  0) :
        0 < (normAbs v) x
        source
        theorem TauCeti.GlobalNumberFields.normAbs_pow_finrank {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) :
        (normAbs v) x ^ Module.finrank β„š K = (normalizedAbsValue v) x

        The [K : β„š]-th power of the degree-normalized absolute value is the normalized absolute value.

        source
        theorem TauCeti.GlobalNumberFields.iSup_normAbs_pow_finrank {K : Type u_1} [Field K] [NumberField K] {ΞΉ : Type u_2} (v : Place K) (y : ΞΉ β†’ K) :
        (⨆ (i : ΞΉ), (normAbs v) (y i)) ^ Module.finrank β„š K = ⨆ (i : ΞΉ), (normalizedAbsValue v) (y i)

        The [K : β„š]-th power of the largest degree-normalized absolute value of a tuple is its largest normalized absolute value.

        source
        theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_iSup_normAbs {K : Type u_1} [Field K] [NumberField K] {ΞΉ : Type u_2} [Finite ΞΉ] {y : ΞΉ β†’ K} (hy : y β‰  0) :
        Function.HasFiniteMulSupport fun (v : Place K) => ⨆ (i : ΞΉ), (normAbs v) (y i)

        A tuple of elements of a number field which is not identically zero has, at all but finitely many places, largest degree-normalized absolute value 1.

        source
        theorem TauCeti.GlobalNumberFields.hasFiniteMulSupport_normAbs {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
        Function.HasFiniteMulSupport fun (v : Place K) => (normAbs v) x

        A nonzero element of a number field has degree-normalized absolute value 1 at all but finitely many places.

        source
        theorem TauCeti.GlobalNumberFields.finprod_normAbs_eq_one {K : Type u_1} [Field K] [NumberField K] {x : K} (hx : x β‰  0) :
        ∏ᢠ (v : Place K), (normAbs v) x = 1

        The product formula for the degree-normalized absolute values of a number field.