p-adic numbers
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.
Important definitions
padic: the type of p-adic numberspadic_norm_e: the rational valued p-adic norm onℚ_p
Notation
We introduce the notation ℚ_[p] for the p-adic numbers.
Implementation notes
Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically
by taking [fact (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.
simp prefers padic_norm to padic_norm_e when possible.
Since padic_norm_e and ∥ ∥ have different types, simp does not rewrite one to the other.
Coercions from ℚ to ℚ_p are set up to work with the norm_cast tactic.
References
- [F. Q. Gouêva, p-adic numbers][gouvea1997]
- [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
- https://en.wikipedia.org/wiki/P-adic_number
Tags
p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion
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.
Equations
Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm to sequences.
Equations
- f.norm = dite (f ≈ 0) (λ (hf : f ≈ 0), 0) (λ (hf : ¬f ≈ 0), padic_norm p (⇑f (padic_seq.stationary_point hf)))
An auxiliary lemma for manipulating sequence indices.
An auxiliary lemma for manipulating sequence indices.
An auxiliary lemma for manipulating sequence indices.
Valuation on padic_seq
This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to padic_norm (f (max _ _ _)).
The discrete field structure on ℚ_p is inherited from the Cauchy completion construction.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Embeds the rational numbers in the p-adic numbers.
Equations
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 (∥ ∥).
Equations
Equations
- padic.lim_seq f = λ (n : ℕ), classical.some _
Equations
- padic.metric_space p = {to_has_dist := padic.has_dist p _inst_1, dist_self := _, eq_of_dist_eq_zero := _, dist_comm := _, dist_triangle := _, edist := λ (x y : ℚ_[p]), ennreal.of_real ((λ (x y : ℚ_[p]), ↑(padic_norm_e (x - y))) x y), edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : ℚ_[p]), ↑(padic_norm_e (x - y))) _ _ _, uniformity_dist := _}
Equations
- padic.normed_field p = {to_has_norm := padic.has_norm p _inst_1, to_field := padic.field _inst_1, to_metric_space := padic.metric_space p _inst_1, dist_eq := _, norm_mul' := _}
Equations
Equations
Equations
- padic.complete = {is_complete := _}
Valuation on ℚ_[p]
padic.valuation lifts the p-adic valuation on rationals to ℚ_[p].
Equations
- padic.valuation = quotient.lift padic_seq.valuation padic.valuation._proof_1