This file defines the p-adic numbers (rationals) ℚ_p as the completion of ℚ with respect to the p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_p, that ℚ is embedded in ℚ_p, and that ℚ_p is Cauchy complete.
We introduce the notation ℚ_[p] for the p-adic numbers.
Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking (prime p) as a type class argument.
We use the same concrete Cauchy sequence construction that is used to construct ℝ. ℚ_p inherits a field structure from this construction. The extension of the norm on ℚ to ℚ_p is not analogous to extending the absolute value to ℝ, and hence the proof that ℚ_p is complete is different from the proof that ℝ is complete.
A small special-purpose simplification tactic, padic_index_simp, is used to manipulate sequence indices in the proof that the norm extends.
padic_norm_e is the rational-valued p-adic norm on ℚ_p. To instantiate ℚ_p as a normed field, we must cast this into a ℝ-valued norm. The ℝ-valued norm, using notation ∥ ∥ from normed spaces, is the canonical representation of this norm.
Coercions from ℚ to ℚ_p are set up to work with the norm_cast tactic.
p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion
The type of Cauchy sequences of rationals with respect to the p-adic norm.
The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually constant.
For all n ≥ stationary_point f hf, the p-adic norm of f n is the same.
Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm to sequences.
An auxiliary lemma for manipulating sequence indices.
An auxiliary lemma for manipulating sequence indices.
An auxiliary lemma for manipulating sequence indices.
This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to padic_norm (f (max _ _ _)).
The p-adic numbers Q_[p] are the Cauchy completion of ℚ with respect to the p-adic norm.
The discrete field structure on ℚ_p is inherited from the Cauchy completion construction.
Builds the equivalence class of a Cauchy sequence of rationals.
Embeds the rational numbers in the p-adic numbers.
The rational-valued p-adic norm on ℚ_p is lifted from the norm on Cauchy sequences. The canonical form of this function is the normed space instance, with notation ∥ ∥.
Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (∥ ∥).
Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (∥ ∥).
Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (∥ ∥).