Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
1121:98af35c9711f | 1122:1c7474446754 |
---|---|
37 field | 37 field |
38 OS : HOD | 38 OS : HOD |
39 OS⊆PL : OS ⊆ Power L | 39 OS⊆PL : OS ⊆ Power L |
40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) | 40 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) |
41 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P | 41 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P |
42 OS∋od∅ : OS ∋ od∅ | |
42 -- closed Set | 43 -- closed Set |
43 CS : HOD | 44 CS : HOD |
44 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where | 45 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
45 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) | 46 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) |
46 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx )) | 47 tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx )) |
47 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L | 48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
48 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) | 49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
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∅ | |
49 | 57 |
50 open Topology | 58 open Topology |
59 | |
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 = ? } | |
51 | 63 |
52 -- Subbase P | 64 -- Subbase P |
53 -- A set of countable intersection of P will be a base (x ix an element of the base) | 65 -- A set of countable intersection of P will be a base (x ix an element of the base) |
54 | 66 |
55 data Subbase (P : HOD) : Ordinal → Set n where | 67 data Subbase (P : HOD) : Ordinal → Set n where |
86 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | 98 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) |
87 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) | 99 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) |
88 | 100 |
89 record IsSubBase (L P : HOD) : Set (suc n) where | 101 record IsSubBase (L P : HOD) : Set (suc n) where |
90 field | 102 field |
91 P⊆PL : P ⊆ Power L | 103 P⊆PL : P ⊆ Power L |
92 -- we may need these if OS ∋ L is necessary | 104 -- we may need these if OS ∋ L is necessary |
93 -- p : {x : HOD} → L ∋ x → HOD | 105 -- p : {x : HOD} → L ∋ x → HOD |
94 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx | 106 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx |
95 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x | 107 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x |
96 | 108 |
97 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L | 109 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
98 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 | 110 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
99 ; o∪ = tp02 ; o∩ = tp01 } where | 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 )) | |
100 tp00 : SO L P ⊆ Power L | 114 tp00 : SO L P ⊆ Power L |
101 tp00 {u} ou x ux with ou ux | 115 tp00 {u} ou x ux with ou ux |
102 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) | 116 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) |
103 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) | 117 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
104 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul | 118 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul |
151 | 165 |
152 -- Finite Intersection Property | 166 -- Finite Intersection Property |
153 | 167 |
154 record FIP {L : HOD} (top : Topology L) : Set n where | 168 record FIP {L : HOD} (top : Topology L) : Set n where |
155 field | 169 field |
156 finite : {X : Ordinal } → * X ⊆ CS top | 170 limit : {X : Ordinal } → * X ⊆ CS top → * X ∋ L |
157 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal | 171 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal |
158 limit : {X : Ordinal } → (CX : * X ⊆ CS top ) | 172 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L ) |
159 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) | 173 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) |
160 → {x : Ordinal } → odef (* X) x → odef (* x) (finite CX fip) | 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) | |
161 | 179 |
162 -- Compact | 180 -- Compact |
163 | 181 |
164 data Finite-∪ (S : HOD) : Ordinal → Set n where | 182 data Finite-∪ (S : HOD) : Ordinal → Set n where |
165 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x | 183 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x |
194 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥ | 212 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥ |
195 fip03 {x} {z} xz nxz = nxz xz | 213 fip03 {x} {z} xz nxz = nxz xz |
196 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | 214 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x |
197 fip02 = ? | 215 fip02 = ? |
198 fip01 : Ordinal | 216 fip01 : Ordinal |
199 fip01 = FIP.finite fip (CCX ox) fip02 | 217 fip01 = FIP.limit fip (CCX ox) ? fip02 |
200 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ | 218 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ |
201 ¬CXfip {X} ox oc = ? where | 219 ¬CXfip {X} ox oc = ? where |
202 fip04 : odef (Cex ox) (cex ox oc) | 220 fip04 : odef (Cex ox) (cex ox oc) |
203 fip04 = ? | 221 fip04 = ? |
204 -- this defines finite cover | 222 -- this defines finite cover |
260 | 278 |
261 open Filter | 279 open Filter |
262 | 280 |
263 -- Ultra Filter has limit point | 281 -- Ultra Filter has limit point |
264 | 282 |
265 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 | 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 | |
266 field | 285 field |
267 limit : Ordinal | 286 limit : Ordinal |
268 P∋limit : odef P limit | 287 P∋limit : odef P limit |
269 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F | 288 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F |
270 | 289 |
271 -- FIP is UFL | 290 -- FIP is UFL |
272 | 291 |
273 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP | 292 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
274 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf | 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 |
275 FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } | 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 | |
276 | 313 |
277 UFLP→FIP : {P : HOD} (TP : Topology P) → | 314 UFLP→FIP : {P : HOD} (TP : Topology P) → |
278 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP | 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 |
279 UFLP→FIP {P} TP uflp = record { fip≠φ = ? } | 316 UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? } |
280 | 317 |
281 -- Product of UFL has limit point (Tychonoff) | 318 -- Product of UFL has limit point (Tychonoff) |
282 | 319 |
283 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) | 320 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) |
284 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where | 321 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where |
285 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) | 322 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (LF : filter F ∋ ZFP P Q) |
286 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf | 323 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F ? uf |
287 uflp {L} LPQ F uf = record { limit = & < * ( UFLP.limit uflpp) , ? > ; P∋limit = ? ; is-limit = ? } where | 324 uflp {L} LPQ F LF uf = record { limit = & < * ( UFLP.limit uflpp) , ? > ; P∋limit = ? ; is-limit = ? } where |
288 LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD | 325 LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD |
289 LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) | 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 )))) ) |
290 LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P | 327 LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P |
291 LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) | 328 LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) |
292 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where | 329 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where |
299 FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where | 336 FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where |
300 tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ | 337 tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ |
301 tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } | 338 tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } |
302 uFP : ultra-filter FP | 339 uFP : ultra-filter FP |
303 uFP = record { proper = ? ; ultra = ? } | 340 uFP = record { proper = ? ; ultra = ? } |
304 uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP | 341 uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP ? uFP |
305 uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP | 342 uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP ? uFP |
306 LQ : HOD | 343 LQ : HOD |
307 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) | 344 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) |
308 LQQ : LQ ⊆ Power Q | 345 LQQ : LQ ⊆ Power Q |
309 LQQ = ? | 346 LQQ = ? |
310 | 347 |