mathlib documentation

number_theory.padics.padic_integers

p-adic integers #

This file defines the p-adic integers ℤ_p as the subtype of ℚ_p with norm ≤ 1. We show that ℤ_p

is complete
is nonarchimedean
is a normed ring
is a local ring
is a discrete valuation ring

The relation between ℤ_[p] and zmod p is established in another file.

Important definitions #

padic_int : the type of p-adic numbers

Notation #

We introduce the notation ℤ_[p] for the p-adic integers.

Implementation notes #

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking `[fact (nat.prime p)] as a type class argument.

Coercions into ℤ_p are set up to work with the norm_cast tactic.

References #

Tags #

p-adic, p adic, padic, p-adic integer

def padic_int (p : ℕ) [fact (nat.prime p)] :

Type

The p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1.

Equations

ℤ_[p] = {x // ∥x∥ ≤ 1}

Instances for padic_int

Ring structure and coercion to `ℚ_[p]` #

@[protected, instance]

def padic_int.padic.has_coe {p : ℕ} [fact (nat.prime p)] :

has_coe ℤ_[p] ℚ_[p]

Equations

padic_int.padic.has_coe = {coe := subtype.val (λ (x : ℚ_[p]), ∥x∥ ≤ 1)}

theorem padic_int.ext {p : ℕ} [fact (nat.prime p)] {x y : ℤ_[p]} :

↑x = ↑y → x = y

@[protected, instance]

noncomputable def padic_int.has_add {p : ℕ} [fact (nat.prime p)] :

has_add ℤ_[p]

Addition on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_add = {add := λ (_x : ℤ_[p]), padic_int.has_add._match_2 _x}
padic_int.has_add._match_2 ⟨x, hx⟩ = λ (_x : ℤ_[p]), padic_int.has_add._match_1 x hx _x
padic_int.has_add._match_1 x hx ⟨y, hy⟩ = ⟨x + y, _⟩

@[protected, instance]

noncomputable def padic_int.has_mul {p : ℕ} [fact (nat.prime p)] :

has_mul ℤ_[p]

Multiplication on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_mul = {mul := λ (_x : ℤ_[p]), padic_int.has_mul._match_2 _x}
padic_int.has_mul._match_2 ⟨x, hx⟩ = λ (_x : ℤ_[p]), padic_int.has_mul._match_1 x hx _x
padic_int.has_mul._match_1 x hx ⟨y, hy⟩ = ⟨x * y, _⟩

@[protected, instance]

noncomputable def padic_int.has_neg {p : ℕ} [fact (nat.prime p)] :

has_neg ℤ_[p]

Negation on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_neg = {neg := λ (_x : ℤ_[p]), padic_int.has_neg._match_1 _x}
padic_int.has_neg._match_1 ⟨x, hx⟩ = ⟨-x, _⟩

@[protected, instance]

noncomputable def padic_int.has_sub {p : ℕ} [fact (nat.prime p)] :

has_sub ℤ_[p]

Subtraction on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_sub = {sub := λ (_x : ℤ_[p]), padic_int.has_sub._match_2 _x}
padic_int.has_sub._match_2 ⟨x, hx⟩ = λ (_x : ℤ_[p]), padic_int.has_sub._match_1 x hx _x
padic_int.has_sub._match_1 x hx ⟨y, hy⟩ = ⟨x - y, _⟩

@[protected, instance]

noncomputable def padic_int.has_zero {p : ℕ} [fact (nat.prime p)] :

has_zero ℤ_[p]

Zero on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_zero = {zero := ⟨0, _⟩}

@[protected, instance]

noncomputable def padic_int.inhabited {p : ℕ} [fact (nat.prime p)] :

inhabited ℤ_[p]

Equations

padic_int.inhabited = {default := 0}

@[protected, instance]

noncomputable def padic_int.has_one {p : ℕ} [fact (nat.prime p)] :

has_one ℤ_[p]

One on ℤ_p is inherited from ℚ_p.

Equations

padic_int.has_one = {one := ⟨1, _⟩}

@[simp]

theorem padic_int.mk_zero {p : ℕ} [fact (nat.prime p)] {h : ∥0∥ ≤ 1} :

⟨0, h⟩ = 0

@[simp]

theorem padic_int.val_eq_coe {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :

@[simp, norm_cast]

theorem padic_int.coe_add {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :

↑(z1 + z2) = ↑z1 + ↑z2

@[simp, norm_cast]

theorem padic_int.coe_mul {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :

↑(z1 * z2) = ↑z1 * ↑z2

@[simp, norm_cast]

theorem padic_int.coe_neg {p : ℕ} [fact (nat.prime p)] (z1 : ℤ_[p]) :

↑-z1 = -↑z1

@[simp, norm_cast]

theorem padic_int.coe_sub {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :

↑(z1 - z2) = ↑z1 - ↑z2

@[simp, norm_cast]

theorem padic_int.coe_one {p : ℕ} [fact (nat.prime p)] :

↑1 = 1

@[simp, norm_cast]

theorem padic_int.coe_coe {p : ℕ} [fact (nat.prime p)] (n : ℕ) :

@[simp, norm_cast]

theorem padic_int.coe_coe_int {p : ℕ} [fact (nat.prime p)] (z : ℤ) :

@[simp, norm_cast]

theorem padic_int.coe_zero {p : ℕ} [fact (nat.prime p)] :

↑0 = 0

@[protected, instance]

noncomputable def padic_int.ring {p : ℕ} [fact (nat.prime p)] :

Equations

padic_int.ring = {add := has_add.add padic_int.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add padic_int.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg padic_int.has_neg, sub := has_sub.sub padic_int.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg padic_int.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul padic_int.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul padic_int.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

def padic_int.coe.ring_hom {p : ℕ} [fact (nat.prime p)] :

ℤ_[p] →+* ℚ_[p]

The coercion from ℤ[p] to ℚ[p] as a ring homomorphism.

Equations

padic_int.coe.ring_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp, norm_cast]

theorem padic_int.coe_pow {p : ℕ} [fact (nat.prime p)] (x : ℤ_[p]) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

@[simp]

theorem padic_int.mk_coe {p : ℕ} [fact (nat.prime p)] (k : ℤ_[p]) :

⟨↑k, _⟩ = k

noncomputable def padic_int.inv {p : ℕ} [fact (nat.prime p)] :

ℤ_[p] → ℤ_[p]

The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the inverse is defined to be 0.

Equations

padic_int.inv ⟨k, _x⟩ = dite (∥k∥ = 1) (λ (h : ∥k∥ = 1), ⟨1 / k, _⟩) (λ (h : ¬∥k∥ = 1), 0)

@[protected, instance]

def padic_int.char_zero {p : ℕ} [fact (nat.prime p)] :

char_zero ℤ_[p]

@[simp, norm_cast]

theorem padic_int.coe_int_eq {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ) :

↑z1 = ↑z2 ↔ z1 = z2

def padic_int.of_int_seq {p : ℕ} [fact (nat.prime p)] (seq : ℕ → ℤ) (h : is_cau_seq (padic_norm p) (λ (n : ℕ), ↑(seq n))) :

A sequence of integers that is Cauchy with respect to the p-adic norm converges to a p-adic integer.

Equations

padic_int.of_int_seq seq h = ⟨⟦⟨λ (n : ℕ), ↑(seq n), h⟩⟧, _⟩

Instances #

We now show that ℤ_[p] is a

complete metric space
normed ring
integral domain

@[protected, instance]

noncomputable def padic_int.metric_space (p : ℕ) [fact (nat.prime p)] :

metric_space ℤ_[p]

Equations

padic_int.metric_space p = subtype.metric_space

@[protected, instance]

def padic_int.complete_space (p : ℕ) [fact (nat.prime p)] :

complete_space ℤ_[p]

@[protected, instance]

noncomputable def padic_int.has_norm (p : ℕ) [fact (nat.prime p)] :

has_norm ℤ_[p]

Equations

padic_int.has_norm p = {norm := λ (z : ℤ_[p]), ∥↑z∥}

@[protected]

theorem padic_int.mul_comm {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :

z1 * z2 = z2 * z1

@[protected]

theorem padic_int.zero_ne_one {p : ℕ} [fact (nat.prime p)] :

0 ≠ 1

@[protected]

theorem padic_int.eq_zero_or_eq_zero_of_mul_eq_zero {p : ℕ} [fact (nat.prime p)] (a b : ℤ_[p]) :

a * b = 0 → a = 0 ∨ b = 0

theorem padic_int.norm_def {p : ℕ} [fact (nat.prime p)] {z : ℤ_[p]} :

∥z∥ = ∥↑z∥

@[protected, instance]

noncomputable def padic_int.normed_comm_ring (p : ℕ) [fact (nat.prime p)] :

normed_comm_ring ℤ_[p]

Equations

padic_int.normed_comm_ring p = {to_normed_ring := {to_has_norm := padic_int.has_norm p _inst_1, to_ring := padic_int.ring _inst_1, to_metric_space := padic_int.metric_space p _inst_1, dist_eq := _, norm_mul := _}, mul_comm := _}

@[protected, instance]

def padic_int.norm_one_class (p : ℕ) [fact (nat.prime p)] :

norm_one_class ℤ_[p]

@[protected, instance]

def padic_int.is_absolute_value (p : ℕ) [fact (nat.prime p)] :

is_absolute_value (λ (z : ℤ_[p]), ∥z∥)

@[protected, instance]

def padic_int.is_domain {p : ℕ} [fact (nat.prime p)] :

is_domain ℤ_[p]

Norm #

theorem padic_int.norm_le_one {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :

@[simp]

theorem padic_int.norm_mul {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :

∥z1 * z2∥ = ∥z1∥ * ∥z2∥

@[simp]

theorem padic_int.norm_pow {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) (n : ℕ) :

∥z ^ n∥ = ∥z∥ ^ n

theorem padic_int.nonarchimedean {p : ℕ} [fact (nat.prime p)] (q r : ℤ_[p]) :

∥q + r∥ ≤ linear_order.max ∥q∥ ∥r∥

theorem padic_int.norm_add_eq_max_of_ne {p : ℕ} [fact (nat.prime p)] {q r : ℤ_[p]} :

∥q∥ ≠ ∥r∥ → ∥q + r∥ = linear_order.max ∥q∥ ∥r∥

theorem padic_int.norm_eq_of_norm_add_lt_right {p : ℕ} [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : ∥z1 + z2∥ < ∥z2∥) :

∥z1∥ = ∥z2∥

theorem padic_int.norm_eq_of_norm_add_lt_left {p : ℕ} [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : ∥z1 + z2∥ < ∥z1∥) :

∥z1∥ = ∥z2∥

@[simp]

theorem padic_int.padic_norm_e_of_padic_int {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :

∥↑z∥ = ∥z∥

theorem padic_int.norm_int_cast_eq_padic_norm {p : ℕ} [fact (nat.prime p)] (z : ℤ) :

∥↑z∥ = ∥↑z∥

@[simp]

theorem padic_int.norm_eq_padic_norm {p : ℕ} [fact (nat.prime p)] {q : ℚ_[p]} (hq : ∥q∥ ≤ 1) :

∥⟨q, hq⟩∥ = ∥q∥

@[simp]

theorem padic_int.norm_p {p : ℕ} [fact (nat.prime p)] :

∥↑p∥ = (↑p)⁻¹

@[simp]

theorem padic_int.norm_p_pow {p : ℕ} [fact (nat.prime p)] (n : ℕ) :

∥↑p ^ n∥ = ↑p ^ -↑n

@[protected, instance]

def padic_int.complete (p : ℕ) [fact (nat.prime p)] :

cau_seq.is_complete ℤ_[p] has_norm.norm

theorem padic_int.exists_pow_neg_lt (p : ℕ) [hp_prime : fact (nat.prime p)] {ε : ℝ} (hε : 0 < ε) :

∃ (k : ℕ), ↑p ^ -↑k < ε

theorem padic_int.exists_pow_neg_lt_rat (p : ℕ) [hp_prime : fact (nat.prime p)] {ε : ℚ} (hε : 0 < ε) :

∃ (k : ℕ), ↑p ^ -↑k < ε

theorem padic_int.norm_int_lt_one_iff_dvd {p : ℕ} [hp_prime : fact (nat.prime p)] (k : ℤ) :

∥↑k∥ < 1 ↔ ↑p ∣ k

theorem padic_int.norm_int_le_pow_iff_dvd {p : ℕ} [hp_prime : fact (nat.prime p)] {k : ℤ} {n : ℕ} :

∥↑k∥ ≤ ↑p ^ -↑n ↔ ↑p ^ n ∣ k

Valuation on `ℤ_[p]` #

noncomputable def padic_int.valuation {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :

padic_int.valuation lifts the p-adic valuation on ℚ to ℤ_[p].

Equations

x.valuation = ↑x.valuation

theorem padic_int.norm_eq_pow_val {p : ℕ} [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :

∥x∥ = ↑p ^ -x.valuation

@[simp]

theorem padic_int.valuation_zero {p : ℕ} [hp_prime : fact (nat.prime p)] :

0.valuation = 0

@[simp]

theorem padic_int.valuation_one {p : ℕ} [hp_prime : fact (nat.prime p)] :

1.valuation = 0

@[simp]

theorem padic_int.valuation_p {p : ℕ} [hp_prime : fact (nat.prime p)] :

↑p.valuation = 1

theorem padic_int.valuation_nonneg {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :

0 ≤ x.valuation

@[simp]

theorem padic_int.valuation_p_pow_mul {p : ℕ} [hp_prime : fact (nat.prime p)] (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) :

(↑p ^ n * c).valuation = ↑n + c.valuation

Units of `ℤ_[p]` #

theorem padic_int.mul_inv {p : ℕ} [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :

∥z∥ = 1 → z * z.inv = 1

theorem padic_int.inv_mul {p : ℕ} [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} (hz : ∥z∥ = 1) :

z.inv * z = 1

theorem padic_int.is_unit_iff {p : ℕ} [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :

is_unit z ↔ ∥z∥ = 1

theorem padic_int.norm_lt_one_add {p : ℕ} [hp_prime : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz1 : ∥z1∥ < 1) (hz2 : ∥z2∥ < 1) :

∥z1 + z2∥ < 1

theorem padic_int.norm_lt_one_mul {p : ℕ} [hp_prime : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz2 : ∥z2∥ < 1) :

∥z1 * z2∥ < 1

@[simp]

theorem padic_int.mem_nonunits {p : ℕ} [hp_prime : fact (nat.prime p)] {z : ℤ_[p]} :

z ∈ nonunits ℤ_[p] ↔ ∥z∥ < 1

noncomputable def padic_int.mk_units {p : ℕ} [hp_prime : fact (nat.prime p)] {u : ℚ_[p]} (h : ∥u∥ = 1) :

A p-adic number u with ∥u∥ = 1 is a unit of ℤ_[p].

Equations

padic_int.mk_units h = let z : ℤ_[p] := ⟨u, _⟩ in {val := z, inv := z.inv, val_inv := _, inv_val := _}

@[simp]

theorem padic_int.mk_units_eq {p : ℕ} [hp_prime : fact (nat.prime p)] {u : ℚ_[p]} (h : ∥u∥ = 1) :

↑↑(padic_int.mk_units h) = u

@[simp]

theorem padic_int.norm_units {p : ℕ} [hp_prime : fact (nat.prime p)] (u : ℤ_[p]ˣ) :

noncomputable def padic_int.unit_coeff {p : ℕ} [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :

unit_coeff hx is the unit u in the unique representation x = u * p ^ n. See unit_coeff_spec.

Equations

padic_int.unit_coeff hx = let u : ℚ_[p] := ↑x * ↑p ^ -x.valuation in have hu : ∥u∥ = 1, from _, padic_int.mk_units hu

@[simp]

theorem padic_int.unit_coeff_coe {p : ℕ} [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :

↑(padic_int.unit_coeff hx) = ↑x * ↑p ^ -x.valuation

theorem padic_int.unit_coeff_spec {p : ℕ} [hp_prime : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :

x = ↑(padic_int.unit_coeff hx) * ↑p ^ x.valuation.nat_abs

Various characterizations of open unit balls #

theorem padic_int.norm_le_pow_iff_le_valuation {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :

∥x∥ ≤ ↑p ^ -↑n ↔ ↑n ≤ x.valuation

theorem padic_int.mem_span_pow_iff_le_valuation {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :

x ∈ ideal.span {↑p ^ n} ↔ ↑n ≤ x.valuation

theorem padic_int.norm_le_pow_iff_mem_span_pow {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ℕ) :

∥x∥ ≤ ↑p ^ -↑n ↔ x ∈ ideal.span {↑p ^ n}

theorem padic_int.norm_le_pow_iff_norm_lt_pow_add_one {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ℤ) :

∥x∥ ≤ ↑p ^ n ↔ ∥x∥ < ↑p ^ (n + 1)

theorem padic_int.norm_lt_pow_iff_norm_le_pow_sub_one {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) (n : ℤ) :

∥x∥ < ↑p ^ n ↔ ∥x∥ ≤ ↑p ^ (n - 1)

theorem padic_int.norm_lt_one_iff_dvd {p : ℕ} [hp_prime : fact (nat.prime p)] (x : ℤ_[p]) :

∥x∥ < 1 ↔ ↑p ∣ x

@[simp]

theorem padic_int.pow_p_dvd_int_iff {p : ℕ} [hp_prime : fact (nat.prime p)] (n : ℕ) (a : ℤ) :

↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a

Discrete valuation ring #

@[protected, instance]

def padic_int.local_ring {p : ℕ} [hp_prime : fact (nat.prime p)] :

local_ring ℤ_[p]

theorem padic_int.p_nonnunit {p : ℕ} [hp_prime : fact (nat.prime p)] :

↑p ∈ nonunits ℤ_[p]

theorem padic_int.maximal_ideal_eq_span_p {p : ℕ} [hp_prime : fact (nat.prime p)] :

local_ring.maximal_ideal ℤ_[p] = ideal.span {↑p}

theorem padic_int.prime_p {p : ℕ} [hp_prime : fact (nat.prime p)] :

theorem padic_int.irreducible_p {p : ℕ} [hp_prime : fact (nat.prime p)] :

irreducible ↑p

@[protected, instance]

def padic_int.discrete_valuation_ring {p : ℕ} [hp_prime : fact (nat.prime p)] :

discrete_valuation_ring ℤ_[p]

theorem padic_int.ideal_eq_span_pow_p {p : ℕ} [hp_prime : fact (nat.prime p)] {s : ideal ℤ_[p]} (hs : s ≠ ⊥) :

∃ (n : ℕ), s = ideal.span {↑p ^ n}

@[protected, instance]

def padic_int.is_adic_complete {p : ℕ} [hp_prime : fact (nat.prime p)] :

is_adic_complete (local_ring.maximal_ideal ℤ_[p]) ℤ_[p]