|
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 = ?
|
|
|
48 -- ∈∅< ( proj1 nop )
|
|
431
|
49
|
|
482
|
50 open Topology
|
|
431
|
51
|
|
1101
|
52
|
|
431
|
53 record _covers_ ( P q : HOD ) : Set (suc n) where
|
|
|
54 field
|
|
|
55 cover : {x : HOD} → q ∋ x → HOD
|
|
|
56 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
|
|
|
57 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
|
|
|
58
|
|
|
59 -- Base
|
|
|
60 -- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
|
|
|
61 -- W ⊆ U ∩ V and x ∈ W .
|
|
|
62
|
|
|
63 data genTop (P : HOD) : HOD → Set (suc n) where
|
|
|
64 gi : {x : HOD} → P ∋ x → genTop P x
|
|
|
65 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
|
|
|
66 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
|
|
|
67
|
|
|
68 -- Finite Intersection Property
|
|
|
69
|
|
|
70 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
|
|
1101
|
71 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
|
|
|
72 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
|
|
431
|
73
|
|
1102
|
74 record FIP {L : HOD} (top : Topology L) : Set (suc n) where
|
|
431
|
75 field
|
|
1102
|
76 fipS⊆PL : L ⊆ CS top
|
|
|
77 fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )
|
|
431
|
78
|
|
|
79 -- Compact
|
|
|
80
|
|
|
81 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
|
|
1101
|
82 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
|
|
431
|
83 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
|
|
|
84
|
|
1102
|
85 record Compact {L : HOD} (top : Topology L) : Set (suc n) where
|
|
431
|
86 field
|
|
1102
|
87 finCover : {X : HOD} → X ⊆ OS top → X covers L → HOD
|
|
|
88 isCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
|
|
|
89 isFinite : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp )
|
|
431
|
90
|
|
|
91 -- FIP is Compact
|
|
|
92
|
|
1102
|
93 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top
|
|
|
94 FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }
|
|
431
|
95
|
|
1102
|
96 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
|
|
482
|
97 Compact→FIP = {!!}
|
|
431
|
98
|
|
|
99 -- Product Topology
|
|
|
100
|
|
1101
|
101 open ZFProduct
|
|
|
102
|
|
1102
|
103 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
|
|
|
104 field
|
|
|
105 p : Ordinal
|
|
|
106 q : Ordinal
|
|
|
107 op : odef (OS TP) p
|
|
|
108 qq : odef Q q
|
|
|
109 prod : x ≡ & < * p , * q >
|
|
|
110
|
|
|
111 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
|
|
|
112 field
|
|
|
113 p : Ordinal
|
|
|
114 q : Ordinal
|
|
|
115 oq : odef (OS TQ) q
|
|
|
116 pp : odef P p
|
|
|
117 prod : x ≡ & < * p , * q >
|
|
|
118
|
|
1101
|
119 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
|
|
|
120 _Top⊗_ {P} {Q} TP TQ = record {
|
|
|
121 OS = POS
|
|
|
122 ; OS⊆PL = ?
|
|
|
123 ; o∪ = ?
|
|
|
124 ; o∩ = ?
|
|
|
125 } where
|
|
1102
|
126 box : HOD
|
|
|
127 box = ZFP (OS TP) (OS TQ)
|
|
|
128 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y )
|
|
|
129 -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U )
|
|
|
130 base : HOD
|
|
|
131 base = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
|
|
|
132 POS : HOD
|
|
|
133 POS = record { od = record { def = λ x → {b : Ordinal } → odef (Power base) b ∧ odef (Union (* b)) x }
|
|
|
134 ; odmax = & (ZFP P Q) ; <odmax = ? }
|
|
431
|
135
|
|
|
136 -- existence of Ultra Filter
|
|
|
137
|
|
1102
|
138 open Filter
|
|
|
139
|
|
431
|
140 -- Ultra Filter has limit point
|
|
|
141
|
|
1102
|
142 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
|
|
|
143 field
|
|
|
144 limit : Ordinal
|
|
|
145 P∋limit : odef P limit
|
|
|
146 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
|
|
|
147
|
|
431
|
148 -- FIP is UFL
|
|
|
149
|
|
1102
|
150 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
|
|
|
151 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf
|
|
|
152 FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
|
|
|
153
|
|
|
154 UFLP→FIP : {P : HOD} (TP : Topology P) →
|
|
|
155 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP
|
|
|
156 UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? }
|
|
|
157
|
|
431
|
158 -- Product of UFL has limit point (Tychonoff)
|
|
|
159
|
|
1102
|
160 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ)
|
|
|
161 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
|
|
1104
|
162 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
|
|
|
163 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
|
|
|
164 uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where
|
|
|
165 lprod : {x y : Ordinal } → (ly : odef L y) → odef (ZFP P Q) x
|
|
|
166 lprod {x} {y} ly = LPQ ly x ?
|
|
|
167 -- LP : HOD
|
|
|
168 -- LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
|
|
|
169 LP : HOD
|
|
|
170 LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) }
|
|
|
171 ; odmax = & P ; <odmax = ? } where
|
|
|
172 L→P : {y : Ordinal } → odef L y → HOD
|
|
|
173 L→P {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ1 (LPQ ly z yz ) ≡ x }
|
|
|
174 ; odmax = & P ; <odmax = ? }
|
|
|
175 LPP : LP ⊆ Power P
|
|
|
176 LPP = ?
|
|
|
177 FP : Filter LPP
|
|
|
178 FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
|
|
|
179 uFP : ultra-filter FP
|
|
|
180 uFP = record { proper = ? ; ultra = ? }
|
|
|
181 LQ : HOD
|
|
|
182 LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) }
|
|
|
183 ; odmax = & P ; <odmax = ? } where
|
|
|
184 L→Q : {y : Ordinal } → odef L y → HOD
|
|
|
185 L→Q {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ2 (LPQ ly z yz ) ≡ x }
|
|
|
186 ; odmax = & Q ; <odmax = ? }
|
|
|
187 LQQ : LQ ⊆ Power Q
|
|
|
188 LQQ = ?
|
|
|
189 uflpp : UFLP {P} TP {LP} LPP FP uFP
|
|
|
190 uflpp = ?
|
|
1102
|
191
|
|
|
192
|
|
|
193
|
|
|
194
|
|
|
195
|
|
|
196
|
