mathlib3 documentation

number_theory.padics.padic_integers

p-adic integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Important definitions #

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 p.prime] 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

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

The p-adic integers ℤ_[p] are the p-adic numbers with norm ≤ 1.

Equations
Instances for padic_int

Ring structure and coercion to ℚ_[p] #

source
@[protected, instance]
def padic_int.padic.has_coe {p : ℕ} [fact (nat.prime p)] :
has_coe ℤ_[p] ℚ_[p]
Equations
source
theorem padic_int.ext {p : ℕ} [fact (nat.prime p)] {x y : ℤ_[p]} :
↑x = ↑y → x = y
source
def padic_int.subring (p : ℕ) [fact (nat.prime p)] :
subring ℚ_[p]

The p-adic integers as a subring of ℚ_[p].

Equations
source
@[simp]
theorem padic_int.mem_subring_iff (p : ℕ) [fact (nat.prime p)] {x : ℚ_[p]} :
x ∈ padic_int.subring p ↔ ‖x‖ ≤ 1
source
@[protected, instance]
def padic_int.has_add {p : ℕ} [fact (nat.prime p)] :
has_add ℤ_[p]

Addition on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[protected, instance]
def padic_int.has_mul {p : ℕ} [fact (nat.prime p)] :
has_mul ℤ_[p]

Multiplication on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[protected, instance]
def padic_int.has_neg {p : ℕ} [fact (nat.prime p)] :
has_neg ℤ_[p]

Negation on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[protected, instance]
def padic_int.has_sub {p : ℕ} [fact (nat.prime p)] :
has_sub ℤ_[p]

Subtraction on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[protected, instance]
def padic_int.has_zero {p : ℕ} [fact (nat.prime p)] :
has_zero ℤ_[p]

Zero on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[protected, instance]
def padic_int.inhabited {p : ℕ} [fact (nat.prime p)] :
inhabited ℤ_[p]
Equations
source
@[protected, instance]
def padic_int.has_one {p : ℕ} [fact (nat.prime p)] :
has_one ℤ_[p]

One on ℤ_[p] is inherited from ℚ_[p].

Equations
source
@[simp]
theorem padic_int.mk_zero {p : ℕ} [fact (nat.prime p)] {h : ‖0‖ ≤ 1} :
⟨0, h⟩ = 0
source
@[simp]
theorem padic_int.val_eq_coe {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
z.val = ↑z
source
@[simp, norm_cast]
theorem padic_int.coe_add {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
↑(z1 + z2) = ↑z1 + ↑z2
source
@[simp, norm_cast]
theorem padic_int.coe_mul {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
↑(z1 * z2) = ↑z1 * ↑z2
source
@[simp, norm_cast]
theorem padic_int.coe_neg {p : ℕ} [fact (nat.prime p)] (z1 : ℤ_[p]) :
↑-z1 = -↑z1
source
@[simp, norm_cast]
theorem padic_int.coe_sub {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
↑(z1 - z2) = ↑z1 - ↑z2
source
@[simp, norm_cast]
theorem padic_int.coe_one {p : ℕ} [fact (nat.prime p)] :
↑1 = 1
source
@[simp, norm_cast]
theorem padic_int.coe_zero {p : ℕ} [fact (nat.prime p)] :
↑0 = 0
source
theorem padic_int.coe_eq_zero {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
↑z = 0 ↔ z = 0
source
theorem padic_int.coe_ne_zero {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
↑z ≠ 0 ↔ z ≠ 0
source
@[protected, instance]
noncomputable def padic_int.add_comm_group {p : ℕ} [fact (nat.prime p)] :
add_comm_group ℤ_[p]
Equations
source
@[protected, instance]
def padic_int.comm_ring {p : ℕ} [fact (nat.prime p)] :
comm_ring ℤ_[p]
Equations
source
@[simp, norm_cast]
theorem padic_int.coe_nat_cast {p : ℕ} [fact (nat.prime p)] (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem padic_int.coe_int_cast {p : ℕ} [fact (nat.prime p)] (z : ℤ) :
↑↑z = ↑z
source
def padic_int.coe.ring_hom {p : ℕ} [fact (nat.prime p)] :
ℤ_[p] →+* ℚ_[p]

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

Equations
source
@[simp, norm_cast]
theorem padic_int.coe_pow {p : ℕ} [fact (nat.prime p)] (x : ℤ_[p]) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
@[simp]
theorem padic_int.mk_coe {p : ℕ} [fact (nat.prime p)] (k : ℤ_[p]) :
⟨↑k, _⟩ = k
source
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
source
@[protected, instance]
def padic_int.char_zero {p : ℕ} [fact (nat.prime p)] :
char_zero ℤ_[p]
source
@[simp, norm_cast]
theorem padic_int.coe_int_eq {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ) :
↑z1 = ↑z2 ↔ z1 = z2
source
def padic_int.of_int_seq {p : ℕ} [fact (nat.prime p)] (seq : ℕ → ℤ) (h : is_cau_seq (padic_norm p) (λ (n : ℕ), ↑(seq n))) :
ℤ_[p]

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

Equations

Instances #

We now show that ℤ_[p] is a

source
@[protected, instance]
noncomputable def padic_int.metric_space (p : ℕ) [fact (nat.prime p)] :
metric_space ℤ_[p]
Equations
source
@[protected, instance]
def padic_int.complete_space (p : ℕ) [fact (nat.prime p)] :
complete_space ℤ_[p]
source
@[protected, instance]
noncomputable def padic_int.has_norm (p : ℕ) [fact (nat.prime p)] :
has_norm ℤ_[p]
Equations
source
theorem padic_int.norm_def {p : ℕ} [fact (nat.prime p)] {z : ℤ_[p]} :
‖z‖ = ‖↑z‖
source
@[protected, instance]
noncomputable def padic_int.normed_comm_ring (p : ℕ) [fact (nat.prime p)] :
normed_comm_ring ℤ_[p]
Equations
source
@[protected, instance]
def padic_int.norm_one_class (p : ℕ) [fact (nat.prime p)] :
norm_one_class ℤ_[p]
source
@[protected, instance]
def padic_int.is_absolute_value (p : ℕ) [fact (nat.prime p)] :
is_absolute_value (λ (z : ℤ_[p]), ‖z‖)
source
@[protected, instance]
def padic_int.is_domain {p : ℕ} [fact (nat.prime p)] :
is_domain ℤ_[p]

Norm #

source
theorem padic_int.norm_le_one {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
‖z‖ ≤ 1
source
@[simp]
theorem padic_int.norm_mul {p : ℕ} [fact (nat.prime p)] (z1 z2 : ℤ_[p]) :
‖z1 * z2‖ = ‖z1‖ * ‖z2‖
source
@[simp]
theorem padic_int.norm_pow {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) (n : ℕ) :
‖z ^ n‖ = ‖z‖ ^ n
source
theorem padic_int.nonarchimedean {p : ℕ} [fact (nat.prime p)] (q r : ℤ_[p]) :
‖q + r‖ ≤ linear_order.max ‖q‖ ‖r‖
source
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‖
source
theorem padic_int.norm_eq_of_norm_add_lt_right {p : ℕ} [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) :
‖z1‖ = ‖z2‖
source
theorem padic_int.norm_eq_of_norm_add_lt_left {p : ℕ} [fact (nat.prime p)] {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) :
‖z1‖ = ‖z2‖
source
@[simp]
theorem padic_int.padic_norm_e_of_padic_int {p : ℕ} [fact (nat.prime p)] (z : ℤ_[p]) :
‖↑z‖ = ‖z‖
source
theorem padic_int.norm_int_cast_eq_padic_norm {p : ℕ} [fact (nat.prime p)] (z : ℤ) :
‖↑z‖ = ‖↑z‖
source
@[simp]
theorem padic_int.norm_eq_padic_norm {p : ℕ} [fact (nat.prime p)] {q : ℚ_[p]} (hq : ‖q‖ ≤ 1) :
‖⟨q, hq⟩‖ = ‖q‖
source
@[simp]
theorem padic_int.norm_p {p : ℕ} [fact (nat.prime p)] :
‖↑p‖ = (↑p)⁻¹
source
@[simp]
theorem padic_int.norm_p_pow {p : ℕ} [fact (nat.prime p)] (n : ℕ) :
‖↑p ^ n‖ = ↑p ^ -↑n
source
@[protected, instance]
def padic_int.complete (p : ℕ) [fact (nat.prime p)] :
cau_seq.is_complete ℤ_[p] has_norm.norm
source
theorem padic_int.exists_pow_neg_lt (p : ℕ) [hp : fact (nat.prime p)] {ε : ℝ} (hε : 0 < ε) :
∃ (k : ℕ), ↑p ^ -↑k < ε
source
theorem padic_int.exists_pow_neg_lt_rat (p : ℕ) [hp : fact (nat.prime p)] {ε : ℚ} (hε : 0 < ε) :
∃ (k : ℕ), ↑p ^ -↑k < ε
source
theorem padic_int.norm_int_lt_one_iff_dvd {p : ℕ} [hp : fact (nat.prime p)] (k : ℤ) :
‖↑k‖ < 1 ↔ ↑p ∣ k
source
theorem padic_int.norm_int_le_pow_iff_dvd {p : ℕ} [hp : fact (nat.prime p)] {k : ℤ} {n : ℕ} :
‖↑k‖ ≤ ↑p ^ -↑n ↔ ↑p ^ n ∣ k

Valuation on ℤ_[p] #

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

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

Equations
source
theorem padic_int.norm_eq_pow_val {p : ℕ} [hp : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :
‖x‖ = ↑p ^ -x.valuation
source
@[simp]
theorem padic_int.valuation_zero {p : ℕ} [hp : fact (nat.prime p)] :
0.valuation = 0
source
@[simp]
theorem padic_int.valuation_one {p : ℕ} [hp : fact (nat.prime p)] :
1.valuation = 0
source
@[simp]
theorem padic_int.valuation_p {p : ℕ} [hp : fact (nat.prime p)] :
↑p.valuation = 1
source
theorem padic_int.valuation_nonneg {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) :
0 ≤ x.valuation
source
@[simp]
theorem padic_int.valuation_p_pow_mul {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) :
(↑p ^ n * c).valuation = ↑n + c.valuation

Units of ℤ_[p] #

source
theorem padic_int.mul_inv {p : ℕ} [hp : fact (nat.prime p)] {z : ℤ_[p]} :
‖z‖ = 1 → z * z.inv = 1
source
theorem padic_int.inv_mul {p : ℕ} [hp : fact (nat.prime p)] {z : ℤ_[p]} (hz : ‖z‖ = 1) :
z.inv * z = 1
source
theorem padic_int.is_unit_iff {p : ℕ} [hp : fact (nat.prime p)] {z : ℤ_[p]} :
is_unit z ↔ ‖z‖ = 1
source
theorem padic_int.norm_lt_one_add {p : ℕ} [hp : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz1 : ‖z1‖ < 1) (hz2 : ‖z2‖ < 1) :
‖z1 + z2‖ < 1
source
theorem padic_int.norm_lt_one_mul {p : ℕ} [hp : fact (nat.prime p)] {z1 z2 : ℤ_[p]} (hz2 : ‖z2‖ < 1) :
‖z1 * z2‖ < 1
source
@[simp]
theorem padic_int.mem_nonunits {p : ℕ} [hp : fact (nat.prime p)] {z : ℤ_[p]} :
z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1
source
noncomputable def padic_int.mk_units {p : ℕ} [hp : fact (nat.prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1) :
ℤ_[p]ˣ

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

Equations
source
@[simp]
theorem padic_int.mk_units_eq {p : ℕ} [hp : fact (nat.prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1) :
↑↑(padic_int.mk_units h) = u
source
@[simp]
theorem padic_int.norm_units {p : ℕ} [hp : fact (nat.prime p)] (u : ℤ_[p]ˣ) :
‖↑u‖ = 1
source
noncomputable def padic_int.unit_coeff {p : ℕ} [hp : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :
ℤ_[p]ˣ

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

Equations
source
@[simp]
theorem padic_int.unit_coeff_coe {p : ℕ} [hp : fact (nat.prime p)] {x : ℤ_[p]} (hx : x ≠ 0) :
↑(padic_int.unit_coeff hx) = ↑x * ↑p ^ -x.valuation
source
theorem padic_int.unit_coeff_spec {p : ℕ} [hp : 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 #

source
theorem padic_int.norm_le_pow_iff_le_valuation {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
‖x‖ ≤ ↑p ^ -↑n ↔ ↑n ≤ x.valuation
source
theorem padic_int.mem_span_pow_iff_le_valuation {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
x ∈ ideal.span {↑p ^ n} ↔ ↑n ≤ x.valuation
source
theorem padic_int.norm_le_pow_iff_mem_span_pow {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) (n : ℕ) :
‖x‖ ≤ ↑p ^ -↑n ↔ x ∈ ideal.span {↑p ^ n}
source
theorem padic_int.norm_le_pow_iff_norm_lt_pow_add_one {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) (n : ℤ) :
‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
source
theorem padic_int.norm_lt_pow_iff_norm_le_pow_sub_one {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) (n : ℤ) :
‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
source
theorem padic_int.norm_lt_one_iff_dvd {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) :
‖x‖ < 1 ↔ ↑p ∣ x
source
@[simp]
theorem padic_int.pow_p_dvd_int_iff {p : ℕ} [hp : fact (nat.prime p)] (n : ℕ) (a : ℤ) :
↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a

Discrete valuation ring #

source
@[protected, instance]
def padic_int.local_ring {p : ℕ} [hp : fact (nat.prime p)] :
local_ring ℤ_[p]
source
theorem padic_int.p_nonnunit {p : ℕ} [hp : fact (nat.prime p)] :
↑p ∈ nonunits ℤ_[p]
source
theorem padic_int.maximal_ideal_eq_span_p {p : ℕ} [hp : fact (nat.prime p)] :
local_ring.maximal_ideal ℤ_[p] = ideal.span {↑p}
source
theorem padic_int.prime_p {p : ℕ} [hp : fact (nat.prime p)] :
prime ↑p
source
theorem padic_int.irreducible_p {p : ℕ} [hp : fact (nat.prime p)] :
irreducible ↑p
source
@[protected, instance]
def padic_int.discrete_valuation_ring {p : ℕ} [hp : fact (nat.prime p)] :
discrete_valuation_ring ℤ_[p]
source
theorem padic_int.ideal_eq_span_pow_p {p : ℕ} [hp : fact (nat.prime p)] {s : ideal ℤ_[p]} (hs : s ≠ ⊥) :
∃ (n : ℕ), s = ideal.span {↑p ^ n}
source
@[protected, instance]
def padic_int.is_adic_complete {p : ℕ} [hp : fact (nat.prime p)] :
is_adic_complete (local_ring.maximal_ideal ℤ_[p]) ℤ_[p]
source
@[protected, instance]
def padic_int.algebra {p : ℕ} [hp : fact (nat.prime p)] :
algebra ℤ_[p] ℚ_[p]
Equations
source
@[simp]
theorem padic_int.algebra_map_apply {p : ℕ} [hp : fact (nat.prime p)] (x : ℤ_[p]) :
⇑(algebra_map ℤ_[p] ℚ_[p]) x = ↑x
source
@[protected, instance]
def padic_int.is_fraction_ring {p : ℕ} [hp : fact (nat.prime p)] :
is_fraction_ring ℤ_[p] ℚ_[p]