-
Notifications
You must be signed in to change notification settings - Fork 13
/
topology.lean
401 lines (338 loc) · 14.6 KB
/
topology.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
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
import topology.opens
import topology.algebra.continuous_functions
import for_mathlib.filter
import for_mathlib.data.set.basic
open topological_space function
local notation `𝓝` x:70 := nhds x
local notation f `∘₂` g := function.bicompr f g
-- We need to think whether we could directly use the class t2_space (which is not using opens though)
definition is_hausdorff (α : Type*) [topological_space α] : Prop :=
∀ x y, x ≠ y → ∃ u v : opens α, x ∈ u ∧ y ∈ v ∧ u ∩ v = ∅
open set filter
instance regular_of_discrete {α : Type*} [topological_space α] [discrete_topology α] :
regular_space α :=
{ t1 := λ x, is_open_discrete _,
regular :=
begin
intros s a s_closed a_not,
refine ⟨s, is_open_discrete s, subset.refl s, _⟩,
erw [← empty_in_sets_eq_bot, mem_inf_sets],
use {a},
rw nhds_discrete α,
simp,
refine ⟨s, subset.refl s, _ ⟩,
rintro x ⟨xa, xs⟩,
rw ← mem_singleton_iff.1 xa at a_not,
exact a_not xs
end }
lemma continuous_of_const {α : Type*} {β : Type*}
[topological_space α] [topological_space β]
{f : α → β} (h : ∀a b, f a = f b) :
continuous f :=
λ s _, by convert @is_open_const _ _ (∃ a, f a ∈ s); exact
set.ext (λ a, ⟨λ fa, ⟨_, fa⟩,
λ ⟨b, fb⟩, show f a ∈ s, from h b a ▸ fb⟩)
section
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
variables [topological_space α] [topological_space β] [topological_space γ] [topological_space δ]
def continuous₂ (f : α → β → γ) := continuous (function.uncurry' f)
lemma continuous₂_def (f : α → β → γ) : continuous₂ f ↔ continuous (function.uncurry' f) := iff.rfl
lemma continuous₂_curry (f : α × β → γ) : continuous₂ (function.curry f) ↔ continuous f :=
by rw [←function.uncurry'_curry f] {occs := occurrences.pos [2]} ; refl
lemma continuous₂.comp {f : α → β → γ} {g : γ → δ} (hf : continuous₂ f)(hg : continuous g) :
continuous₂ (g ∘₂ f) := hg.comp hf
section
open set filter lattice function
/-
f
α → β
g ↓ ↓ h
γ → δ
i
-/
variables {f : α → β} {g : α → γ} {i : γ → δ} {h : β → δ}
lemma continuous_of_continuous_on_of_induced (H : h ∘ f = i ∘ g) (hi : continuous_on i $ range g)
(hg : ‹topological_space α› = induced g ‹topological_space γ›)
(hh : ‹topological_space β› = induced h ‹topological_space δ›) : continuous f :=
begin
rw continuous_iff_continuous_at,
intro x,
dsimp [continuous_at, tendsto],
rw [hg, hh, nhds_induced, nhds_induced, ← map_le_iff_le_comap, map_comm H],
specialize hi (g x) ⟨x, rfl⟩,
have := calc
nhds_within (g x) (range g) = 𝓝 g x ⊓ principal (range g) : rfl
... = 𝓝 g x ⊓ map g (principal univ) : by rw [← image_univ, ← map_principal]
... = 𝓝 g x ⊓ map g ⊤ : by rw principal_univ,
rw [continuous_within_at, this, ← comp_app i g, ← congr_fun H x] at hi, clear this,
have := calc
map g (comap g 𝓝 g x) = map g (comap g 𝓝 g x ⊓ ⊤) : by rw inf_top_eq
... ≤ map g (comap g 𝓝 g x) ⊓ map g ⊤ : map_inf_le
... ≤ 𝓝 g x ⊓ map g ⊤ : inf_le_inf map_comap_le (le_refl _),
exact le_trans (map_mono this) hi,
end
variables (eg : embedding g) (eh : embedding h)
include eg
lemma embedding.nhds_eq_comap (a : α) : nhds a = comap g (nhds $ g a) :=
by rw [eg.induced, nhds_induced]
include eh
lemma embedding.tendsto_iff (H : h ∘ f = i ∘ g) (a : α) : continuous_at i (g a) → continuous_at f a:=
begin
let N := nhds a, let Nf := nhds (f a),
let Nhf := nhds (h $ f a), let Ng := nhds (g a),
have Neq1 : Nf = comap h Nhf, from eh.nhds_eq_comap (f a),
have Neq2 : N = comap g Ng, from eg.nhds_eq_comap a,
intro hyp,
replace hyp : Ng ≤ comap i Nhf,
{ unfold continuous_at at hyp,
rw ← show h (f a) = i (g a), from congr_fun H a at hyp,
rwa tendsto_iff_comap at hyp },
rw calc
continuous_at f a ↔ tendsto f N Nf : iff.rfl
... ↔ N ≤ comap f Nf : tendsto_iff_comap
... ↔ comap g Ng ≤ comap f (comap h Nhf) : by rw [Neq1, Neq2]
... ↔ comap g Ng ≤ comap g (comap i Nhf) : by rw comap_comm H,
exact comap_mono hyp
end
end
end
namespace dense_inducing
open set function filter
variables {α : Type*} {β : Type*} {δ : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space δ] [topological_space γ]
/-
f
α → β
g ↓ ↓ h
γ → δ
i
-/
variables {f : α → β} {g : α → γ} {i : γ → δ} {h : β → δ}
lemma comp (dh : dense_inducing h) (df : dense_inducing f) : dense_inducing (h ∘ f) :=
{ dense := dense_range.comp _ dh.dense df.dense dh.continuous,
induced := (dh.to_inducing.comp df.to_inducing).induced }
lemma of_comm_square (dg : dense_inducing g) (di : dense_inducing i)
(dh : dense_inducing h) (H : h ∘ f = i ∘ g) : dense_inducing f :=
have dhf : dense_inducing (h ∘ f),
by {rw H, exact di.comp dg },
{ dense := begin
intro x,
have H := dhf.dense (h x),
rw mem_closure_iff_nhds at H ⊢,
intros t ht,
rw [dh.nhds_eq_comap x, mem_comap_sets] at ht,
rcases ht with ⟨u, hu, hinc⟩,
rcases H u hu with ⟨v, hv1, a, rfl⟩,
use f a,
split, swap, apply mem_range_self,
apply mem_of_mem_of_subset _ hinc,
rwa mem_preimage,
end ,
-- inj := λ a b H, dhf.inj (by {show h (f a) = _, rw H}),
induced := by rw [dg.induced, di.induced, induced_compose, ← H, ← induced_compose, dh.induced] }
end dense_inducing
namespace dense_embedding
open set function filter
variables {α : Type*} {β : Type*} {δ : Type*} {γ : Type*}
variables [topological_space α] [topological_space β] [topological_space δ] [topological_space γ]
/-
f
α → β
g ↓ ↓ h
γ → δ
i
-/
variables {f : α → β} {g : α → γ} {i : γ → δ} {h : β → δ}
-- TODO: fix implicit argument in dense_range.comp before PRing
lemma comp (dh : dense_embedding h) (df : dense_embedding f) : dense_embedding (h ∘ f) :=
{ dense := dense_range.comp _ dh.dense df.dense dh.to_dense_inducing.continuous,
inj := function.injective_comp dh.inj df.inj,
induced := (dh.to_inducing.comp df.to_inducing).induced }
lemma of_homeo (h : α ≃ₜ β) : dense_embedding h :=
{ dense := dense_range_iff_closure_range.mpr $
(range_iff_surjective.mpr h.to_equiv.surjective).symm ▸ closure_univ,
inj := h.to_equiv.injective,
induced := h.induced_eq.symm, }
lemma of_comm_square (dg : dense_embedding g) (di : dense_embedding i)
(dh : dense_embedding h) (H : h ∘ f = i ∘ g) : dense_embedding f :=
{ inj := begin
intros a b hab,
have : (h ∘ f) a = (h ∘ f) b := by convert congr_arg h hab,
rw H at this,
exact dg.inj (di.inj this),
end,
..dense_inducing.of_comm_square dg.to_dense_inducing di.to_dense_inducing dh.to_dense_inducing H }
end dense_embedding
section
open filter
variables {α : Type*} [topological_space α] {β : Type*} [topological_space β] [discrete_topology β]
lemma continuous_into_discrete_iff (f : α → β) : continuous f ↔ ∀ b : β, is_open (f ⁻¹' {b}) :=
begin
split,
{ intros hf b,
exact hf _ (is_open_discrete _) },
{ intro h,
rw continuous_iff_continuous_at,
intro x,
have key : f ⁻¹' {f x} ∈ nhds x,
from mem_nhds_sets (h $ f x) (set.mem_insert (f x) ∅),
calc map f (nhds x) ≤ pure (f x) : le_pure_iff.mpr key
... ≤ nhds (f x) : pure_le_nhds _ }
end
lemma discrete_iff_open_singletons : discrete_topology α ↔ ∀ x, is_open ({x} : set α) :=
⟨by introsI ; exact is_open_discrete _, λ h, ⟨eq_bot_of_singletons_open h⟩⟩
lemma discrete_iff_nhds_eq_pure {X : Type*} [topological_space X] :
discrete_topology X ↔ ∀ x : X, nhds x = pure x :=
begin
split,
{ introsI h,
exact congr_fun (nhds_discrete X) },
{ intro h,
constructor,
apply eq_bot_of_singletons_open,
intro x,
change _root_.is_open {x},
rw is_open_iff_nhds,
simp [h] },
end
lemma discrete_of_embedding_discrete {X : Type*} {Y : Type*} [topological_space X] [topological_space Y]
{f : X → Y} (hf : embedding f) [discrete_topology Y] : discrete_topology X :=
begin
rw discrete_iff_nhds_eq_pure,
intro x,
rw [hf.to_inducing.nhds_eq_comap, nhds_discrete, comap_pure hf.inj]
end
lemma is_open_singleton_iff {X : Type*} [topological_space X] {x : X} :
is_open ({x} : set X) ↔ {x} ∈ nhds x :=
begin
rw is_open_iff_nhds,
split ; intro h,
{ apply h x (mem_singleton _),
simp },
{ intros y y_in,
rw mem_singleton_iff at y_in,
simp [*] },
end
end
-- tools for proving that a product of top rings is a top ring
def continuous_pi₁ {I : Type*} {R : I → Type*} {S : I → Type*}
[∀ i, topological_space (R i)] [∀ i, topological_space (S i)]
{f : Π (i : I), (R i) → (S i)} (Hfi : ∀ i, continuous (f i)) :
continuous (λ rs i, f i (rs i) : (Π (i : I), R i) → Π (i : I), S i) :=
continuous_pi (λ i, (Hfi i).comp (continuous_apply i))
def continuous_pi₂ {I : Type*} {R : I → Type*} {S : I → Type*} {T : I → Type*}
[∀ i, topological_space (R i)] [∀ i, topological_space (S i)] [∀ i, topological_space (T i)]
{f : Π (i : I), (R i) × (S i) → (T i)} (Hfi : ∀ i, continuous (f i)) :
continuous (λ rs i, f i ⟨rs.1 i, rs.2 i⟩ : (Π (i : I), R i) × (Π (i : I), S i) → Π (i : I), T i) :=
continuous_pi (λ i, (Hfi i).comp
(continuous.prod_mk ((continuous_apply i).comp continuous_fst) $
(continuous_apply i).comp continuous_snd))
/-
The following class probably won't have global instances, but is meant to model proofs where
we implictly fix a neighborhood filter basis.
-/
class nhds_basis (α : Type*) [topological_space α] :=
(B : α → filter_basis α)
(is_nhds : ∀ x, 𝓝 x = (B x).filter)
namespace nhds_basis
open filter set
variables {α : Type*} {ι : Type*} [topological_space α] [nhds_basis α]
variables {β : Type*} [topological_space β] {δ : Type*}
lemma mem_nhds_iff (x : α) (U : set α) : U ∈ 𝓝 x ↔ ∃ V ∈ B x, V ⊆ U :=
by rw [is_nhds x, filter_basis.mem_filter]
lemma mem_nhds_of_basis {x : α} {U : set α} (U_in : U ∈ B x) : U ∈ 𝓝 x :=
(is_nhds x).symm ▸ filter_basis.mem_filter_of_mem U_in
lemma tendsto_from {f : α → δ} {x : α} {y : filter δ} :
tendsto f (𝓝 x) y ↔ ∀ {V}, V ∈ y → ∃ U ∈ B x, U ⊆ f ⁻¹' V :=
by split ; intros h V V_in ; specialize h V_in ; rwa [← mem_nhds_iff x] at *
lemma continuous_from {f : α → β} : continuous f ↔ ∀ x, ∀ {V}, V ∈ 𝓝 f x → ∃ U ∈ B x, U ⊆ f ⁻¹' V :=
by simp [continuous_iff_continuous_at, continuous_at, tendsto_from]
lemma tendsto_into {f : δ → α} {x : filter δ} {y : α} : tendsto f x 𝓝 y ↔ ∀ U ∈ B y, f ⁻¹' U ∈ x :=
begin
split ; intros h,
{ rintro U U_in,
exact h (mem_nhds_of_basis U_in) },
{ intros V V_in,
rcases (mem_nhds_iff _ _).1 V_in with ⟨W, W_in, hW⟩,
filter_upwards [h W W_in],
exact preimage_mono hW }
end
lemma continuous_into {f : β → α} : continuous f ↔ ∀ x, ∀ U ∈ B (f x), f ⁻¹' U ∈ 𝓝 x :=
by simp [continuous_iff_continuous_at, continuous_at, tendsto_into]
lemma tendsto_both [nhds_basis β] {f : α → β} {x : α} {y : β} :
tendsto f (𝓝 x) 𝓝 y ↔ ∀ U ∈ B y, ∃ V ∈ B x, V ⊆ f ⁻¹' U :=
begin
rw tendsto_into,
split ; introv h U_in ; specialize h U U_in ; rwa mem_nhds_iff x at *
end
lemma continuous_both [nhds_basis β] {f : α → β} :
continuous f ↔ ∀ x, ∀ U ∈ B (f x), ∃ V ∈ B x, V ⊆ f ⁻¹' U :=
by simp [continuous_iff_continuous_at, continuous_at, tendsto_both]
end nhds_basis
lemma dense_range.mem_nhds {α : Type*} [topological_space α] {β : Type*} [topological_space β]
{f : α → β} (h : dense_range f) {b : β} {U : set β} (U_in : U ∈ nhds b) :
∃ a : α, f a ∈ U :=
begin
rcases (mem_closure_iff_nhds.mp
((dense_range_iff_closure_range.mp h).symm ▸ mem_univ b : b ∈ closure (range f)) U U_in)
with ⟨_, h, a, rfl⟩,
exact ⟨a, h⟩
end
lemma mem_closure_union {α : Type*} [topological_space α] {s₁ s₂ : set α} {x : α}
(h : x ∈ closure (s₁ ∪ s₂)) (h₁ : -s₁ ∈ 𝓝 x) : x ∈ closure s₂ :=
begin
rw closure_eq_nhds at *,
have := calc
𝓝 x ⊓ principal (s₁ ∪ s₂) = 𝓝 x ⊓ (principal s₁ ⊔ principal s₂) : by rw sup_principal
... = (𝓝 x ⊓ principal s₁) ⊔ (𝓝 x ⊓ principal s₂) : by rw lattice.inf_sup_left
... = ⊥ ⊔ 𝓝 x ⊓ principal s₂ : by rw inf_principal_eq_bot h₁
... = 𝓝 x ⊓ principal s₂ : by rw lattice.bot_sup_eq,
dsimp,
rwa ← this
end
open lattice
lemma mem_closure_image {α : Type*} {β : Type*} [topological_space α] [topological_space β]
{f : α → β} {x : α} {s : set α} (hf : continuous_at f x) (hx : x ∈ closure s) :
f x ∈ closure (f '' s) :=
begin
rw [closure_eq_nhds, mem_set_of_eq] at *,
rw ← bot_lt_iff_ne_bot,
calc
⊥ < map f (𝓝 x ⊓ principal s) : bot_lt_iff_ne_bot.mpr (map_ne_bot hx)
... ≤ (map f 𝓝 x) ⊓ (map f $ principal s) : map_inf_le
... = (map f 𝓝 x) ⊓ (principal $ f '' s) : by rw map_principal
... ≤ 𝓝 (f x) ⊓ (principal $ f '' s) : inf_le_inf hf (le_refl _)
end
lemma continuous_at.prod_mk {α : Type*} {β : Type*} {γ : Type*} [topological_space α]
[topological_space β] [topological_space γ] {f : γ → α} {g : γ → β} {x : γ}
(hf : continuous_at f x) (hg : continuous_at g x) : continuous_at (λ x, prod.mk (f x) $ g x) x :=
calc
map (λ (x : γ), (f x, g x)) (𝓝 x) ≤ (map f 𝓝 x).prod (map g 𝓝 x) : filter.map_prod_mk _ _ _
... ≤ (𝓝 f x).prod (𝓝 g x) : filter.prod_mono hf hg
... = 𝓝 (f x, g x) : by rw nhds_prod_eq
lemma continuous_at.congr_aux {α : Type*} {β : Type*} [topological_space α] [topological_space β]
{f g : α → β} {a : α} (h : {x | f x = g x } ∈ 𝓝 a) (hf : continuous_at f a) : continuous_at g a :=
begin
intros U U_in,
rw show g a = f a, from (mem_of_nhds h).symm at U_in,
let V := {x : α | g x ∈ U} ∩ {x | f x = g x},
suffices : V ∈ 𝓝 a,
{ rw mem_map,
exact mem_sets_of_superset this (inter_subset_left _ _) },
have : V = {x : α | f x ∈ U} ∩ {x | f x = g x},
{ ext x,
split ; rintros ⟨hl, hr⟩ ; rw mem_set_of_eq at hr hl ;
[ rw ← hr at hl, rw hr at hl ] ; exact ⟨hl, hr⟩ },
rw this,
exact filter.inter_mem_sets (hf U_in) ‹_›
end
lemma continuous_at.congr {α : Type*} {β : Type*} [topological_space α] [topological_space β]
{f g : α → β} {a : α} (h : {x | f x = g x } ∈ 𝓝 a) : continuous_at f a ↔ continuous_at g a :=
begin
split ; intro h',
{ exact continuous_at.congr_aux h h' },
{ apply continuous_at.congr_aux _ h',
convert h,
ext x,
rw eq_comm }
end