Places of a number field

DefinitionDegree-normalized absolute value at a finite place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be a finite place of \(K\), with absolute value \(|\cdot|_v\). The degree-normalized absolute value at \(v\) is the absolute value \(x \mapsto |x|_v^{1/d}\) on \(K\).

The finite-place absolute value \(|\cdot|_v\) already contains the local-degree factor, so the remaining normalization exponent is \(1/d\).

noncomputable def FinitePlace.normalizedAbsoluteValue (v : FinitePlace K) :
    AbsoluteValue K ℝ := by
  refine v.val.rpow (1 / (Module.finrank ℚ K : ℝ)) ?_ ?_
  · have hfinrank : 0 < (Module.finrank ℚ K : ℝ) := by
      exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)
    positivity
  · have hfinrank : 0 < (Module.finrank ℚ K : ℝ) := by
      exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)
    rw [div_le_one hfinrank]
    exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)

Uses 1 · Used by 2

Statement usesPowers of an absolute value

Used byValue of the degree-normalized absolute value at a finite place · Degree-normalized finite absolute value through the prime ideal

TheoremValue of the degree-normalized absolute value at a finite place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be a finite place of \(K\), with absolute value \(|\cdot|_v\). For every \(x \in K\), the degree-normalized absolute value of \(x\) at \(v\) equals \(|x|_v^{1/d}\).

@[simp]
theorem FinitePlace.normalizedAbsoluteValue_apply (v : FinitePlace K) (x : K) :
    v.normalizedAbsoluteValue x = v x ^ (1 / (Module.finrank ℚ K : ℝ))

Uses 3 · Used by 1

Statement usesDegree-normalized absolute value at a finite place

Proof usesPowers of an absolute value · Values of a power of an absolute value

Used byDegree-normalized finite absolute value through the prime ideal

TheoremDegree-normalized finite absolute value through the prime ideal#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\), let \(v\) be a finite place of \(K\), and let \(\mathfrak{p}\) be the nonzero prime ideal of the ring of integers of \(K\) that defines \(v\). For every \(x \in K\), the degree-normalized absolute value of \(x\) at \(v\) equals \(|x|_{\mathfrak{p}}^{1/d}\), where \(|x|_{\mathfrak{p}} = N(\mathfrak{p})^{-v_{\mathfrak{p}}(x)}\) for \(x \neq 0\) and \(|0|_{\mathfrak{p}} = 0\), with \(N(\mathfrak{p})\) the absolute norm of \(\mathfrak{p}\) and \(v_{\mathfrak{p}}\) the \(\mathfrak{p}\)-adic valuation.

theorem FinitePlace.normalizedAbsoluteValue_apply_eq_adicAbv (v : FinitePlace K) (x : K) :
    v.normalizedAbsoluteValue x =
      (HeightOneSpectrum.adicAbv K v.maximalIdeal x) ^
        (1 / (Module.finrank ℚ K : ℝ))

Uses 2

Statement usesDegree-normalized absolute value at a finite place

Proof usesValue of the degree-normalized absolute value at a finite place

DefinitionDegree-normalized absolute value at an infinite place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be an infinite place of \(K\), with absolute value \(|\cdot|_v\) and multiplicity \(m_v\), equal to \(1\) if \(v\) is real and \(2\) if \(v\) is complex. The degree-normalized absolute value at \(v\) is the absolute value \(x \mapsto |x|_v^{m_v/d}\) on \(K\).

NumberField.InfinitePlace.normalizedAbsoluteValue · 15 lines

noncomputable def InfinitePlace.normalizedAbsoluteValue (v : InfinitePlace K) :
    AbsoluteValue K ℝ := by
  refine v.val.rpow ((v.mult : ℝ) / (Module.finrank ℚ K : ℝ)) ?_ ?_
  · have hmult : 0 < (v.mult : ℝ) := by
      exact_mod_cast InfinitePlace.mult_pos (w := v)
    have hfinrank : 0 < (Module.finrank ℚ K : ℝ) := by
      exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)
    positivity
  · have hfinrank : 0 < (Module.finrank ℚ K : ℝ) := by
      exact_mod_cast Module.finrank_pos (R := ℚ) (M := K)
    rw [div_le_one hfinrank]
    exact_mod_cast calc
      v.mult ≤ ∑ w : InfinitePlace K, w.mult :=
        Finset.single_le_sum (fun w _ => Nat.zero_le w.mult) (Finset.mem_univ v)
      _ = Module.finrank ℚ K := InfinitePlace.sum_mult_eq

Uses 1 · Used by 3

Statement usesPowers of an absolute value

Used byValue of the degree-normalized absolute value at an infinite place · Degree-normalized absolute value at a complex place · Degree-normalized absolute value at a real place

TheoremValue of the degree-normalized absolute value at an infinite place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be an infinite place of \(K\), with absolute value \(|\cdot|_v\) and multiplicity \(m_v\), equal to \(1\) if \(v\) is real and \(2\) if \(v\) is complex. For every \(x \in K\), the degree-normalized absolute value of \(x\) at \(v\) equals \(|x|_v^{m_v/d}\).

@[simp]
theorem InfinitePlace.normalizedAbsoluteValue_apply (v : InfinitePlace K) (x : K) :
    v.normalizedAbsoluteValue x = v x ^ ((v.mult : ℝ) / (Module.finrank ℚ K : ℝ))

Uses 3 · Used by 2

Statement usesDegree-normalized absolute value at an infinite place

Proof usesPowers of an absolute value · Values of a power of an absolute value

Used byDegree-normalized absolute value at a complex place · Degree-normalized absolute value at a real place

TheoremDegree-normalized absolute value at a real place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be a real infinite place of \(K\), with absolute value \(|\cdot|_v\). For every \(x \in K\), the degree-normalized absolute value of \(x\) at \(v\) equals \(|x|_v^{1/d}\).

theorem InfinitePlace.normalizedAbsoluteValue_apply_of_isReal (v : InfinitePlace K)
    (hv : v.IsReal) (x : K) :
    v.normalizedAbsoluteValue x = v x ^ (1 / (Module.finrank ℚ K : ℝ))

Uses 2

Statement usesDegree-normalized absolute value at an infinite place

Proof usesValue of the degree-normalized absolute value at an infinite place

TheoremDegree-normalized absolute value at a complex place#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(v\) be a complex infinite place of \(K\), with absolute value \(|\cdot|_v\). For every \(x \in K\), the degree-normalized absolute value of \(x\) at \(v\) equals \(|x|_v^{2/d}\).

theorem InfinitePlace.normalizedAbsoluteValue_apply_of_isComplex (v : InfinitePlace K)
    (hv : v.IsComplex) (x : K) :
    v.normalizedAbsoluteValue x = v x ^ (2 / (Module.finrank ℚ K : ℝ))

Uses 2

Statement usesDegree-normalized absolute value at an infinite place

Proof usesValue of the degree-normalized absolute value at an infinite place

DefinitionPlaces of a number field#✓fully proved

For a number field \(K\), the places of \(K\) form the disjoint union of the infinite places of \(K\) (the absolute values coming from complex embeddings of \(K\)) and the finite places of \(K\) (the absolute values coming from nonzero prime ideals of the ring of integers \(\mathcal{O}_K\)).

def Place (K : Type*) [Field K] [NumberField K] : Type _ :=
  InfinitePlace K ⊕ FinitePlace K

Used by 2

Used byFinite places as places · Infinite places as places

DefinitionInfinite places as places#✓fully proved

For a number field \(K\), each infinite place \(v\) of \(K\) is regarded as a place of \(K\) via the inclusion of the infinite places into the disjoint union of the infinite and finite places of \(K\).

def infinitePlace {K : Type*} [Field K] [NumberField K]
    (v : InfinitePlace K) : Place K :=
  Sum.inl v

Uses 1

Statement usesPlaces of a number field

DefinitionFinite places as places#✓fully proved

For a number field \(K\), each finite place \(v\) of \(K\) is regarded as a place of \(K\) via the inclusion of the finite places into the disjoint union of the infinite and finite places of \(K\).

def finitePlace {K : Type*} [Field K] [NumberField K]
    (v : FinitePlace K) : Place K :=
  Sum.inr v

Uses 1

Statement usesPlaces of a number field

DefinitionResidue norm of a finite place#✓fully proved

Let \(v\) be a finite place of a number field \(K\) and \(\mathfrak{p}_v\) the corresponding nonzero prime ideal of the ring of integers \(\mathcal{O}_K\). The residue norm \(N(v)\) is the absolute norm \(|\mathcal{O}_K / \mathfrak{p}_v|\) of \(\mathfrak{p}_v\), the cardinality of the residue field at \(v\), regarded as a real number.

noncomputable def residueNorm {K : Type*} [Field K] [NumberField K]
    (v : FinitePlace K) : ℝ :=
  (Ideal.absNorm v.maximalIdeal.asIdeal : ℝ)

Used by 1

Used byHecke bound from a Satake pair at a finite place

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.