431
|
1 open import Level
|
|
2 open import Ordinals
|
|
3 module Topology {n : Level } (O : Ordinals {n}) where
|
|
4
|
|
5 open import zf
|
|
6 open import logic
|
|
7 open _∧_
|
|
8 open _∨_
|
|
9 open Bool
|
|
10
|
|
11 import OD
|
|
12 open import Relation.Nullary
|
|
13 open import Data.Empty
|
|
14 open import Relation.Binary.Core
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
16 import BAlgbra
|
|
17 open BAlgbra O
|
|
18 open inOrdinal O
|
|
19 open OD O
|
|
20 open OD.OD
|
|
21 open ODAxiom odAxiom
|
|
22 import OrdUtil
|
|
23 import ODUtil
|
|
24 open Ordinals.Ordinals O
|
|
25 open Ordinals.IsOrdinals isOrdinal
|
|
26 open Ordinals.IsNext isNext
|
|
27 open OrdUtil O
|
|
28 open ODUtil O
|
|
29
|
|
30 import ODC
|
|
31 open ODC O
|
|
32
|
1102
|
33 open import filter O
|
1101
|
34 open import OPair O
|
|
35
|
431
|
36
|
482
|
37 record Topology ( L : HOD ) : Set (suc n) where
|
431
|
38 field
|
|
39 OS : HOD
|
|
40 OS⊆PL : OS ⊆ Power L
|
|
41 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P
|
|
42 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
|
1101
|
43 -- closed Set
|
|
44 CS : HOD
|
|
45 CS = record { od = record { def = λ x → odef OS (& ( L \ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
|
|
46 tp02 : {y : Ordinal } → odef OS (& (L \ * y)) → y o< & L
|
|
47 tp02 {y} nop = ?
|
1108
|
48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L
|
|
49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy )
|
1101
|
50 -- ∈∅< ( proj1 nop )
|
431
|
51
|
482
|
52 open Topology
|
431
|
53
|
1107
|
54 -- Base
|
|
55 -- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
|
|
56 -- W ⊆ U ∩ V and x ∈ W .
|
|
57
|
|
58 data Subbase (P : HOD) : Ordinal → Set n where
|
|
59 gi : {x : Ordinal } → odef P x → Subbase P x
|
|
60 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))
|
|
61
|
1108
|
62 Subbases : (P : HOD) → HOD
|
|
63 Subbases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }
|
1107
|
64
|
|
65 record Base (P : HOD) (x : Ordinal) : Set n where
|
|
66 field
|
|
67 b : Ordinal
|
1108
|
68 pb : odef (Power (Subbases P) ) b
|
|
69 bx : odef (* b) x
|
1107
|
70
|
|
71 GeneratedTop : (P : HOD) → HOD
|
|
72 GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
|
|
73
|
1110
|
74 record IsBase (L P : HOD) : Set (suc n) where
|
|
75 field
|
|
76 p : {x : HOD} → L ∋ x → HOD
|
|
77 in-P : {x : HOD} → (lx : L ∋ x ) → P ∋ p lx
|
|
78 b∩ : {x y : HOD} → (bx : P ∋ x ) (by : P ∋ y ) → HOD
|
|
79 b∩⊂ : {x y z : HOD} → {bx : P ∋ x } {by : P ∋ y } → ( x ∩ y ) ∋ z → ( b∩ bx by ∋ x ) ∧ ( b∩ bx by ⊆ ( x ∩ y ) )
|
|
80
|
|
81 GeneratedIsTopogy : (P L : HOD) → IsBase L P → Topology L
|
|
82 GeneratedIsTopogy = ?
|
|
83
|
1107
|
84 -- covers
|
1101
|
85
|
431
|
86 record _covers_ ( P q : HOD ) : Set (suc n) where
|
|
87 field
|
|
88 cover : {x : HOD} → q ∋ x → HOD
|
|
89 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
|
|
90 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
|
|
91
|
|
92 -- Finite Intersection Property
|
|
93
|
|
94 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
|
1101
|
95 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
|
|
96 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
|
431
|
97
|
1102
|
98 record FIP {L : HOD} (top : Topology L) : Set (suc n) where
|
431
|
99 field
|
1102
|
100 fipS⊆PL : L ⊆ CS top
|
|
101 fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )
|
431
|
102
|
|
103 -- Compact
|
|
104
|
|
105 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
|
1101
|
106 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
|
431
|
107 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
|
|
108
|
1102
|
109 record Compact {L : HOD} (top : Topology L) : Set (suc n) where
|
431
|
110 field
|
1102
|
111 finCover : {X : HOD} → X ⊆ OS top → X covers L → HOD
|
|
112 isCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
|
|
113 isFinite : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp )
|
431
|
114
|
|
115 -- FIP is Compact
|
|
116
|
1102
|
117 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top
|
|
118 FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }
|
431
|
119
|
1102
|
120 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
|
482
|
121 Compact→FIP = {!!}
|
431
|
122
|
|
123 -- Product Topology
|
|
124
|
1101
|
125 open ZFProduct
|
|
126
|
1102
|
127 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
|
|
128 field
|
1106
|
129 p q : Ordinal
|
1102
|
130 op : odef (OS TP) p
|
1106
|
131 prod : x ≡ & (ZFP (* p) Q )
|
1102
|
132
|
|
133 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
|
|
134 field
|
1106
|
135 p q : Ordinal
|
1102
|
136 oq : odef (OS TQ) q
|
1106
|
137 prod : x ≡ & (ZFP P (* q ))
|
|
138
|
1107
|
139 -- box : HOD
|
|
140 -- box = ZFP (OS TP) (OS TQ)
|
|
141
|
1106
|
142 base : {P Q : HOD} → Topology P → Topology Q → HOD
|
|
143 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
|
|
144
|
|
145 POS : {P Q : HOD} → Topology P → Topology Q → HOD
|
1107
|
146 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)
|
1102
|
147
|
1110
|
148 PU : {A B : HOD} → Power A ∋ B → Power A ∋ Union B
|
|
149 PU = ?
|
1108
|
150
|
1101
|
151 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
|
|
152 _Top⊗_ {P} {Q} TP TQ = record {
|
1106
|
153 OS = POS TP TQ
|
|
154 ; OS⊆PL = tp10
|
1108
|
155 ; o∪ = tp13
|
1109
|
156 ; o∩ = tp14
|
1101
|
157 } where
|
1102
|
158 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y )
|
|
159 -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U )
|
1108
|
160 tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x
|
|
161 tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12 where
|
|
162 tp12 : ZFProduct P Q x
|
|
163 tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso) zx
|
|
164 ... | ab-pair pa qb = ZFP→
|
|
165 (os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op ) (subst (λ k → odef (* p) k) (sym &iso) pa) )
|
|
166 (subst (λ k → odef Q k ) (sym &iso) qb )
|
|
167 tp11 {x} {z} (gi (case2 record { p = p ; q = q ; oq = oq ; prod = z=zfp })) zx = tp12 where
|
|
168 tp12 : ZFProduct P Q x
|
|
169 tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso) zx
|
|
170 ... | ab-pair pa qb = ZFP→
|
|
171 (subst (λ k → odef P k ) (sym &iso) pa )
|
|
172 ((os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq )) (subst (λ k → odef (* q) k) (sym &iso) qb) )
|
|
173 tp11 {x} (g∩ {a} {b} sb sb₁) zx = tp11 sb (proj1 (subst (λ k → odef k x) *iso zx ))
|
1106
|
174 tp10 : POS TP TQ ⊆ Power (ZFP P Q)
|
1108
|
175 tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz
|
|
176 tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
|
1109
|
177 tp13 {U} U⊆O = tp20 U U⊆O where
|
|
178 ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x
|
1110
|
179 ind {x} prev x⊆O = record { b = & ub ; pb = ? ; bx = ? } where
|
|
180 ub : HOD
|
|
181 ub = Union ( Replace' x ( λ z xz → * (Base.b (x⊆O xz) ) ) )
|
|
182 tp14 : ub ∋ Union x
|
|
183 tp14 = ?
|
1109
|
184 tp20 : (U : HOD ) → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
|
|
185 tp20 U U⊆O = ε-induction0 { λ U → U ⊆ POS TP TQ → POS TP TQ ∋ Union U } ind U U⊆O
|
|
186 tp14 : {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q)
|
|
187 tp14 {p} {q} op oq = record { b = & tp15 ; pb = ? ; bx = ? } where
|
|
188 tp15 : HOD
|
|
189 tp15 = ?
|
431
|
190
|
|
191 -- existence of Ultra Filter
|
|
192
|
1102
|
193 open Filter
|
|
194
|
431
|
195 -- Ultra Filter has limit point
|
|
196
|
1102
|
197 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
|
|
198 field
|
|
199 limit : Ordinal
|
|
200 P∋limit : odef P limit
|
|
201 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
|
|
202
|
431
|
203 -- FIP is UFL
|
|
204
|
1102
|
205 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
|
|
206 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf
|
|
207 FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
|
|
208
|
|
209 UFLP→FIP : {P : HOD} (TP : Topology P) →
|
|
210 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP
|
|
211 UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? }
|
|
212
|
431
|
213 -- Product of UFL has limit point (Tychonoff)
|
|
214
|
1102
|
215 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ)
|
|
216 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
|
1104
|
217 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
|
|
218 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
|
1106
|
219 uflp {L} LPQ F uf = record { limit = & < * ( UFLP.limit uflpp) , ? > ; P∋limit = ? ; is-limit = ? } where
|
|
220 LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD
|
|
221 LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
|
|
222 LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P
|
|
223 LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w)
|
1105
|
224 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where
|
|
225 tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P
|
|
226 tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) )
|
|
227 (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where
|
|
228 tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1))
|
|
229 tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
|
1106
|
230 FP : Filter (LPP L LPQ)
|
|
231 FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where
|
|
232 tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ
|
|
233 tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? }
|
1104
|
234 uFP : ultra-filter FP
|
|
235 uFP = record { proper = ? ; ultra = ? }
|
1106
|
236 uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP
|
|
237 uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP
|
1104
|
238 LQ : HOD
|
1105
|
239 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
|
1104
|
240 LQQ : LQ ⊆ Power Q
|
|
241 LQQ = ?
|
1102
|
242
|