Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1122:1c7474446754
add OS ∋ od∅
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 04 Jan 2023 09:39:25 +0900 |
parents | 98af35c9711f |
children | 256a3ba634f6 |
rev | line source |
---|---|
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 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
11 import OD |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
12 open import Relation.Nullary |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
13 open import Data.Empty |
431 | 14 open import Relation.Binary.Core |
15 open import Relation.Binary.PropositionalEquality | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
16 import BAlgbra |
431 | 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 | |
482 | 36 record Topology ( L : HOD ) : Set (suc n) where |
431 | 37 field |
38 OS : HOD | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
39 OS⊆PL : OS ⊆ Power L |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
41 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P |
1122 | 42 OS∋od∅ : OS ∋ od∅ |
1101 | 43 -- closed Set |
44 CS : HOD | |
1119 | 45 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
46 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) | |
47 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx )) | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
1108 | 49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
1122 | 50 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L |
51 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) | |
52 CS∋L : CS ∋ L | |
53 CS∋L = ⟪ ? , ? ⟫ | |
54 --- we may add | |
55 -- OS∋L : OS ∋ L | |
56 -- OS∋od∅ : OS ∋ od∅ | |
431 | 57 |
482 | 58 open Topology |
431 | 59 |
1122 | 60 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD |
61 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x } | |
62 ; odmax = & L ; <odmax = ? } | |
63 | |
1119 | 64 -- Subbase P |
65 -- A set of countable intersection of P will be a base (x ix an element of the base) | |
1107 | 66 |
67 data Subbase (P : HOD) : Ordinal → Set n where | |
68 gi : {x : Ordinal } → odef P x → Subbase P x | |
69 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
70 | |
1119 | 71 -- |
72 -- if y is in a Subbase, some element of P contains it | |
73 | |
1111 | 74 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
75 sbp P {x} (gi {y} px) = x | |
76 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
1107 | 77 |
1111 | 78 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
79 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
80 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
1107 | 81 |
1119 | 82 -- An open set generate from a base |
83 -- | |
1115 | 84 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } |
1114 | 85 |
1115 | 86 record Base (L P : HOD) (u x : Ordinal) : Set n where |
1114 | 87 field |
88 b : Ordinal | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
89 u⊂L : * u ⊆ L |
1114 | 90 sb : Subbase P b |
91 b⊆u : * b ⊆ * u | |
92 bx : odef (* b) x | |
1119 | 93 x⊆L : odef L x |
94 x⊆L = u⊂L (b⊆u bx) | |
1114 | 95 |
1115 | 96 SO : (L P : HOD) → HOD |
1119 | 97 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where |
98 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | |
99 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) | |
1114 | 100 |
1111 | 101 record IsSubBase (L P : HOD) : Set (suc n) where |
1110 | 102 field |
1122 | 103 P⊆PL : P ⊆ Power L |
1116 | 104 -- we may need these if OS ∋ L is necessary |
105 -- p : {x : HOD} → L ∋ x → HOD | |
106 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx | |
107 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x | |
1110 | 108 |
1111 | 109 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
1115 | 110 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
1122 | 111 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where |
112 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x | |
113 tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) | |
1115 | 114 tp00 : SO L P ⊆ Power L |
115 tp00 {u} ou x ux with ou ux | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
116 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) |
1115 | 117 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
118 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul |
1116 | 119 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
1115 | 120 px : odef (* (& p)) x |
121 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
122 qx : odef (* (& q)) x | |
123 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
124 b : Ordinal | |
125 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
1116 | 126 tp08 : * b ⊆ * (& (p ∩ q) ) |
127 tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where | |
128 tp11 : * (Base.b (op px)) ⊆ * (& p ) | |
129 tp11 = Base.b⊆u (op px) | |
130 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
131 tp12 = Base.b⊆u (oq qx) | |
132 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p | |
133 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) | |
134 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q | |
135 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) | |
136 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | |
137 tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
138 ul : (p ∩ q) ⊆ L |
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
139 ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq → (Base.u⊂L (op px)) (pz pq) ) where |
1116 | 140 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
141 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | |
1115 | 142 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q |
143 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux | |
144 ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
145 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) tp04 |
1116 | 146 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where |
147 tp05 : Union q ⊆ L | |
148 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
149 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
150 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
151 tp04 : Union q ⊆ L |
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
152 tp04 = tp05 |
1116 | 153 tp06 : * b ⊆ Union q |
154 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } | |
1110 | 155 |
1107 | 156 -- covers |
1101 | 157 |
1120 | 158 record _covers_ ( P q : HOD ) : Set n where |
431 | 159 field |
1120 | 160 cover : {x : Ordinal } → odef q x → Ordinal |
161 P∋cover : {x : Ordinal } → {lt : odef q x} → odef P (cover lt) | |
162 isCover : {x : Ordinal } → {lt : odef q x} → odef (* (cover lt)) x | |
163 | |
164 open _covers_ | |
431 | 165 |
166 -- Finite Intersection Property | |
167 | |
1120 | 168 record FIP {L : HOD} (top : Topology L) : Set n where |
431 | 169 field |
1122 | 170 limit : {X : Ordinal } → * X ⊆ CS top → * X ∋ L |
1120 | 171 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal |
1122 | 172 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L ) |
1120 | 173 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) |
1122 | 174 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX XL fip) |
175 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L) | |
176 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) | |
177 → odef L (limit CX XL fip) | |
178 L∋limit {X} CX XL fip = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX XL)) (is-limit CX XL fip XL) | |
431 | 179 |
180 -- Compact | |
181 | |
1119 | 182 data Finite-∪ (S : HOD) : Ordinal → Set n where |
183 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x | |
184 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) | |
431 | 185 |
1120 | 186 record Compact {L : HOD} (top : Topology L) : Set n where |
431 | 187 field |
1120 | 188 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal |
189 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L | |
190 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) | |
431 | 191 |
192 -- FIP is Compact | |
193 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
194 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
1120 | 195 FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where |
1121 | 196 -- set of coset of X |
197 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal | |
198 CX {X} ox = & ( Replace' (* X) (λ z xz → L \ z )) | |
199 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top | |
200 CCX {X} ox = ? | |
201 -- CX has finite intersection | |
202 CXfip : {X : Ordinal } → * X ⊆ OS top → Set n | |
203 CXfip {X} ox = { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | |
204 Cex : {X : Ordinal } → * X ⊆ OS top → HOD | |
205 Cex {X} ox = record { od = record { def = λ C → { x : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) o∅ } | |
206 ; odmax = osuc ( & (Power L)) ; <odmax = ? } | |
207 -- a counter example of fip , some CX has no finite intersection | |
208 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal | |
209 cex {X} ox oc = & ( ODC.minimal O (Cex ox) fip00) where | |
210 fip00 : ¬ ( Cex ox =h= od∅ ) | |
211 fip00 cex=0 = fip03 ? ? where | |
212 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥ | |
213 fip03 {x} {z} xz nxz = nxz xz | |
214 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | |
215 fip02 = ? | |
216 fip01 : Ordinal | |
1122 | 217 fip01 = FIP.limit fip (CCX ox) ? fip02 |
1121 | 218 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ |
219 ¬CXfip {X} ox oc = ? where | |
220 fip04 : odef (Cex ox) (cex ox oc) | |
221 fip04 = ? | |
222 -- this defines finite cover | |
1120 | 223 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
1121 | 224 finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L \ z )) |
225 -- create Finite-∪ from cex | |
1120 | 226 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
227 isFinite = ? | |
228 -- is also a cover | |
229 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | |
230 isCover1 = ? | |
231 | |
431 | 232 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
233 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
482 | 234 Compact→FIP = {!!} |
431 | 235 |
236 -- Product Topology | |
237 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
238 open ZFProduct |
1101 | 239 |
1119 | 240 -- Product Topology is not |
241 -- ZFP (OS TP) (OS TQ) (box) | |
242 | |
1102 | 243 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where |
244 field | |
1106 | 245 p q : Ordinal |
1102 | 246 op : odef (OS TP) p |
1106 | 247 prod : x ≡ & (ZFP (* p) Q ) |
1102 | 248 |
249 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where | |
250 field | |
1106 | 251 p q : Ordinal |
1102 | 252 oq : odef (OS TQ) q |
1106 | 253 prod : x ≡ & (ZFP P (* q )) |
254 | |
1119 | 255 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x |
256 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where | |
257 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) | |
258 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
259 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where | |
260 tp03 : odef P a | |
261 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa | |
262 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where | |
263 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) | |
264 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
265 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where | |
266 tp03 : odef Q b | |
267 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb | |
1107 | 268 |
1119 | 269 pbase : {P Q : HOD} → Topology P → Topology Q → HOD |
270 pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where | |
271 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) | |
272 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) | |
1106 | 273 |
1101 | 274 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) |
1119 | 275 _Top⊗_ {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } |
431 | 276 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
277 -- existence of Ultra Filter |
431 | 278 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
279 open Filter |
1102 | 280 |
431 | 281 -- Ultra Filter has limit point |
282 | |
1122 | 283 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) |
284 (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where | |
1102 | 285 field |
286 limit : Ordinal | |
287 P∋limit : odef P limit | |
288 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F | |
289 | |
431 | 290 -- FIP is UFL |
291 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
292 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
1122 | 293 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FL uf |
294 FIP→UFLP {P} TP fip {L} LP F FL uf = record { limit = FIP.limit fip fip00 CFP fip01 ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 } | |
295 where | |
296 CF : Ordinal | |
297 CF = & ( Replace' (filter F) (λ z fz → Cl TP z (fip03 fz)) ) where | |
298 fip03 : {z : HOD} → filter F ∋ z → z ⊆ P | |
299 fip03 {z} fz {x} zx with LP ( f⊆L F fz ) | |
300 ... | pw = pw x (subst (λ k → odef k x) (sym *iso) zx ) | |
301 CFP : * CF ∋ P -- filter F ∋ P | |
302 CFP = ? | |
303 fip00 : * CF ⊆ CS TP -- replaced | |
304 fip00 = ? | |
305 fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x | |
306 fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅ | |
307 fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ? | |
308 fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 ? fip01) → * o ⊆ filter F | |
309 fip02 {p} oo ol = ? where | |
310 fip04 : odef ? (FIP.limit fip fip00 ? fip01) | |
311 fip04 = FIP.is-limit fip fip00 CFP fip01 ? | |
312 | |
1102 | 313 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
314 UFLP→FIP : {P : HOD} (TP : Topology P) → |
1122 | 315 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F ? uf ) → FIP TP |
316 UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? } | |
1102 | 317 |
431 | 318 -- Product of UFL has limit point (Tychonoff) |
319 | |
1102 | 320 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) |
321 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where | |
1122 | 322 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (LF : filter F ∋ ZFP P Q) |
323 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F ? uf | |
324 uflp {L} LPQ F LF uf = record { limit = & < * ( UFLP.limit uflpp) , ? > ; P∋limit = ? ; is-limit = ? } where | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
325 LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD |
1106 | 326 LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) |
327 LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
328 LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) |
1105 | 329 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where |
330 tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
331 tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) ) |
1105 | 332 (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
333 tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1)) |
1105 | 334 tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt) |
1106 | 335 FP : Filter (LPP L LPQ) |
336 FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where | |
337 tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
338 tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } |
1104 | 339 uFP : ultra-filter FP |
340 uFP = record { proper = ? ; ultra = ? } | |
1122 | 341 uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP ? uFP |
342 uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP ? uFP | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
343 LQ : HOD |
1105 | 344 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) |
1104 | 345 LQQ : LQ ⊆ Power Q |
346 LQQ = ? | |
1102 | 347 |