Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1116:6386019deef1
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Jan 2023 20:03:29 +0900 |
parents | 97f4a14d88ce |
children | 53ca3c609f0e |
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 |
1101 | 42 -- closed Set |
43 CS : HOD | |
44 CS = record { od = record { def = λ x → odef OS (& ( L \ (* x ))) } ; odmax = & L ; <odmax = tp02 } where | |
45 tp02 : {y : Ordinal } → odef OS (& (L \ * y)) → y o< & L | |
46 tp02 {y} nop = ? | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
47 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
1108 | 48 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
1101 | 49 -- ∈∅< ( proj1 nop ) |
431 | 50 |
482 | 51 open Topology |
431 | 52 |
1107 | 53 -- Base |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
54 -- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that |
1107 | 55 -- W ⊆ U ∩ V and x ∈ W . |
56 | |
57 data Subbase (P : HOD) : Ordinal → Set n where | |
58 gi : {x : Ordinal } → odef P x → Subbase P x | |
59 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
60 | |
1111 | 61 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
62 sbp P {x} (gi {y} px) = x | |
63 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
1107 | 64 |
1111 | 65 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
66 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
|
67 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
1107 | 68 |
1115 | 69 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } |
1114 | 70 |
1115 | 71 record Base (L P : HOD) (u x : Ordinal) : Set n where |
1114 | 72 field |
73 b : Ordinal | |
1115 | 74 u⊂L : * u ⊂ L |
1114 | 75 sb : Subbase P b |
76 b⊆u : * b ⊆ * u | |
77 bx : odef (* b) x | |
78 | |
1115 | 79 SO : (L P : HOD) → HOD |
80 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? } | |
1114 | 81 |
1111 | 82 record IsSubBase (L P : HOD) : Set (suc n) where |
1110 | 83 field |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
84 P⊆PL : P ⊆ Power L |
1116 | 85 |
86 -- we may need these if OS ∋ L is necessary | |
87 -- p : {x : HOD} → L ∋ x → HOD | |
88 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx | |
89 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x | |
1110 | 90 |
1111 | 91 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
1115 | 92 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
93 ; o∪ = tp02 ; o∩ = tp01 } where | |
94 tp00 : SO L P ⊆ Power L | |
95 tp00 {u} ou x ux with ou ux | |
96 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = proj2 u⊂L (b⊆u bx) | |
97 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) | |
98 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊂ L) (sym *iso) ul | |
1116 | 99 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
1115 | 100 px : odef (* (& p)) x |
101 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
102 qx : odef (* (& q)) x | |
103 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
104 b : Ordinal | |
105 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
1116 | 106 tp08 : * b ⊆ * (& (p ∩ q) ) |
107 tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where | |
108 tp11 : * (Base.b (op px)) ⊆ * (& p ) | |
109 tp11 = Base.b⊆u (op px) | |
110 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
111 tp12 = Base.b⊆u (oq qx) | |
112 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p | |
113 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) | |
114 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q | |
115 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) | |
116 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | |
117 tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ | |
1115 | 118 ul : (p ∩ q) ⊂ L |
1116 | 119 ul = subst (λ k → k ⊂ L ) *iso ⟪ tp02 , (λ {z} pq → proj2 (Base.u⊂L (op px)) (pz pq) ) ⟫ where |
120 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z | |
121 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | |
122 tp02 : & (* (& (p ∩ q))) o< & L | |
123 tp02 = subst ( λ k → k o< & L) (sym &iso) ? | |
1115 | 124 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q |
125 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux | |
126 ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
1116 | 127 ... | 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 |
128 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where | |
129 tp05 : Union q ⊆ L | |
130 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
131 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
132 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) | |
133 tp04 : Union q ⊂ L | |
134 tp04 = ⟪ ? , tp05 ⟫ | |
135 tp06 : * b ⊆ Union q | |
136 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } | |
1110 | 137 |
1107 | 138 -- covers |
1101 | 139 |
431 | 140 record _covers_ ( P q : HOD ) : Set (suc n) where |
141 field | |
142 cover : {x : HOD} → q ∋ x → HOD | |
143 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt | |
144 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x | |
145 | |
146 -- Finite Intersection Property | |
147 | |
148 data Finite-∩ (S : HOD) : HOD → Set (suc n) where | |
1101 | 149 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x |
150 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y) | |
431 | 151 |
1102 | 152 record FIP {L : HOD} (top : Topology L) : Set (suc n) where |
431 | 153 field |
1102 | 154 fipS⊆PL : L ⊆ CS top |
155 fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ ) | |
431 | 156 |
157 -- Compact | |
158 | |
159 data Finite-∪ (S : HOD) : HOD → Set (suc n) where | |
1101 | 160 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x |
431 | 161 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y) |
162 | |
1102 | 163 record Compact {L : HOD} (top : Topology L) : Set (suc n) where |
431 | 164 field |
1102 | 165 finCover : {X : HOD} → X ⊆ OS top → X covers L → HOD |
166 isCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L | |
167 isFinite : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp ) | |
431 | 168 |
169 -- FIP is Compact | |
170 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
171 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
1102 | 172 FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? } |
431 | 173 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
174 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
482 | 175 Compact→FIP = {!!} |
431 | 176 |
177 -- Product Topology | |
178 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
179 open ZFProduct |
1101 | 180 |
1102 | 181 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where |
182 field | |
1106 | 183 p q : Ordinal |
1102 | 184 op : odef (OS TP) p |
1106 | 185 prod : x ≡ & (ZFP (* p) Q ) |
1102 | 186 |
187 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where | |
188 field | |
1106 | 189 p q : Ordinal |
1102 | 190 oq : odef (OS TQ) q |
1106 | 191 prod : x ≡ & (ZFP P (* q )) |
192 | |
1107 | 193 -- box : HOD |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
194 -- box = ZFP (OS TP) (OS TQ) |
1107 | 195 |
1106 | 196 base : {P Q : HOD} → Topology P → Topology Q → HOD |
197 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? } | |
198 | |
1101 | 199 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) |
1111 | 200 _Top⊗_ {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (base TP TQ) ? |
431 | 201 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
202 -- existence of Ultra Filter |
431 | 203 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
204 open Filter |
1102 | 205 |
431 | 206 -- Ultra Filter has limit point |
207 | |
1102 | 208 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 |
209 field | |
210 limit : Ordinal | |
211 P∋limit : odef P limit | |
212 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F | |
213 | |
431 | 214 -- FIP is UFL |
215 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
216 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
217 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf |
1102 | 218 FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } |
219 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
220 UFLP→FIP : {P : HOD} (TP : Topology P) → |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
221 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP |
1102 | 222 UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? } |
223 | |
431 | 224 -- Product of UFL has limit point (Tychonoff) |
225 | |
1102 | 226 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ) |
227 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where | |
1104 | 228 uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) |
229 (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf | |
1106 | 230 uflp {L} LPQ F 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
|
231 LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD |
1106 | 232 LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) |
233 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
|
234 LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) |
1105 | 235 (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where |
236 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
|
237 tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) ) |
1105 | 238 (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
|
239 tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1)) |
1105 | 240 tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt) |
1106 | 241 FP : Filter (LPP L LPQ) |
242 FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where | |
243 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
|
244 tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } |
1104 | 245 uFP : ultra-filter FP |
246 uFP = record { proper = ? ; ultra = ? } | |
1106 | 247 uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
248 uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
249 LQ : HOD |
1105 | 250 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) |
1104 | 251 LQQ : LQ ⊆ Power Q |
252 LQQ = ? | |
1102 | 253 |