/
Valuation.lean
187 lines (154 loc) · 7.09 KB
/
Valuation.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
/-
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.Nonarchimedean.Bases
import Mathlib.Topology.Algebra.UniformFilterBasis
import Mathlib.RingTheory.Valuation.ValuationSubring
#align_import topology.algebra.valuation from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
/-!
# The topology on a valued ring
In this file, we define the non archimedean topology induced by a valuation on a ring.
The main definition is a `Valued` type class which equips a ring with a valuation taking
values in a group with zero. Other instances are then deduced from this.
-/
open scoped Classical
open Topology uniformity
open Set Valuation
noncomputable section
universe v u
variable {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀]
namespace Valuation
variable (v : Valuation R Γ₀)
/-- The basis of open subgroups for the topology on a ring determined by a valuation. -/
theorem subgroups_basis : RingSubgroupsBasis fun γ : Γ₀ˣ => (v.ltAddSubgroup γ : AddSubgroup R) :=
{ inter := by
rintro γ₀ γ₁
use min γ₀ γ₁
simp only [ltAddSubgroup, ge_iff_le, Units.min_val, Units.val_le_val, lt_min_iff,
AddSubgroup.mk_le_mk, setOf_subset_setOf, le_inf_iff, and_imp, imp_self, implies_true,
forall_const, and_true]
tauto
mul := by
rintro γ
cases' exists_square_le γ with γ₀ h
use γ₀
rintro - ⟨r, r_in, s, s_in, rfl⟩
calc
(v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
_ < γ₀ * γ₀ := mul_lt_mul₀ r_in s_in
_ ≤ γ := mod_cast h
leftMul := by
rintro x γ
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
· use (1 : Γ₀ˣ)
rintro y _
change v (x * y) < _
rw [Valuation.map_mul, Hx, zero_mul]
exact Units.zero_lt γ
· use γx⁻¹ * γ
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
change (v (x * y) : Γ₀) < γ
rw [Valuation.map_mul, Hx, mul_comm]
rw [Units.val_mul, mul_comm] at vy_lt
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
rightMul := by
rintro x γ
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
· use 1
rintro y _
change v (y * x) < _
rw [Valuation.map_mul, Hx, mul_zero]
exact Units.zero_lt γ
· use γx⁻¹ * γ
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
change (v (y * x) : Γ₀) < γ
rw [Valuation.map_mul, Hx]
rw [Units.val_mul, mul_comm] at vy_lt
simpa using mul_inv_lt_of_lt_mul₀ vy_lt }
#align valuation.subgroups_basis Valuation.subgroups_basis
end Valuation
/-- A valued ring is a ring that comes equipped with a distinguished valuation. The class `Valued`
is designed for the situation that there is a canonical valuation on the ring.
TODO: show that there always exists an equivalent valuation taking values in a type belonging to
the same universe as the ring.
See Note [forgetful inheritance] for why we extend `UniformSpace`, `UniformAddGroup`. -/
class Valued (R : Type u) [Ring R] (Γ₀ : outParam (Type v))
[LinearOrderedCommGroupWithZero Γ₀] extends UniformSpace R, UniformAddGroup R where
v : Valuation R Γ₀
is_topological_valuation : ∀ s, s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γ₀ˣ, { x : R | v x < γ } ⊆ s
#align valued Valued
-- Porting note(#12094): removed nolint; dangerous_instance linter not ported yet
--attribute [nolint dangerous_instance] Valued.toUniformSpace
namespace Valued
/-- Alternative `Valued` constructor for use when there is no preferred `UniformSpace` structure. -/
def mk' (v : Valuation R Γ₀) : Valued R Γ₀ :=
{ v
toUniformSpace := @TopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
toUniformAddGroup := @comm_topologicalAddGroup_is_uniform _ _ v.subgroups_basis.topology _
is_topological_valuation := by
letI := @TopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
intro s
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
exact exists_congr fun γ => by rw [true_and]; rfl }
#align valued.mk' Valued.mk'
variable (R Γ₀)
variable [_i : Valued R Γ₀]
theorem hasBasis_nhds_zero :
(𝓝 (0 : R)).HasBasis (fun _ => True) fun γ : Γ₀ˣ => { x | v x < (γ : Γ₀) } := by
simp [Filter.hasBasis_iff, is_topological_valuation]
#align valued.has_basis_nhds_zero Valued.hasBasis_nhds_zero
-- Porting note: Replaced `𝓤 R` with `uniformity R`
theorem hasBasis_uniformity : (uniformity R).HasBasis (fun _ => True)
fun γ : Γ₀ˣ => { p : R × R | v (p.2 - p.1) < (γ : Γ₀) } := by
rw [uniformity_eq_comap_nhds_zero]
exact (hasBasis_nhds_zero R Γ₀).comap _
#align valued.has_basis_uniformity Valued.hasBasis_uniformity
theorem toUniformSpace_eq :
toUniformSpace = @TopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _ :=
UniformSpace.ext
((hasBasis_uniformity R Γ₀).eq_of_same_basis <| v.subgroups_basis.hasBasis_nhds_zero.comap _)
#align valued.to_uniform_space_eq Valued.toUniformSpace_eq
variable {R Γ₀}
theorem mem_nhds {s : Set R} {x : R} : s ∈ 𝓝 x ↔ ∃ γ : Γ₀ˣ, { y | (v (y - x) : Γ₀) < γ } ⊆ s := by
simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
((hasBasis_nhds_zero R Γ₀).comap fun y => y - x).mem_iff]
#align valued.mem_nhds Valued.mem_nhds
theorem mem_nhds_zero {s : Set R} : s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γ₀ˣ, { x | v x < (γ : Γ₀) } ⊆ s := by
simp only [mem_nhds, sub_zero]
#align valued.mem_nhds_zero Valued.mem_nhds_zero
theorem loc_const {x : R} (h : (v x : Γ₀) ≠ 0) : { y : R | v y = v x } ∈ 𝓝 x := by
rw [mem_nhds]
rcases Units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩
use γ
rw [hx]
intro y y_in
exact Valuation.map_eq_of_sub_lt _ y_in
#align valued.loc_const Valued.loc_const
instance (priority := 100) : TopologicalRing R :=
(toUniformSpace_eq R Γ₀).symm ▸ v.subgroups_basis.toRingFilterBasis.isTopologicalRing
theorem cauchy_iff {F : Filter R} : Cauchy F ↔
F.NeBot ∧ ∀ γ : Γ₀ˣ, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), (v (y - x) : Γ₀) < γ := by
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
apply and_congr Iff.rfl
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
constructor
· intro h γ
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis _)
· rintro h - ⟨γ, rfl⟩
exact h γ
#align valued.cauchy_iff Valued.cauchy_iff
variable (R)
/-- The unit ball of a valued ring is open. -/
theorem integer_isOpen : IsOpen (_i.v.integer : Set R) := by
rw [isOpen_iff_mem_nhds]
intro x hx
rw [mem_nhds]
exact ⟨1,
fun y hy => (sub_add_cancel y x).symm ▸ le_trans (map_add _ _ _) (max_le (le_of_lt hy) hx)⟩
/-- The valuation subring of a valued field is open. -/
theorem valuationSubring_isOpen (K : Type u) [Field K] [hv : Valued K Γ₀] :
IsOpen (hv.v.valuationSubring : Set K) :=
integer_isOpen K
end Valued