-
Notifications
You must be signed in to change notification settings - Fork 283
/
ValuedField.lean
364 lines (323 loc) · 15.3 KB
/
ValuedField.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
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
/-
Copyright (c) 2021 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot
-/
import Mathlib.Topology.Algebra.Valuation
import Mathlib.Topology.Algebra.WithZeroTopology
import Mathlib.Topology.Algebra.UniformField
#align_import topology.algebra.valued_field from "leanprover-community/mathlib"@"3e0c4d76b6ebe9dfafb67d16f7286d2731ed6064"
/-!
# Valued fields and their completions
In this file we study the topology of a field `K` endowed with a valuation (in our application
to adic spaces, `K` will be the valuation field associated to some valuation on a ring, defined in
valuation.basic).
We already know from valuation.topology that one can build a topology on `K` which
makes it a topological ring.
The first goal is to show `K` is a topological *field*, ie inversion is continuous
at every non-zero element.
The next goal is to prove `K` is a *completable* topological field. This gives us
a completion `hat K` which is a topological field. We also prove that `K` is automatically
separated, so the map from `K` to `hat K` is injective.
Then we extend the valuation given on `K` to a valuation on `hat K`.
-/
open Filter Set
open Topology
section DivisionRing
variable {K : Type*} [DivisionRing K] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀]
section ValuationTopologicalDivisionRing
section InversionEstimate
variable (v : Valuation K Γ₀)
-- The following is the main technical lemma ensuring that inversion is continuous
-- in the topology induced by a valuation on a division ring (i.e. the next instance)
-- and the fact that a valued field is completable
-- [BouAC, VI.5.1 Lemme 1]
theorem Valuation.inversion_estimate {x y : K} {γ : Γ₀ˣ} (y_ne : y ≠ 0)
(h : v (x - y) < min (γ * (v y * v y)) (v y)) : v (x⁻¹ - y⁻¹) < γ := by
have hyp1 : v (x - y) < γ * (v y * v y) := lt_of_lt_of_le h (min_le_left _ _)
have hyp1' : v (x - y) * (v y * v y)⁻¹ < γ := mul_inv_lt_of_lt_mul₀ hyp1
have hyp2 : v (x - y) < v y := lt_of_lt_of_le h (min_le_right _ _)
have key : v x = v y := Valuation.map_eq_of_sub_lt v hyp2
have x_ne : x ≠ 0 := by
intro h
apply y_ne
rw [h, v.map_zero] at key
exact v.zero_iff.1 key.symm
have decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹ := by
rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel y_ne,
show x⁻¹ * x = 1 from inv_mul_cancel x_ne, mul_one, one_mul]
calc
v (x⁻¹ - y⁻¹) = v (x⁻¹ * (y - x) * y⁻¹) := by rw [decomp]
_ = v x⁻¹ * (v <| y - x) * v y⁻¹ := by repeat' rw [Valuation.map_mul]
_ = (v x)⁻¹ * (v <| y - x) * (v y)⁻¹ := by rw [map_inv₀, map_inv₀]
_ = (v <| y - x) * (v y * v y)⁻¹ := by rw [mul_assoc, mul_comm, key, mul_assoc, mul_inv_rev]
_ = (v <| y - x) * (v y * v y)⁻¹ := rfl
_ = (v <| x - y) * (v y * v y)⁻¹ := by rw [Valuation.map_sub_swap]
_ < γ := hyp1'
#align valuation.inversion_estimate Valuation.inversion_estimate
end InversionEstimate
open Valued
/-- The topology coming from a valuation on a division ring makes it a topological division ring
[BouAC, VI.5.1 middle of Proposition 1] -/
instance (priority := 100) Valued.topologicalDivisionRing [Valued K Γ₀] :
TopologicalDivisionRing K :=
{ (by infer_instance : TopologicalRing K) with
continuousAt_inv₀ := by
intro x x_ne s s_in
cases' Valued.mem_nhds.mp s_in with γ hs; clear s_in
rw [mem_map, Valued.mem_nhds]
change ∃ γ : Γ₀ˣ, { y : K | (v (y - x) : Γ₀) < γ } ⊆ { x : K | x⁻¹ ∈ s }
have vx_ne := (Valuation.ne_zero_iff <| v).mpr x_ne
let γ' := Units.mk0 _ vx_ne
use min (γ * (γ' * γ')) γ'
intro y y_in
apply hs
simp only [mem_setOf_eq] at y_in
rw [Units.min_val, Units.val_mul, Units.val_mul] at y_in
exact Valuation.inversion_estimate _ x_ne y_in }
#align valued.topological_division_ring Valued.topologicalDivisionRing
/-- A valued division ring is separated. -/
instance (priority := 100) ValuedRing.separated [Valued K Γ₀] : T0Space K := by
suffices T2Space K by infer_instance
apply TopologicalAddGroup.t2Space_of_zero_sep
intro x x_ne
refine ⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩
rw [Valued.mem_nhds]
have vx_ne := (Valuation.ne_zero_iff <| v).mpr x_ne
let γ' := Units.mk0 _ vx_ne
exact ⟨γ', fun y hy => by simpa using hy⟩
#align valued_ring.separated ValuedRing.separated
section
open WithZeroTopology
open Valued
theorem Valued.continuous_valuation [Valued K Γ₀] : Continuous (v : K → Γ₀) := by
rw [continuous_iff_continuousAt]
intro x
rcases eq_or_ne x 0 with (rfl | h)
· rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
intro γ hγ
rw [Filter.Eventually, Valued.mem_nhds_zero]
use Units.mk0 γ hγ; rfl
· have v_ne : (v x : Γ₀) ≠ 0 := (Valuation.ne_zero_iff _).mpr h
rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero v_ne]
apply Valued.loc_const v_ne
#align valued.continuous_valuation Valued.continuous_valuation
end
end ValuationTopologicalDivisionRing
end DivisionRing
namespace Valued
open UniformSpace
variable {K : Type*} [Field K] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
local notation "hat " => Completion
/-- A valued field is completable. -/
instance (priority := 100) completable : CompletableTopField K :=
{ ValuedRing.separated with
nice := by
rintro F hF h0
have : ∃ γ₀ : Γ₀ˣ, ∃ M ∈ F, ∀ x ∈ M, (γ₀ : Γ₀) ≤ v x := by
rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩
rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩
exists γ₀, M, M_in
intro x xM
apply le_of_not_lt _
intro hyp
have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
rwa [H] at this
rcases this with ⟨γ₀, M₀, M₀_in, H₀⟩
rw [Valued.cauchy_iff] at hF ⊢
refine ⟨hF.1.map _, ?_⟩
replace hF := hF.2
intro γ
rcases hF (min (γ * γ₀ * γ₀) γ₀) with ⟨M₁, M₁_in, H₁⟩
clear hF
use (fun x : K => x⁻¹) '' (M₀ ∩ M₁)
constructor
· rw [mem_map]
apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)
exact subset_preimage_image _ _
· rintro _ ⟨x, ⟨x_in₀, x_in₁⟩, rfl⟩ _ ⟨y, ⟨_, y_in₁⟩, rfl⟩
simp only [mem_setOf_eq]
specialize H₁ x x_in₁ y y_in₁
replace x_in₀ := H₀ x x_in₀
clear H₀
apply Valuation.inversion_estimate
· have : (v x : Γ₀) ≠ 0 := by
intro h
rw [h] at x_in₀
simp at x_in₀
exact (Valuation.ne_zero_iff _).mp this
· refine lt_of_lt_of_le H₁ ?_
rw [Units.min_val]
apply min_le_min _ x_in₀
rw [mul_assoc]
have : ((γ₀ * γ₀ : Γ₀ˣ) : Γ₀) ≤ v x * v x :=
calc
↑γ₀ * ↑γ₀ ≤ ↑γ₀ * v x := mul_le_mul_left' x_in₀ ↑γ₀
_ ≤ _ := mul_le_mul_right' x_in₀ (v x)
rw [Units.val_mul]
exact mul_le_mul_left' this γ }
#align valued.completable Valued.completable
open WithZeroTopology
/-- The extension of the valuation of a valued field to the completion of the field. -/
noncomputable def extension : hat K → Γ₀ :=
Completion.denseInducing_coe.extend (v : K → Γ₀)
#align valued.extension Valued.extension
theorem continuous_extension : Continuous (Valued.extension : hat K → Γ₀) := by
refine Completion.denseInducing_coe.continuous_extend ?_
intro x₀
rcases eq_or_ne x₀ 0 with (rfl | h)
· refine ⟨0, ?_⟩
erw [← Completion.denseInducing_coe.toInducing.nhds_eq_comap]
exact Valued.continuous_valuation.tendsto' 0 0 (map_zero v)
· have preimage_one : v ⁻¹' {(1 : Γ₀)} ∈ 𝓝 (1 : K) := by
have : (v (1 : K) : Γ₀) ≠ 0 := by
rw [Valuation.map_one]
exact zero_ne_one.symm
convert Valued.loc_const this
ext x
rw [Valuation.map_one, mem_preimage, mem_singleton_iff, mem_setOf_eq]
obtain ⟨V, V_in, hV⟩ : ∃ V ∈ 𝓝 (1 : hat K), ∀ x : K, (x : hat K) ∈ V → (v x : Γ₀) = 1 := by
rwa [Completion.denseInducing_coe.nhds_eq_comap, mem_comap] at preimage_one
have : ∃ V' ∈ 𝓝 (1 : hat K), (0 : hat K) ∉ V' ∧ ∀ (x) (_ : x ∈ V') (y) (_ : y ∈ V'),
x * y⁻¹ ∈ V := by
have : Tendsto (fun p : hat K × hat K => p.1 * p.2⁻¹) ((𝓝 1) ×ˢ (𝓝 1)) (𝓝 1) := by
rw [← nhds_prod_eq]
conv =>
congr
rfl
rfl
rw [← one_mul (1 : hat K)]
refine
Tendsto.mul continuous_fst.continuousAt (Tendsto.comp ?_ continuous_snd.continuousAt)
-- Porting note: Added `ContinuousAt.tendsto`
convert (continuousAt_inv₀ (zero_ne_one.symm : 1 ≠ (0 : hat K))).tendsto
exact inv_one.symm
rcases tendsto_prod_self_iff.mp this V V_in with ⟨U, U_in, hU⟩
let hatKstar := ({0}ᶜ : Set <| hat K)
have : hatKstar ∈ 𝓝 (1 : hat K) := compl_singleton_mem_nhds zero_ne_one.symm
use U ∩ hatKstar, Filter.inter_mem U_in this
constructor
· rintro ⟨_, h'⟩
rw [mem_compl_singleton_iff] at h'
exact h' rfl
· rintro x ⟨hx, _⟩ y ⟨hy, _⟩
apply hU <;> assumption
rcases this with ⟨V', V'_in, zeroV', hV'⟩
have nhds_right : (fun x => x * x₀) '' V' ∈ 𝓝 x₀ := by
have l : Function.LeftInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
intro x
simp only [mul_assoc, mul_inv_cancel h, mul_one]
have r : Function.RightInverse (fun x : hat K => x * x₀⁻¹) fun x : hat K => x * x₀ := by
intro x
simp only [mul_assoc, inv_mul_cancel h, mul_one]
have c : Continuous fun x : hat K => x * x₀⁻¹ := continuous_id.mul continuous_const
rw [image_eq_preimage_of_inverse l r]
rw [← mul_inv_cancel h] at V'_in
exact c.continuousAt V'_in
have : ∃ z₀ : K, ∃ y₀ ∈ V', ↑z₀ = y₀ * x₀ ∧ z₀ ≠ 0 := by
rcases Completion.denseRange_coe.mem_nhds nhds_right with ⟨z₀, y₀, y₀_in, H : y₀ * x₀ = z₀⟩
refine ⟨z₀, y₀, y₀_in, ⟨H.symm, ?_⟩⟩
rintro rfl
exact mul_ne_zero (ne_of_mem_of_not_mem y₀_in zeroV') h H
rcases this with ⟨z₀, y₀, y₀_in, hz₀, z₀_ne⟩
have vz₀_ne : (v z₀ : Γ₀) ≠ 0 := by rwa [Valuation.ne_zero_iff]
refine ⟨v z₀, ?_⟩
rw [WithZeroTopology.tendsto_of_ne_zero vz₀_ne, eventually_comap]
filter_upwards [nhds_right] with x x_in a ha
rcases x_in with ⟨y, y_in, rfl⟩
have : (v (a * z₀⁻¹) : Γ₀) = 1 := by
apply hV
have : (z₀⁻¹ : K) = (z₀ : hat K)⁻¹ := map_inv₀ (Completion.coeRingHom : K →+* hat K) z₀
rw [Completion.coe_mul, this, ha, hz₀, mul_inv, mul_comm y₀⁻¹, ← mul_assoc, mul_assoc y,
mul_inv_cancel h, mul_one]
solve_by_elim
calc
v a = v (a * z₀⁻¹ * z₀) := by rw [mul_assoc, inv_mul_cancel z₀_ne, mul_one]
_ = v (a * z₀⁻¹) * v z₀ := Valuation.map_mul _ _ _
_ = v z₀ := by rw [this, one_mul]
#align valued.continuous_extension Valued.continuous_extension
@[simp, norm_cast]
theorem extension_extends (x : K) : extension (x : hat K) = v x := by
refine Completion.denseInducing_coe.extend_eq_of_tendsto ?_
rw [← Completion.denseInducing_coe.nhds_eq_comap]
exact Valued.continuous_valuation.continuousAt
#align valued.extension_extends Valued.extension_extends
/-- the extension of a valuation on a division ring to its completion. -/
noncomputable def extensionValuation : Valuation (hat K) Γ₀ where
toFun := Valued.extension
map_zero' := by
rw [← v.map_zero (R := K), ← Valued.extension_extends (0 : K)]
rfl
map_one' := by
simp only
rw [← Completion.coe_one, Valued.extension_extends (1 : K)]
exact Valuation.map_one _
map_mul' x y := by
apply Completion.induction_on₂ x y
(p := fun x y => extension (x * y) = extension x * extension y)
· have c1 : Continuous fun x : hat K × hat K => Valued.extension (x.1 * x.2) :=
Valued.continuous_extension.comp (continuous_fst.mul continuous_snd)
have c2 : Continuous fun x : hat K × hat K => Valued.extension x.1 * Valued.extension x.2 :=
(Valued.continuous_extension.comp continuous_fst).mul
(Valued.continuous_extension.comp continuous_snd)
exact isClosed_eq c1 c2
· intro x y
norm_cast
exact Valuation.map_mul _ _ _
map_add_le_max' x y := by
rw [le_max_iff]
apply Completion.induction_on₂ x y
(p := fun x y => extension (x + y) ≤ extension x ∨ extension (x + y) ≤ extension y)
· have cont : Continuous (Valued.extension : hat K → Γ₀) := Valued.continuous_extension
exact
(isClosed_le (cont.comp continuous_add) <| cont.comp continuous_fst).union
(isClosed_le (cont.comp continuous_add) <| cont.comp continuous_snd)
· intro x y
norm_cast
rw [← le_max_iff]
exact v.map_add x y
#align valued.extension_valuation Valued.extensionValuation
-- Bourbaki CA VI §5 no.3 Proposition 5 (d)
theorem closure_coe_completion_v_lt {γ : Γ₀ˣ} :
closure ((↑) '' { x : K | v x < (γ : Γ₀) }) =
{ x : hat K | extensionValuation x < (γ : Γ₀) } := by
ext x
let γ₀ := extensionValuation x
suffices γ₀ ≠ 0 → (x ∈ closure ((↑) '' { x : K | v x < (γ : Γ₀) }) ↔ γ₀ < (γ : Γ₀)) by
rcases eq_or_ne γ₀ 0 with h | h
· simp only [h, (Valuation.zero_iff _).mp h, mem_setOf_eq, Valuation.map_zero, Units.zero_lt,
iff_true_iff]
apply subset_closure
exact ⟨0, by simp only [mem_setOf_eq, Valuation.map_zero, Units.zero_lt, true_and_iff]; rfl⟩
· exact this h
intro h
have hγ₀ : extension ⁻¹' {γ₀} ∈ 𝓝 x :=
continuous_extension.continuousAt.preimage_mem_nhds
(WithZeroTopology.singleton_mem_nhds_of_ne_zero h)
rw [mem_closure_iff_nhds']
refine ⟨fun hx => ?_, fun hx s hs => ?_⟩
· obtain ⟨⟨-, y, hy₁ : v y < (γ : Γ₀), rfl⟩, hy₂⟩ := hx _ hγ₀
replace hy₂ : v y = γ₀ := by simpa using hy₂
rwa [← hy₂]
· obtain ⟨y, hy₁, hy₂⟩ := Completion.denseRange_coe.mem_nhds (inter_mem hγ₀ hs)
replace hy₁ : v y = γ₀ := by simpa using hy₁
rw [← hy₁] at hx
exact ⟨⟨y, ⟨y, hx, rfl⟩⟩, hy₂⟩
#align valued.closure_coe_completion_v_lt Valued.closure_coe_completion_v_lt
noncomputable instance valuedCompletion : Valued (hat K) Γ₀ where
v := extensionValuation
is_topological_valuation s := by
suffices
HasBasis (𝓝 (0 : hat K)) (fun _ => True) fun γ : Γ₀ˣ => { x | extensionValuation x < γ } by
rw [this.mem_iff]
exact exists_congr fun γ => by simp
simp_rw [← closure_coe_completion_v_lt]
exact (hasBasis_nhds_zero K Γ₀).hasBasis_of_denseInducing Completion.denseInducing_coe
#align valued.valued_completion Valued.valuedCompletion
-- Porting note: removed @[norm_cast] attribute due to error:
-- norm_cast: badly shaped lemma, rhs can't start with coe
@[simp]
theorem valuedCompletion_apply (x : K) : Valued.v (x : hat K) = v x :=
extension_extends x
#align valued.valued_completion_apply Valued.valuedCompletion_apply
end Valued