theorem rat_dense_in_padic (p : ℕ) [Fact (Nat.Prime p)] : DenseRange Rat.cast

The rational numbers are dense in $\mathbb{Q}_p$: the inclusion $\mathbb{Q} \hookrightarrow \mathbb{Q}_p$ has dense range.

theorem AbsoluteValue.denseRange_algebraMap_pi {R : Type u_1} [Field R] {ι : Type u_2} [Fintype ι] {v : ι → AbsoluteValue R ℝ} (hnt : ∀ (i : ι), (v i).IsNontrivial) (hne : Pairwise fun (i j : ι) => ¬(v i).IsEquiv (v j)) : DenseRange ⇑(algebraMap R ((i : ι) → WithAbs (v i)))

Density of the diagonal embedding $R \to \prod_i (R, v_i)$ given a finite family of pairwise inequivalent nontrivial absolute values; this is the algebraic core of weak approximation.

theorem AbsoluteValue.denseRange_coe_completion_pi {R : Type u_1} [Field R] {ι : Type u_2} [Fintype ι] {v : ι → AbsoluteValue R ℝ} (hnt : ∀ (i : ι), (v i).IsNontrivial) (hne : Pairwise fun (i j : ι) => ¬(v i).IsEquiv (v j)) : DenseRange fun (x : R) (i : ι) => ↑(WithAbs.toAbs (v i) x)

Diagonal embedding into the product of completions has dense range: the image of $R$ is dense in $\prod_i \widehat{R}_{v_i}$ for pairwise inequivalent nontrivial absolute values.

inductive PlaceQ : Type

A place of $\mathbb{Q}$ is either the archimedean (real) place or a $p$-adic place for some prime $p$.

• finite (p : Nat.Primes) : PlaceQ
• infinite : PlaceQ

@[implicit_reducible]

instance instDecidableEqPlaceQ : DecidableEq PlaceQ

Decidable equality on places of $\mathbb{Q}$: two places are either both infinite, or finite with the same prime.

def PlaceQ.absValue : PlaceQ → AbsoluteValue ℚ ℝ

The absolute value on $\mathbb{Q}$ associated to a place: the $p$-adic absolute value for a finite place, and the real absolute value $|\cdot|_\infty$ for the infinite place.

theorem PlaceQ.absValue_isNontrivial_finite (p : Nat.Primes) : (finite p).absValue.IsNontrivial

The $p$-adic absolute value on $\mathbb{Q}$ is nontrivial: $|p|_p = 1/p < 1$.

theorem PlaceQ.absValue_isNontrivial_infinite : infinite.absValue.IsNontrivial

The real (infinite) absolute value on $\mathbb{Q}$ is nontrivial: $|2|_\infty = 2 \ne 1$.

theorem PlaceQ.absValue_isNontrivial (v : PlaceQ) : v.absValue.IsNontrivial

Every place of $\mathbb{Q}$ yields a nontrivial absolute value.

theorem PlaceQ.padic_not_equiv_real (p : ℕ) [hp : Fact (Nat.Prime p)] : ¬(Rat.AbsoluteValue.padic p).IsEquiv Rat.AbsoluteValue.real

A $p$-adic absolute value is not equivalent to the real absolute value: any $p$ has $|p|_p < 1$ while $|p|_\infty > 1$.

theorem PlaceQ.padic_not_equiv_padic {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p ≠ q) : ¬(Rat.AbsoluteValue.padic p).IsEquiv (Rat.AbsoluteValue.padic q)

$p$-adic and $q$-adic absolute values are inequivalent whenever $p \ne q$.

theorem PlaceQ.absValue_pairwise_not_equiv (v w : PlaceQ) : v ≠ w → ¬v.absValue.IsEquiv w.absValue

Pairwise inequivalence of distinct places: the absolute values from any two distinct places of $\mathbb{Q}$ are not equivalent.

theorem weak_approximation_rationals {ι : Type u_1} [Fintype ι] (v : ι → PlaceQ) (hv : Function.Injective v) : DenseRange fun (x : ℚ) (i : ι) => ↑(WithAbs.toAbs (v i).absValue x)

Theorem 11.7 (Weak Approximation for $\mathbb{Q}$): the diagonal embedding $\mathbb{Q} \to \prod_i \widehat{\mathbb{Q}}_{v_i}$ has dense range for any finite injective family of places. Concretely, one can simultaneously approximate any tuple of elements in the completions by a single rational number.

theorem strong_approximation_integers {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℕ) [hp : ∀ (i : ι), Fact (Nat.Prime (p i))] (hinj : Function.Injective p) : DenseRange fun (z : ℤ) (i : ι) => ↑z

Theorem 11.8 (Strong Approximation for $\mathbb{Z}$): the diagonal embedding $\mathbb{Z} \to \prod_i \mathbb{Z}_{p_i}$ has dense range for any finite injective family of primes. The proof combines $p$-adic density with the Chinese Remainder Theorem.