/
padic_integers.lean
289 lines (207 loc) · 10.2 KB
/
padic_integers.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis, Mario Carneiro
-/
import data.padics.padic_numbers ring_theory.ideals data.int.modeq
/-!
# p-adic integers
This file defines the p-adic integers ℤ_p as the subtype of ℚ_p with norm ≤ 1. We show that ℤ_p is a
complete nonarchimedean normed local ring.
## 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 (prime p) as a type class argument.
Coercions into ℤ_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, p-adic integer
-/
open nat padic metric
noncomputable theory
local attribute [instance] classical.prop_decidable
/-- The p-adic integers ℤ_p are the p-adic numbers with norm ≤ 1. -/
def padic_int (p : ℕ) [p.prime] := {x : ℚ_[p] // ∥x∥ ≤ 1}
notation `ℤ_[`p`]` := padic_int p
namespace padic_int
variables {p : ℕ} [nat.prime p]
/-- Addition on ℤ_p is inherited from ℚ_p. -/
def add : ℤ_[p] → ℤ_[p] → ℤ_[p]
| ⟨x, hx⟩ ⟨y, hy⟩ := ⟨x+y,
le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx,hy⟩)⟩
/-- Multiplication on ℤ_p is inherited from ℚ_p. -/
def mul : ℤ_[p] → ℤ_[p] → ℤ_[p]
| ⟨x, hx⟩ ⟨y, hy⟩ := ⟨x*y,
begin rw padic_norm_e.mul, apply mul_le_one; {assumption <|> apply norm_nonneg} end⟩
/-- Negation on ℤ_p is inherited from ℚ_p. -/
def neg : ℤ_[p] → ℤ_[p]
| ⟨x, hx⟩ := ⟨-x, by simpa⟩
instance : ring ℤ_[p] :=
begin
refine { add := add,
mul := mul,
neg := neg,
zero := ⟨0, by simp [zero_le_one]⟩,
one := ⟨1, by simp⟩,
.. };
{repeat {rintro ⟨_, _⟩}, simp [mul_assoc, left_distrib, right_distrib, add, mul, neg]}
end
lemma zero_def : ∀ x : ℤ_[p], x = 0 ↔ x.val = 0
| ⟨x, _⟩ := ⟨subtype.mk.inj, λ h, by simp at h; simp only [h]; refl⟩
@[simp] lemma add_def : ∀ (x y : ℤ_[p]), (x+y).val = x.val + y.val
| ⟨x, hx⟩ ⟨y, hy⟩ := rfl
@[simp] lemma mul_def : ∀ (x y : ℤ_[p]), (x*y).val = x.val * y.val
| ⟨x, hx⟩ ⟨y, hy⟩ := rfl
@[simp] lemma mk_zero {h} : (⟨0, h⟩ : ℤ_[p]) = (0 : ℤ_[p]) := rfl
instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩
@[simp] lemma val_eq_coe (z : ℤ_[p]) : z.val = ↑z := rfl
@[simp, move_cast] lemma coe_add : ∀ (z1 z2 : ℤ_[p]), (↑(z1 + z2) : ℚ_[p]) = ↑z1 + ↑z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl
@[simp, move_cast] lemma coe_mul : ∀ (z1 z2 : ℤ_[p]), (↑(z1 * z2) : ℚ_[p]) = ↑z1 * ↑z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl
@[simp, move_cast] lemma coe_neg : ∀ (z1 : ℤ_[p]), (↑(-z1) : ℚ_[p]) = -↑z1
| ⟨_, _⟩ := rfl
@[simp, move_cast] lemma coe_sub : ∀ (z1 z2 : ℤ_[p]), (↑(z1 - z2) : ℚ_[p]) = ↑z1 - ↑z2
| ⟨_, _⟩ ⟨_, _⟩ := rfl
@[simp, squash_cast] lemma coe_one : (↑(1 : ℤ_[p]) : ℚ_[p]) = 1 := rfl
@[simp, squash_cast] lemma coe_coe : ∀ n : ℕ, (↑(↑n : ℤ_[p]) : ℚ_[p]) = (↑n : ℚ_[p])
| 0 := rfl
| (k+1) := by simp [coe_coe]
@[simp, squash_cast] lemma coe_zero : (↑(0 : ℤ_[p]) : ℚ_[p]) = 0 := rfl
@[simp, move_cast] lemma cast_pow (x : ℤ_[p]) : ∀ (n : ℕ), (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n
| 0 := by simp
| (k+1) := by simp [monoid.pow, pow]; congr; apply cast_pow
lemma mk_coe : ∀ (k : ℤ_[p]), (⟨↑k, k.2⟩ : ℤ_[p]) = k
| ⟨_, _⟩ := rfl
/-- 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. -/
def inv : ℤ_[p] → ℤ_[p]
| ⟨k, _⟩ := if h : ∥k∥ = 1 then ⟨1/k, by simp [h]⟩ else 0
end padic_int
section instances
variables {p : ℕ} [nat.prime p]
@[reducible] def padic_norm_z (z : ℤ_[p]) : ℝ := ∥z.val∥
instance : metric_space ℤ_[p] := subtype.metric_space
instance : has_norm ℤ_[p] := ⟨padic_norm_z⟩
instance : normed_ring ℤ_[p] :=
{ dist_eq := λ ⟨_, _⟩ ⟨_, _⟩, rfl,
norm_mul := λ ⟨_, _⟩ ⟨_, _⟩, norm_mul_le _ _ }
instance padic_norm_z.is_absolute_value : is_absolute_value (λ z : ℤ_[p], ∥z∥) :=
{ abv_nonneg := norm_nonneg,
abv_eq_zero := λ ⟨_, _⟩, by simp [norm_eq_zero, padic_int.zero_def],
abv_add := λ ⟨_,_⟩ ⟨_, _⟩, norm_triangle _ _,
abv_mul := λ _ _, by unfold norm; simp [padic_norm_z] }
protected lemma padic_int.pmul_comm : ∀ z1 z2 : ℤ_[p], z1*z2 = z2*z1
| ⟨q1, h1⟩ ⟨q2, h2⟩ := show (⟨q1*q2, _⟩ : ℤ_[p]) = ⟨q2*q1, _⟩, by simp [mul_comm]
instance : comm_ring ℤ_[p] :=
{ mul_comm := padic_int.pmul_comm,
..padic_int.ring }
protected lemma padic_int.zero_ne_one : (0 : ℤ_[p]) ≠ 1 :=
show (⟨(0 : ℚ_[p]), _⟩ : ℤ_[p]) ≠ ⟨(1 : ℚ_[p]), _⟩, from mt subtype.ext.1 zero_ne_one
protected lemma padic_int.eq_zero_or_eq_zero_of_mul_eq_zero :
∀ (a b : ℤ_[p]), a * b = 0 → a = 0 ∨ b = 0
| ⟨a, ha⟩ ⟨b, hb⟩ := λ h : (⟨a * b, _⟩ : ℤ_[p]) = ⟨0, _⟩,
have a * b = 0, from subtype.ext.1 h,
(mul_eq_zero_iff_eq_zero_or_eq_zero.1 this).elim
(λ h1, or.inl (by simp [h1]; refl))
(λ h2, or.inr (by simp [h2]; refl))
instance : integral_domain ℤ_[p] :=
{ eq_zero_or_eq_zero_of_mul_eq_zero := padic_int.eq_zero_or_eq_zero_of_mul_eq_zero,
zero_ne_one := padic_int.zero_ne_one,
..padic_int.comm_ring }
end instances
namespace padic_norm_z
variables {p : ℕ} [nat.prime p]
lemma le_one : ∀ z : ℤ_[p], ∥z∥ ≤ 1
| ⟨_, h⟩ := h
@[simp] lemma one : ∥(1 : ℤ_[p])∥ = 1 := by simp [norm, padic_norm_z]
@[simp] lemma mul (z1 z2 : ℤ_[p]) : ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ :=
by unfold norm; simp [padic_norm_z]
@[simp] lemma pow (z : ℤ_[p]) : ∀ n : ℕ, ∥z^n∥ = ∥z∥^n
| 0 := by simp
| (k+1) := show ∥z*z^k∥ = ∥z∥*∥z∥^k, by {rw mul, congr, apply pow}
theorem nonarchimedean : ∀ (q r : ℤ_[p]), ∥q + r∥ ≤ max (∥q∥) (∥r∥)
| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.nonarchimedean _ _
theorem add_eq_max_of_ne : ∀ {q r : ℤ_[p]}, ∥q∥ ≠ ∥r∥ → ∥q+r∥ = max (∥q∥) (∥r∥)
| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.add_eq_max_of_ne
@[simp] lemma norm_one : ∥(1 : ℤ_[p])∥ = 1 := norm_one
lemma eq_of_norm_add_lt_right {z1 z2 : ℤ_[p]}
(h : ∥z1 + z2∥ < ∥z2∥) : ∥z1∥ = ∥z2∥ :=
by_contradiction $ λ hne,
not_lt_of_ge (by rw padic_norm_z.add_eq_max_of_ne hne; apply le_max_right) h
lemma eq_of_norm_add_lt_left {z1 z2 : ℤ_[p]}
(h : ∥z1 + z2∥ < ∥z1∥) : ∥z1∥ = ∥z2∥ :=
by_contradiction $ λ hne,
not_lt_of_ge (by rw padic_norm_z.add_eq_max_of_ne hne; apply le_max_left) h
@[simp] lemma padic_norm_e_of_padic_int (z : ℤ_[p]) : ∥(↑z : ℚ_[p])∥ = ∥z∥ :=
by simp [norm, padic_norm_z]
@[simp] lemma padic_norm_z_eq_padic_norm_e {q : ℚ_[p]} (hq : ∥q∥ ≤ 1) :
@norm ℤ_[p] _ ⟨q, hq⟩ = ∥q∥ := rfl
end padic_norm_z
private lemma mul_lt_one {α} [decidable_linear_ordered_comm_ring α] {a b : α} (hbz : 0 < b)
(ha : a < 1) (hb : b < 1) : a * b < 1 :=
suffices a*b < 1*1, by simpa,
mul_lt_mul ha (le_of_lt hb) hbz zero_le_one
private lemma mul_lt_one_of_le_of_lt {α} [decidable_linear_ordered_comm_ring α] {a b : α} (ha : a ≤ 1)
(hbz : 0 ≤ b) (hb : b < 1) : a * b < 1 :=
if hb' : b = 0 then by simpa [hb'] using zero_lt_one
else if ha' : a = 1 then by simpa [ha']
else mul_lt_one (lt_of_le_of_ne hbz (ne.symm hb')) (lt_of_le_of_ne ha ha') hb
namespace padic_int
variables {p : ℕ} [nat.prime p]
local attribute [reducible] padic_int
lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
| ⟨k, _⟩ h :=
begin
have hk : k ≠ 0, from λ h', @zero_ne_one ℚ_[p] _ (by simpa [h'] using h),
unfold padic_int.inv, split_ifs,
{ change (⟨k * (1/k), _⟩ : ℤ_[p]) = 1,
simp [hk], refl },
{ apply subtype.ext.2, simp [mul_inv_cancel hk] }
end
lemma inv_mul {z : ℤ_[p]} (hz : ∥z∥ = 1) : z.inv * z = 1 :=
by rw [mul_comm, mul_inv hz]
lemma is_unit_iff {z : ℤ_[p]} : is_unit z ↔ ∥z∥ = 1 :=
⟨λ h, begin
rcases is_unit_iff_dvd_one.1 h with ⟨w, eq⟩,
refine le_antisymm (padic_norm_z.le_one _) _,
have := mul_le_mul_of_nonneg_left (padic_norm_z.le_one w) (norm_nonneg z),
rwa [mul_one, ← padic_norm_z.mul, ← eq, padic_norm_z.one] at this
end, λ h, ⟨⟨z, z.inv, mul_inv h, inv_mul h⟩, rfl⟩⟩
lemma norm_lt_one_add {z1 z2 : ℤ_[p]} (hz1 : ∥z1∥ < 1) (hz2 : ∥z2∥ < 1) : ∥z1 + z2∥ < 1 :=
lt_of_le_of_lt (padic_norm_z.nonarchimedean _ _) (max_lt hz1 hz2)
lemma norm_lt_one_mul {z1 z2 : ℤ_[p]} (hz2 : ∥z2∥ < 1) : ∥z1 * z2∥ < 1 :=
calc ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ : by simp
... < 1 : mul_lt_one_of_le_of_lt (padic_norm_z.le_one _) (norm_nonneg _) hz2
@[simp] lemma mem_nonunits {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ∥z∥ < 1 :=
by rw lt_iff_le_and_ne; simp [padic_norm_z.le_one z, nonunits, is_unit_iff]
instance : local_ring ℤ_[p] :=
local_of_nonunits_ideal zero_ne_one $ λ x y, by simp; exact norm_lt_one_add
private def cau_seq_to_rat_cau_seq (f : cau_seq ℤ_[p] norm) :
cau_seq ℚ_[p] (λ a, ∥a∥) :=
⟨ λ n, f n,
λ _ hε, by simpa [norm, padic_norm_z] using f.cauchy hε ⟩
instance complete : cau_seq.is_complete ℤ_[p] norm :=
⟨ λ f,
have hqn : ∥cau_seq.lim (cau_seq_to_rat_cau_seq f)∥ ≤ 1,
from padic_norm_e_lim_le zero_lt_one (λ _, padic_norm_z.le_one _),
⟨ ⟨_, hqn⟩,
λ ε, by simpa [norm, padic_norm_z] using cau_seq.equiv_lim (cau_seq_to_rat_cau_seq f) ε⟩⟩
end padic_int
namespace padic_norm_z
variables {p : ℕ} [nat.prime p]
lemma padic_val_of_cong_pow_p {z1 z2 : ℤ} {n : ℕ} (hz : z1 ≡ z2 [ZMOD ↑(p^n)]) :
∥(z1 - z2 : ℚ_[p])∥ ≤ ↑(↑p ^ (-n : ℤ) : ℚ) :=
have hdvd : ↑(p^n) ∣ z2 - z1, from int.modeq.modeq_iff_dvd.1 hz,
have (z2 - z1 : ℚ_[p]) = ↑(↑(z2 - z1) : ℚ), by norm_cast,
begin
rw [norm_sub_rev, this, padic_norm_e.eq_padic_norm],
exact_mod_cast padic_norm.le_of_dvd p hdvd
end
end padic_norm_z