mathlib documentation

data.padics.padic_numbers

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

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

Tags

p-adic, p adic, padic, norm, valuation, cauchy, completion, p-adic completion

def padic_seq  :
→ Type

The type of Cauchy sequences of rationals with respect to the p-adic norm.

Equations
theorem padic_seq.stationary {p : } [fact (nat.prime p)] {f : cau_seq (padic_norm p)} :
¬f 0(∃ (N : ), ∀ (m n : ), N mN npadic_norm p (f n) = padic_norm p (f m))

The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually constant.

def padic_seq.stationary_point {p : } [fact (nat.prime p)] {f : padic_seq p} :
¬f 0

For all n ≥ stationary_point f hf, the p-adic norm of f n is the same.

Equations
def padic_seq.norm {p : } [fact (nat.prime p)] :

Since the norm of the entries of a Cauchy sequence is eventually stationary, we can lift the norm to sequences.

Equations
theorem padic_seq.norm_zero_iff {p : } [fact (nat.prime p)] (f : padic_seq p) :
f.norm = 0 f 0

theorem padic_seq.equiv_zero_of_val_eq_of_equiv_zero {p : } [fact (nat.prime p)] {f g : padic_seq p} :
(∀ (k : ), padic_norm p (f k) = padic_norm p (g k))f 0g 0

theorem padic_seq.norm_eq_norm_app_of_nonzero {p : } [fact (nat.prime p)] {f : padic_seq p} :
¬f 0(∃ (k : ), f.norm = padic_norm p k k 0)

theorem padic_seq.norm_nonneg {p : } [fact (nat.prime p)] (f : padic_seq p) :
0 f.norm

theorem padic_seq.lift_index_left_left {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v2 v3 : ) :

An auxiliary lemma for manipulating sequence indices.

theorem padic_seq.lift_index_left {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v1 v3 : ) :

An auxiliary lemma for manipulating sequence indices.

theorem padic_seq.lift_index_right {p : } [fact (nat.prime p)] {f : padic_seq p} (hf : ¬f 0) (v1 v2 : ) :

An auxiliary lemma for manipulating sequence indices.

Valuation on padic_seq

def padic_seq.valuation {p : } [fact (nat.prime p)] :

The p-adic valuation on lifts to padic_seq p. valuation f is defined to be the valuation of the (-valued) stationary point of f.

Equations
theorem padic_seq.norm_eq_pow_val {p : } [fact (nat.prime p)] {f : padic_seq p} :
¬f 0f.norm = p ^ -f.valuation

theorem padic_seq.val_eq_iff_norm_eq {p : } [fact (nat.prime p)] {f g : padic_seq p} :
¬f 0¬g 0(f.valuation = g.valuation f.norm = g.norm)

This is a special-purpose tactic that lifts padic_norm (f (stationary_point f)) to padic_norm (f (max _ _ _)).

theorem padic_seq.norm_mul {p : } [hp : fact (nat.prime p)] (f g : padic_seq p) :
(f * g).norm = (f.norm) * g.norm

theorem padic_seq.norm_values_discrete {p : } [hp : fact (nat.prime p)] (a : padic_seq p) :
¬a 0(∃ (z : ), a.norm = p ^ -z)

theorem padic_seq.norm_one {p : } [hp : fact (nat.prime p)] :
1.norm = 1

theorem padic_seq.norm_equiv {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} :
f gf.norm = g.norm

theorem padic_seq.norm_nonarchimedean {p : } [hp : fact (nat.prime p)] (f g : padic_seq p) :
(f + g).norm max f.norm g.norm

theorem padic_seq.norm_eq {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} :
(∀ (k : ), padic_norm p (f k) = padic_norm p (g k))f.norm = g.norm

theorem padic_seq.norm_neg {p : } [hp : fact (nat.prime p)] (a : padic_seq p) :
(-a).norm = a.norm

theorem padic_seq.norm_eq_of_add_equiv_zero {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} :
f + g 0f.norm = g.norm

theorem padic_seq.add_eq_max_of_ne {p : } [hp : fact (nat.prime p)] {f g : padic_seq p} :
f.norm g.norm(f + g).norm = max f.norm g.norm

def padic (p : ) [fact (nat.prime p)] :
Type

The p-adic numbers Q_[p] are the Cauchy completion of with respect to the p-adic norm.

Equations
@[instance]
def padic.field {p : } [fact (nat.prime p)] :

The discrete field structure on ℚ_p is inherited from the Cauchy completion construction.

Equations
@[instance]

Equations
@[instance]

Equations
def padic.mk {p : } [fact (nat.prime p)] :

Builds the equivalence class of a Cauchy sequence of rationals.

Equations
theorem padic.mk_eq (p : ) [fact (nat.prime p)] {f g : padic_seq p} :

def padic.of_rat (p : ) [fact (nat.prime p)] :
ℚ_[p]

Embeds the rational numbers in the p-adic numbers.

Equations
@[simp]
theorem padic.of_rat_add (p : ) [fact (nat.prime p)] (x y : ) :

@[simp]
theorem padic.of_rat_neg (p : ) [fact (nat.prime p)] (x : ) :

@[simp]
theorem padic.of_rat_mul (p : ) [fact (nat.prime p)] (x y : ) :

@[simp]
theorem padic.of_rat_sub (p : ) [fact (nat.prime p)] (x y : ) :

@[simp]
theorem padic.of_rat_div (p : ) [fact (nat.prime p)] (x y : ) :

@[simp]
theorem padic.of_rat_one (p : ) [fact (nat.prime p)] :

@[simp]
theorem padic.of_rat_zero (p : ) [fact (nat.prime p)] :

theorem padic.cast_eq_of_rat (p : ) [fact (nat.prime p)] (q : ) :

theorem padic.coe_add (p : ) [fact (nat.prime p)] {x y : } :
(x + y) = x + y

theorem padic.coe_neg (p : ) [fact (nat.prime p)] {x : } :

theorem padic.coe_mul (p : ) [fact (nat.prime p)] {x y : } :
x * y = (x) * y

theorem padic.coe_sub (p : ) [fact (nat.prime p)] {x y : } :
(x - y) = x - y

theorem padic.coe_div (p : ) [fact (nat.prime p)] {x y : } :
(x / y) = x / y

theorem padic.coe_one (p : ) [fact (nat.prime p)] :
1 = 1

theorem padic.coe_zero (p : ) [fact (nat.prime p)] :
0 = 0

theorem padic.of_rat_eq (p : ) [fact (nat.prime p)] {q r : } :

theorem padic.coe_inj (p : ) [fact (nat.prime p)] {q r : } :
q = r q = r

@[instance]

def padic_norm_e {p : } [hp : fact (nat.prime p)] :
ℚ_[p]

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 ∥ ∥.

Equations
theorem padic_norm_e.defn {p : } [fact (nat.prime p)] (f : padic_seq p) {ε : } :
0 < ε(∃ (N : ), ∀ (i : ), i Npadic_norm_e (f - (f i)) < ε)

theorem padic_norm_e.nonneg {p : } [fact (nat.prime p)] (q : ℚ_[p]) :

theorem padic_norm_e.zero_def {p : } [fact (nat.prime p)] :

theorem padic_norm_e.zero_iff {p : } [fact (nat.prime p)] (q : ℚ_[p]) :

@[simp]
theorem padic_norm_e.zero {p : } [fact (nat.prime p)] :

@[simp]
theorem padic_norm_e.one' {p : } [fact (nat.prime p)] :

Theorems about padic_norm_e are named with a ' so the names do not conflict with the equivalent theorems about norm (∥ ∥).

@[simp]
theorem padic_norm_e.neg {p : } [fact (nat.prime p)] (q : ℚ_[p]) :

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 (∥ ∥).

theorem padic_norm_e.triangle_ineq {p : } [fact (nat.prime p)] (x y z : ℚ_[p]) :

theorem padic_norm_e.mul' {p : } [fact (nat.prime p)] (q r : ℚ_[p]) :

@[simp]

theorem padic_norm_e.image' {p : } [fact (nat.prime p)] {q : ℚ_[p]} :
q 0(∃ (n : ), padic_norm_e q = p ^ -n)

theorem padic_norm_e.sub_rev {p : } [fact (nat.prime p)] (q r : ℚ_[p]) :

theorem padic.rat_dense' {p : } [fact (nat.prime p)] (q : ℚ_[p]) {ε : } :
0 < ε(∃ (r : ), padic_norm_e (q - r) < ε)

lim_seq f, for f a Cauchy sequence of p-adic numbers, is a sequence of rationals with the same limit point as f.

Equations
theorem padic.exi_rat_seq_conv {p : } [fact (nat.prime p)] (f : cau_seq ℚ_[p] padic_norm_e) {ε : } :
0 < ε(∃ (N : ), ∀ (i : ), i Npadic_norm_e (f i - (padic.lim_seq f i)) < ε)

theorem padic.complete' {p : } [fact (nat.prime p)] (f : cau_seq ℚ_[p] padic_norm_e) :
∃ (q : ℚ_[p]), ∀ (ε : ), ε > 0(∃ (N : ), ∀ (i : ), i Npadic_norm_e (q - f i) < ε)

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

theorem padic.rat_dense {p : } {hp : fact (nat.prime p)} (q : ℚ_[p]) {ε : } :
0 < ε(∃ (r : ), q - r < ε)

@[simp]
theorem padic_norm_e.mul {p : } [hp : fact (nat.prime p)] (q r : ℚ_[p]) :

theorem padic_norm_e.is_norm {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :

theorem padic_norm_e.nonarchimedean {p : } [hp : fact (nat.prime p)] (q r : ℚ_[p]) :

theorem padic_norm_e.add_eq_max_of_ne {p : } [hp : fact (nat.prime p)] {q r : ℚ_[p]} :

@[simp]
theorem padic_norm_e.eq_padic_norm {p : } [hp : fact (nat.prime p)] (q : ) :

@[simp]
theorem padic_norm_e.norm_p {p : } [hp : fact (nat.prime p)] :

theorem padic_norm_e.norm_p_lt_one {p : } [hp : fact (nat.prime p)] :

@[simp]
theorem padic_norm_e.norm_p_pow {p : } [hp : fact (nat.prime p)] (n : ) :

theorem padic_norm_e.image {p : } [hp : fact (nat.prime p)] {q : ℚ_[p]} :
q 0(∃ (n : ), q = (p ^ -n))

theorem padic_norm_e.is_rat {p : } [hp : fact (nat.prime p)] (q : ℚ_[p]) :
∃ (q' : ), q = q'

def padic_norm_e.rat_norm {p : } [hp : fact (nat.prime p)] :
ℚ_[p]

rat_norm q, for a p-adic number q is the p-adic norm of q, as rational number.

The lemma padic_norm_e.eq_rat_norm asserts ∥q∥ = rat_norm q.

Equations
theorem padic_norm_e.norm_rat_le_one {p : } [hp : fact (nat.prime p)] {q : } :

theorem padic_norm_e.norm_int_le_one {p : } [hp : fact (nat.prime p)] (z : ) :

theorem padic_norm_e.norm_int_le_pow_iff_dvd {p : } [hp : fact (nat.prime p)] (k : ) (n : ) :

theorem padic_norm_e.eq_of_norm_add_lt_right {p : } {hp : fact (nat.prime p)} {z1 z2 : ℚ_[p]} :
z1 + z2 < z2z1 = z2

theorem padic_norm_e.eq_of_norm_add_lt_left {p : } {hp : fact (nat.prime p)} {z1 z2 : ℚ_[p]} :
z1 + z2 < z1z1 = z2

theorem padic.padic_norm_e_lim_le {p : } [fact (nat.prime p)] {f : cau_seq ℚ_[p] norm} {a : } :
0 < a(∀ (i : ), f i a)f.lim a

Valuation on ℚ_[p]

def padic.valuation {p : } [fact (nat.prime p)] :
ℚ_[p]

padic.valuation lifts the p-adic valuation on rationals to ℚ_[p].

Equations
@[simp]
theorem padic.valuation_zero {p : } [fact (nat.prime p)] :

@[simp]
theorem padic.valuation_one {p : } [fact (nat.prime p)] :

theorem padic.norm_eq_pow_val {p : } [fact (nat.prime p)] {x : ℚ_[p]} :
x 0x = p ^ -x.valuation

@[simp]
theorem padic.valuation_p {p : } [fact (nat.prime p)] :