Places and completions of the rationals

15 fully proved

Place

InductivePlaces of \(\mathbb{Q}\)#✓fully proved

The set \(M_{\mathbb{Q}}\) of places of \(\mathbb{Q}\), which indexes the inequivalent normalised absolute values on \(\mathbb{Q}\). It consists of one infinite place, corresponding to the ordinary archimedean absolute value, and one finite place for each prime number \(p\), corresponding to the \(p\)-adic absolute value.

inductive Place : Type where
  | infinite : Place
  | finite : (prime : Nat.Primes) → Place
  deriving DecidableEq

Used by 13

Used byAbsolute value at a rational place · Absolute value at a finite rational place · Absolute value at the infinite rational place · Bundled completed field at a rational place · Completed field at a rational place · The rationals are dense in each completion · Density of the rationals with a place's absolute value in the completion · Embedding of the rationals into a completion · Norm of a rational in a completion · Every nontrivial absolute value on \(\mathbb{Q}\) is equivalent to that of a place · Ostrowski's theorem for \(\mathbb{Q}\), indexed by places · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

DefinitionAbsolute value at a rational place#✓fully proved

For a place \(v\) of \(\mathbb{Q}\), the absolute value \(|\cdot|_v : \mathbb{Q} \to \mathbb{R}\) sends \(q \in \mathbb{Q}\) to the ordinary absolute value \(|q|\) when \(v\) is the infinite place. When \(v\) is the finite place at a prime \(p\), it sends \(q\) to the normalised \(p\)-adic absolute value \(|q|_p\), where \(|0|_p = 0\) and \(|q|_p = p^{-v_p(q)}\) for \(q \neq 0\), with \(v_p(q)\) the \(p\)-adic valuation of \(q\).

noncomputable def absoluteValue : Place → AbsoluteValue ℚ ℝ
  | .infinite => Rat.AbsoluteValue.real
  | .finite prime =>
    haveI : Fact prime.1.Prime := ⟨prime.2⟩
    Rat.AbsoluteValue.padic prime.1

Uses 1 · Used by 8

Statement usesPlaces of \(\mathbb{Q}\)

Used byAbsolute value at a finite rational place · Absolute value at the infinite rational place · Density of the rationals with a place's absolute value in the completion · Norm of a rational in a completion · Every nontrivial absolute value on \(\mathbb{Q}\) is equivalent to that of a place · Ostrowski's theorem for \(\mathbb{Q}\), indexed by places · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

StructureBundled complete normed field#✓fully proved

A complete normed field bundled with its structure: a type \(K\) together with a normed field structure on \(K\) for which \(K\) is complete with respect to the metric induced by the norm. It is used to package the completed fields \(\mathbb{Q}_v\) of \(\mathbb{Q}\) at its places \(v\).

structure CompletedFieldBundle where
  carrier : Type
  [normedField : NormedField carrier]
  [completeSpace : CompleteSpace carrier]

Used by 8

Used byBundled completed field at a rational place · Completed field at a rational place · The rationals are dense in each completion · Density of the rationals with a place's absolute value in the completion · Embedding of the rationals into a completion · Norm of a rational in a completion · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

AbbreviationBundled completed field at a rational place#✓fully proved

To each place \(v\) of \(\mathbb{Q}\) this assigns a complete normed field: the real numbers \(\mathbb{R}\) with the usual absolute value when \(v\) is the infinite place, and, when \(v\) is the finite place at a prime \(p\), the field \(\mathbb{Q}_p\) of \(p\)-adic numbers with the \(p\)-adic norm.

noncomputable abbrev bundle : Place → CompletedFieldBundle
  | .infinite => ⟨ℝ⟩
  | .finite prime =>
    haveI : Fact prime.1.Prime := ⟨prime.2⟩
    ⟨Padic prime.1⟩

Uses 2 · Used by 7

Statement usesPlaces of \(\mathbb{Q}\) · Bundled complete normed field

Used byCompleted field at a rational place · The rationals are dense in each completion · Density of the rationals with a place's absolute value in the completion · Embedding of the rationals into a completion · Norm of a rational in a completion · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

AbbreviationCompleted field at a rational place#✓fully proved

For a place \(v\) of \(\mathbb{Q}\), the completed field \(\mathbb{Q}_v\) is the field \(\mathbb{R}\) of real numbers when \(v\) is the infinite place and, when \(v\) is the finite place at a prime \(p\), the field \(\mathbb{Q}_p\) of \(p\)-adic numbers.

It is a complete normed field, with the usual absolute value on \(\mathbb{R}\) and the \(p\)-adic norm on \(\mathbb{Q}_p\).

noncomputable abbrev CompletedField (v : Place) : Type :=
  (bundle v : Type)

Uses 3 · Used by 6

Statement usesPlaces of \(\mathbb{Q}\) · Bundled complete normed field · Bundled completed field at a rational place

Used byThe rationals are dense in each completion · Density of the rationals with a place's absolute value in the completion · Embedding of the rationals into a completion · Norm of a rational in a completion · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

DefinitionEmbedding of the rationals into a completion#✓fully proved

For a place \(v\) of \(\mathbb{Q}\) with completed field \(\mathbb{Q}_v\), the canonical ring homomorphism \(\mathbb{Q} \to \mathbb{Q}_v\) sends each rational number to itself, viewed as a real number when \(v\) is the infinite place and as a \(p\)-adic number when \(v\) is the finite place at a prime \(p\).

noncomputable def embedding : (v : Place) → ℚ →+* CompletedField v
  | .infinite => Rat.castHom ℝ
  | .finite prime =>
    haveI : Fact prime.1.Prime := ⟨prime.2⟩
    Rat.castHom (Padic prime.1)

Uses 4 · Used by 5

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Bundled completed field at a rational place

Used byThe rationals are dense in each completion · Density of the rationals with a place's absolute value in the completion · Norm of a rational in a completion · Embedding of \(\mathbb{Q}\), normed by a place, into its completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

TheoremAbsolute value at the infinite rational place#✓fully proved

For every \(q \in \mathbb{Q}\), the absolute value attached to the infinite place of \(\mathbb{Q}\), evaluated at \(q\), equals the ordinary absolute value \(|q|\) of \(q\) viewed as a real number.

theorem absoluteValue_infinite_apply (q : ℚ) :
    absoluteValue .infinite q = |(q : ℝ)|

Uses 2

Statement usesPlaces of \(\mathbb{Q}\) · Absolute value at a rational place

TheoremAbsolute value at a finite rational place#✓fully proved

For every prime \(p\) and every \(q \in \mathbb{Q}\), the absolute value attached to the finite place of \(\mathbb{Q}\) at \(p\), evaluated at \(q\), equals the \(p\)-adic absolute value \(|q|_p\) of \(q\). Here \(|0|_p = 0\), and \(|q|_p = p^{-v_p(q)}\) for \(q \neq 0\), where \(v_p(q)\) is the \(p\)-adic valuation of \(q\).

theorem absoluteValue_finite_apply (prime : Nat.Primes) (q : ℚ) :
    let _ : Fact prime.1.Prime := ⟨prime.2⟩
    absoluteValue (.finite prime) q = Rat.AbsoluteValue.padic prime.1 q

Uses 2

Statement usesPlaces of \(\mathbb{Q}\) · Absolute value at a rational place

TheoremNorm of a rational in a completion#✓fully proved

For every place \(v\) of \(\mathbb{Q}\) and every \(q \in \mathbb{Q}\), the norm in the completed field \(\mathbb{Q}_v\) of the image of \(q\) under the canonical embedding \(\mathbb{Q} \to \mathbb{Q}_v\) equals \(|q|_v\), the absolute value attached to \(v\) evaluated at \(q\).

theorem embedding_norm_eq_absoluteValue (v : Place) (q : ℚ) :
    ‖embedding v q‖ = v.absoluteValue q

Uses 6 · Used by 1

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Absolute value at a rational place · Bundled completed field at a rational place · Embedding of the rationals into a completion

Used byThe embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

TheoremThe rationals are dense in each completion#✓fully proved

For every place \(v\) of \(\mathbb{Q}\), with completed field \(\mathbb{Q}_v\), the image of \(\mathbb{Q}\) under the canonical embedding \(\mathbb{Q} \to \mathbb{Q}_v\) is dense in \(\mathbb{Q}_v\).

theorem denseRange_embedding (v : Place) :
    DenseRange (embedding v)

Uses 5 · Used by 1

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Bundled completed field at a rational place · Embedding of the rationals into a completion

Used byDensity of the rationals with a place's absolute value in the completion

TheoremEvery nontrivial absolute value on \(\mathbb{Q}\) is equivalent to that of a place#✓fully proved

Let \(f\) be a real-valued absolute value on \(\mathbb{Q}\) that is nontrivial, that is, \(f(x) \ne 1\) for some \(x \ne 0\). Then there is a place \(v\) of \(\mathbb{Q}\) such that \(f\) is equivalent to the absolute value \(|\cdot|_v\) attached to \(v\) (the ordinary absolute value at the infinite place, the \(p\)-adic absolute value at the prime \(p\)).

Here two absolute values \(f\) and \(g\) on \(\mathbb{Q}\) are equivalent when \(f(x) \le f(y)\) holds exactly when \(g(x) \le g(y)\), for all \(x, y \in \mathbb{Q}\).

theorem exists_place_equiv (f : AbsoluteValue ℚ ℝ) (hf : f.IsNontrivial) :
    ∃ v : Place, f ≈ v.absoluteValue

Uses 2

Statement usesPlaces of \(\mathbb{Q}\) · Absolute value at a rational place

TheoremOstrowski's theorem for \(\mathbb{Q}\), indexed by places#✓fully proved

Let \(f\) be a real-valued absolute value on \(\mathbb{Q}\) that is nontrivial, that is, \(f(x) \ne 1\) for some \(x \ne 0\). Then there is exactly one place \(v\) of \(\mathbb{Q}\) such that \(f\) is equivalent to the absolute value \(|\cdot|_v\) attached to \(v\) (the ordinary absolute value at the infinite place, the \(p\)-adic absolute value at the prime \(p\)).

Here two absolute values \(f\) and \(g\) on \(\mathbb{Q}\) are equivalent when \(f(x) \le f(y)\) holds exactly when \(g(x) \le g(y)\), for all \(x, y \in \mathbb{Q}\).

theorem exists_unique_place_equiv (f : AbsoluteValue ℚ ℝ) (hf : f.IsNontrivial) :
    ∃! v : Place, f ≈ v.absoluteValue

Uses 2

Statement usesPlaces of \(\mathbb{Q}\) · Absolute value at a rational place

DefinitionEmbedding of \(\mathbb{Q}\), normed by a place, into its completion#✓fully proved

For a place \(v\) of \(\mathbb{Q}\), the ring homomorphism from \(\mathbb{Q}\), equipped with the absolute value \(|\cdot|_v\) attached to \(v\) as its norm, into the completed field \(\mathbb{Q}_v\) given by the canonical embedding of \(\mathbb{Q}\) (\(\mathbb{Q}_v = \mathbb{R}\) at the infinite place and \(\mathbb{Q}_v = \mathbb{Q}_p\) at a prime \(p\)).

noncomputable def withAbsEmbedding (v : Place) :
    WithAbs (v.absoluteValue) →+* CompletedField v :=
  (embedding v).comp (WithAbs.equiv (v.absoluteValue)).toRingHom

Uses 6 · Used by 2

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Absolute value at a rational place · Bundled completed field at a rational place · Embedding of the rationals into a completion

Used byDensity of the rationals with a place's absolute value in the completion · The embedding of \(\mathbb{Q}\) into its completion at a place is an isometry

TheoremThe embedding of \(\mathbb{Q}\) into its completion at a place is an isometry#✓fully proved

Let \(v\) be a place of \(\mathbb{Q}\), let \(|\cdot|_v\) be the absolute value attached to \(v\), and let \(\mathbb{Q}_v\) be the completed field at \(v\). The canonical embedding of \(\mathbb{Q}\), equipped with the metric \(d(x, y) = |x - y|_v\), into \(\mathbb{Q}_v\) is an isometry: for all \(x, y \in \mathbb{Q}\), the distance between the images of \(x\) and \(y\) in \(\mathbb{Q}_v\) equals \(|x - y|_v\).

theorem withAbsEmbedding_isometry (v : Place) :
    Isometry (withAbsEmbedding v)

Uses 8

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Absolute value at a rational place · Bundled completed field at a rational place · Embedding of \(\mathbb{Q}\), normed by a place, into its completion

Proof usesEmbedding of the rationals into a completion · Norm of a rational in a completion

TheoremDensity of the rationals with a place's absolute value in the completion#✓fully proved

Let \(v\) be a place of \(\mathbb{Q}\), let \(|\cdot|_v\) be the absolute value attached to \(v\), let \(\mathbb{Q}_v\) be the completed field at \(v\), and write \((\mathbb{Q}, |\cdot|_v)\) for the field \(\mathbb{Q}\) equipped with \(|\cdot|_v\). The image of the canonical ring homomorphism \((\mathbb{Q}, |\cdot|_v) \to \mathbb{Q}_v\), which sends each rational number to itself, is dense in \(\mathbb{Q}_v\).

theorem denseRange_withAbsEmbedding (v : Place) :
    DenseRange (withAbsEmbedding v)

Uses 8

Statement usesPlaces of \(\mathbb{Q}\) · Completed field at a rational place · Bundled complete normed field · Absolute value at a rational place · Bundled completed field at a rational place · Embedding of \(\mathbb{Q}\), normed by a place, into its completion

Proof usesThe rationals are dense in each completion · Embedding of the rationals into a completion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.