Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1145:f8c3537e68a6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 16 Jan 2023 02:22:03 +0900 |
parents | 73b256c5474b |
children | 1966127fc14f |
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 |
1143 | 15 open import Relation.Binary.Definitions |
431 | 16 open import Relation.Binary.PropositionalEquality |
1124 | 17 import BAlgebra |
18 open BAlgebra O | |
431 | 19 open inOrdinal O |
20 open OD O | |
21 open OD.OD | |
22 open ODAxiom odAxiom | |
23 import OrdUtil | |
24 import ODUtil | |
25 open Ordinals.Ordinals O | |
26 open Ordinals.IsOrdinals isOrdinal | |
27 open Ordinals.IsNext isNext | |
28 open OrdUtil O | |
29 open ODUtil O | |
30 | |
31 import ODC | |
32 open ODC O | |
33 | |
1102 | 34 open import filter O |
1101 | 35 open import OPair O |
36 | |
482 | 37 record Topology ( L : HOD ) : Set (suc n) where |
431 | 38 field |
39 OS : HOD | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
40 OS⊆PL : OS ⊆ Power L |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
41 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
|
42 o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P |
1122 | 43 OS∋od∅ : OS ∋ od∅ |
1101 | 44 -- closed Set |
45 CS : HOD | |
1119 | 46 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
47 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) | |
48 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
|
49 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
1108 | 50 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
1122 | 51 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L |
52 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) | |
53 CS∋L : CS ∋ L | |
1123 | 54 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where |
55 lem0 : L \ * (& L) ≡ od∅ | |
56 lem0 = subst (λ k → L \ k ≡ od∅) (sym *iso) L\L=0 | |
1122 | 57 --- we may add |
58 -- OS∋L : OS ∋ L | |
431 | 59 |
482 | 60 open Topology |
431 | 61 |
1122 | 62 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD |
1142 | 63 Cl {L} top A A⊆L = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } |
64 ; odmax = & L ; <odmax = odef∧< } | |
1122 | 65 |
1123 | 66 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L |
67 ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic | |
1142 | 68 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) |
69 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) | |
1123 | 70 |
1119 | 71 -- Subbase P |
72 -- A set of countable intersection of P will be a base (x ix an element of the base) | |
1107 | 73 |
74 data Subbase (P : HOD) : Ordinal → Set n where | |
75 gi : {x : Ordinal } → odef P x → Subbase P x | |
76 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
77 | |
1119 | 78 -- |
79 -- if y is in a Subbase, some element of P contains it | |
80 | |
1111 | 81 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
82 sbp P {x} (gi {y} px) = x | |
83 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
1107 | 84 |
1111 | 85 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
86 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
|
87 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
1107 | 88 |
1119 | 89 -- An open set generate from a base |
90 -- | |
1115 | 91 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } |
1114 | 92 |
1115 | 93 record Base (L P : HOD) (u x : Ordinal) : Set n where |
1114 | 94 field |
95 b : Ordinal | |
1117
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
96 u⊂L : * u ⊆ L |
1114 | 97 sb : Subbase P b |
98 b⊆u : * b ⊆ * u | |
99 bx : odef (* b) x | |
1119 | 100 x⊆L : odef L x |
101 x⊆L = u⊂L (b⊆u bx) | |
1114 | 102 |
1115 | 103 SO : (L P : HOD) → HOD |
1119 | 104 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where |
105 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | |
106 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) | |
1114 | 107 |
1111 | 108 record IsSubBase (L P : HOD) : Set (suc n) where |
1110 | 109 field |
1122 | 110 P⊆PL : P ⊆ Power L |
1116 | 111 -- we may need these if OS ∋ L is necessary |
112 -- p : {x : HOD} → L ∋ x → HOD | |
113 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx | |
114 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x | |
1110 | 115 |
1111 | 116 GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L |
1115 | 117 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 |
1122 | 118 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where |
119 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x | |
120 tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) | |
1115 | 121 tp00 : SO L P ⊆ Power L |
122 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
|
123 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) |
1115 | 124 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
|
125 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul |
1116 | 126 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
1115 | 127 px : odef (* (& p)) x |
128 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
129 qx : odef (* (& q)) x | |
130 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
131 b : Ordinal | |
132 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
1116 | 133 tp08 : * b ⊆ * (& (p ∩ q) ) |
134 tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where | |
135 tp11 : * (Base.b (op px)) ⊆ * (& p ) | |
136 tp11 = Base.b⊆u (op px) | |
137 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
138 tp12 = Base.b⊆u (oq qx) | |
139 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p | |
140 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) | |
141 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q | |
142 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) | |
143 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | |
144 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
|
145 ul : (p ∩ q) ⊆ L |
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
146 ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq → (Base.u⊂L (op px)) (pz pq) ) where |
1116 | 147 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
148 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | |
1115 | 149 tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q |
150 tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux | |
151 ... | 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
|
152 ... | 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 | 153 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where |
154 tp05 : Union q ⊆ L | |
155 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx | |
156 ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
157 = 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
|
158 tp04 : Union q ⊆ L |
53ca3c609f0e
generated topology from subbase done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1116
diff
changeset
|
159 tp04 = tp05 |
1116 | 160 tp06 : * b ⊆ Union q |
161 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } | |
1110 | 162 |
1142 | 163 -- Product Topology |
164 | |
165 open ZFProduct | |
166 | |
167 -- Product Topology is not | |
168 -- ZFP (OS TP) (OS TQ) (box) | |
169 | |
170 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where | |
171 field | |
172 p q : Ordinal | |
173 op : odef (OS TP) p | |
174 prod : x ≡ & (ZFP (* p) Q ) | |
175 | |
176 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where | |
177 field | |
178 p q : Ordinal | |
179 oq : odef (OS TQ) q | |
180 prod : x ≡ & (ZFP P (* q )) | |
181 | |
182 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 | |
183 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 | |
184 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) | |
185 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
186 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where | |
187 tp03 : odef P a | |
188 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa | |
189 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 | |
190 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) | |
191 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
192 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where | |
193 tp03 : odef Q b | |
194 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb | |
195 | |
196 pbase : {P Q : HOD} → Topology P → Topology Q → HOD | |
197 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 | |
198 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) | |
199 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) | |
200 | |
201 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) | |
202 ProductTopology {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } | |
203 | |
1107 | 204 -- covers |
1101 | 205 |
1120 | 206 record _covers_ ( P q : HOD ) : Set n where |
431 | 207 field |
1120 | 208 cover : {x : Ordinal } → odef q x → Ordinal |
1145 | 209 P∋cover : {x : Ordinal } → (lt : odef q x) → odef P (cover lt) |
210 isCover : {x : Ordinal } → (lt : odef q x) → odef (* (cover lt)) x | |
1120 | 211 |
212 open _covers_ | |
431 | 213 |
214 -- Finite Intersection Property | |
215 | |
1120 | 216 record FIP {L : HOD} (top : Topology L) : Set n where |
431 | 217 field |
1143 | 218 limit : {X : Ordinal } → * X ⊆ CS top |
1120 | 219 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal |
1143 | 220 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
1120 | 221 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) |
1143 | 222 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) |
223 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) | |
1122 | 224 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) |
1143 | 225 → {x : Ordinal } → odef (* X) x |
226 → odef L (limit CX fip) | |
227 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) | |
431 | 228 |
229 -- Compact | |
230 | |
1119 | 231 data Finite-∪ (S : HOD) : Ordinal → Set n where |
232 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x | |
233 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) | |
431 | 234 |
1120 | 235 record Compact {L : HOD} (top : Topology L) : Set n where |
431 | 236 field |
1120 | 237 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal |
238 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L | |
239 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) | |
431 | 240 |
241 -- FIP is Compact | |
242 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
243 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
1120 | 244 FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where |
1121 | 245 -- set of coset of X |
246 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal | |
247 CX {X} ox = & ( Replace' (* X) (λ z xz → L \ z )) | |
248 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top | |
1143 | 249 CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox |
250 ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L \ * z) | |
251 fip07 : z ≡ & (L \ * x) | |
252 fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L \ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where | |
253 fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L \ * z))) x) → odef (* z) x | |
254 fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ | |
255 ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ ) | |
256 fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L \ * z))) x) | |
257 fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , subst (λ k → ¬ odef k w) (sym *iso) fip10 ⟫ where | |
258 fip10 : ¬ (odef (L \ * z) w) | |
259 fip10 ⟪ Lw , nzw ⟫ = nzw zw | |
260 fip06 : odef (OS top) (& (L \ * x)) | |
261 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) | |
262 fip05 : * x ⊆ L | |
263 fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw ) | |
1121 | 264 -- CX has finite intersection |
265 CXfip : {X : Ordinal } → * X ⊆ OS top → Set n | |
266 CXfip {X} ox = { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | |
1143 | 267 -- |
268 -- X covres L means Intersection of (CX X) contains nothing | |
269 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP ) | |
270 -- it means there is a finite cover | |
271 -- | |
272 record CFIP (x : Ordinal) : Set n where | |
273 field | |
274 is-CS : * x ⊆ CS top | |
275 y : Ordinal | |
1144 | 276 sy : Subbase (* y) o∅ |
1143 | 277 Cex : HOD |
278 Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → | |
279 subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) } | |
1121 | 280 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal |
1143 | 281 cex {X} ox oc = & ( ODC.minimal O Cex fip00) where |
282 fip00 : ¬ ( Cex =h= od∅ ) | |
1145 | 283 fip00 cex=0 = ⊥-elim (fip09 fip25 fip20) where |
1121 | 284 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥ |
285 fip03 {x} {z} xz nxz = nxz xz | |
286 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | |
1143 | 287 fip02 {C} {x} C<CX sc with trio< x o∅ |
288 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
289 ... | tri> ¬a ¬b c = c | |
1144 | 290 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where |
1143 | 291 fip10 : * C ⊆ CS top |
1144 | 292 fip10 {w} cw = CCX ox ( C<CX cw ) |
1145 | 293 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) |
294 fip25 = FIP.L∋limit fip (CCX ox) fip02 ? | |
295 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) | |
296 fip20 {y} Xy yl = proj2 fip21 yl where | |
297 fip22 : odef (* (CX ox)) (& ( L \ * y )) | |
298 fip22 = subst (λ k → odef k (& ( L \ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } | |
299 fip21 : odef (L \ * y) ( FIP.limit fip (CCX ox) fip02 ) | |
300 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) | |
301 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) | |
302 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) | |
1121 | 303 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ |
1124 | 304 ¬CXfip {X} ox oc = {!!} where |
1143 | 305 fip04 : odef Cex (cex ox oc) |
1124 | 306 fip04 = {!!} |
1121 | 307 -- this defines finite cover |
1120 | 308 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
1121 | 309 finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L \ z )) |
1142 | 310 -- create Finite-∪ from cex |
1120 | 311 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
1124 | 312 isFinite = {!!} |
1120 | 313 -- is also a cover |
314 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | |
1124 | 315 isCover1 = {!!} |
1120 | 316 |
431 | 317 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
318 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
482 | 319 Compact→FIP = {!!} |
431 | 320 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
321 -- existence of Ultra Filter |
431 | 322 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
323 open Filter |
1102 | 324 |
431 | 325 -- Ultra Filter has limit point |
326 | |
1142 | 327 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) |
328 (FL : filter F ∋ P) (ultra : ultra-filter F ) : Set (suc (suc n)) where | |
1102 | 329 field |
330 limit : Ordinal | |
331 P∋limit : odef P limit | |
332 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F | |
333 | |
431 | 334 -- FIP is UFL |
335 | |
1142 | 336 UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) → |
337 ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP | |
338 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where | |
1143 | 339 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
340 fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x | |
341 F : Filter {L} {P} LP | |
1142 | 342 F = ? |
1143 | 343 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
344 uf00 {X} CSX fip = UFLP.limit ( uflp F ? (F→ultra LP ? ? F ? ? ? ) ) | |
345 | |
1142 | 346 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
347 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
1142 | 348 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF |
349 FIP→UFLP {P} TP fip {L} LP F FP UF = ? | |
1102 | 350 |
1124 | 351 -- product topology of compact topology is compact |
431 | 352 |
1142 | 353 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) |
354 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) LPQ uflp ) where | |
355 L = pbase TP TQ | |
356 LPQ = pbase⊆PL TP TQ | |
1124 | 357 -- Product of UFL has limit point |
1142 | 358 uflp : (F : Filter {pbase TP TQ} LPQ) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F) |
359 → UFLP (ProductTopology TP TQ) LPQ F LF UF | |
360 uflp F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} } |