Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1163:cd54ee498249
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 21 Jan 2023 09:02:52 +0900 |
parents | 0a6040d914f8 |
children | 5e065f0a7ba2 |
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) |
1161 | 42 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P |
1122 | 43 OS∋od∅ : OS ∋ od∅ |
1160 | 44 --- we may add |
45 -- OS∋L : OS ∋ L | |
1101 | 46 -- closed Set |
47 CS : HOD | |
1119 | 48 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
49 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) | |
50 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
|
51 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
1108 | 52 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) |
1122 | 53 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L |
54 cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy ) | |
55 CS∋L : CS ∋ L | |
1123 | 56 CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x) , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅ ⟫ where |
57 lem0 : L \ * (& L) ≡ od∅ | |
58 lem0 = subst (λ k → L \ k ≡ od∅) (sym *iso) L\L=0 | |
1154 | 59 CS⊆PL : CS ⊆ Power L |
1161 | 60 CS⊆PL {x} Cx y xy = proj1 Cx xy |
1160 | 61 P\CS=OS : {cs : HOD} → CS ∋ cs → OS ∋ ( L \ cs ) |
62 P\CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (cong (λ k → & ( L \ k)) *iso) olcs | |
63 P\OS=CS : {cs : HOD} → OS ∋ cs → CS ∋ ( L \ cs ) | |
1161 | 64 P\OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1 |
1160 | 65 , subst (λ k → odef OS k) (cong (&) (trans (sym (L\Lx=x (os⊆L oos))) (cong (λ k → L \ k) (sym *iso)) )) oos ⟫ |
431 | 66 |
482 | 67 open Topology |
431 | 68 |
1163 | 69 -- Closure ( Intersection of Closed Set which include A ) |
70 | |
1162 | 71 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD |
72 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } | |
1150 | 73 ; odmax = & L ; <odmax = odef∧< } |
1122 | 74 |
1162 | 75 ClL : {L : HOD} → (top : Topology L) → Cl top L ≡ L |
76 ClL {L} top = ==→o≡ ( record { eq→ = λ {x} ic | |
1142 | 77 → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) |
78 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) | |
1123 | 79 |
1163 | 80 -- Closure is Closed Set |
81 | |
1162 | 82 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A |
83 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P\OS=CS top UOCl-is-OS) where | |
1163 | 84 OCl : HOD -- set of open set which it not contains A |
1162 | 85 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L \ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< } |
86 OCl⊆OS : OCl ⊆ OS top | |
87 OCl⊆OS ox = proj1 ox | |
88 UOCl-is-OS : OS top ∋ Union OCl | |
89 UOCl-is-OS = o∪ top OCl⊆OS | |
90 cc00 : (L \ Union OCl) =h= Cl top A | |
91 cc00 = record { eq→ = cc01 ; eq← = cc03 } where | |
92 cc01 : {x : Ordinal} → odef (L \ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) | |
93 cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where | |
94 cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x → odef (* c) x | |
95 cc02 c cc ac nox with ODC.∋-p O (* c) (* x) | |
96 ... | yes y = subst (λ k → odef (* c) k) &iso y | |
97 ... | no ncx = ⊥-elim ( nox record { owner = & ( L \ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) (sym *iso) cc06 } ) where | |
98 cc06 : odef (L \ * c) x | |
99 cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫ | |
100 cc08 : * c ⊆ L | |
101 cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc ) | |
102 cc07 : A ⊆ (L \ * (& (L \ * c))) | |
103 cc07 {z} az = subst (λ k → odef k z ) ( | |
104 begin * c ≡⟨ sym ( L\Lx=x cc08 ) ⟩ | |
105 L \ (L \ * c) ≡⟨ cong (λ k → L \ k ) (sym *iso) ⟩ | |
106 L \ * (& (L \ * c)) ∎ ) ( ac az ) where open ≡-Reasoning | |
107 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L \ Union OCl) x | |
108 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where | |
1163 | 109 -- if x is in Cl A, it is in some c : CS, OCl says it is not , i.e. L \ o ∋ x, so it is in (L \ Union OCl) x |
1162 | 110 cc04 : ¬ odef (Union OCl) x |
111 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox where | |
112 cc05 : odef (* (& (L \ * o))) x | |
113 cc05 = ccx (& (L \ * o)) (P\OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) (sym *iso) A⊆L-o) | |
1161 | 114 |
1160 | 115 |
1119 | 116 -- Subbase P |
117 -- A set of countable intersection of P will be a base (x ix an element of the base) | |
1107 | 118 |
119 data Subbase (P : HOD) : Ordinal → Set n where | |
120 gi : {x : Ordinal } → odef P x → Subbase P x | |
121 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
122 | |
1119 | 123 -- |
1150 | 124 -- if y is in a Subbase, some element of P contains it |
1119 | 125 |
1111 | 126 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
127 sbp P {x} (gi {y} px) = x | |
128 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
1107 | 129 |
1111 | 130 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
131 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
|
132 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) |
1107 | 133 |
1155 | 134 sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x |
135 sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px) | |
136 sb⊆ {P} {Q} P⊆Q (g∩ px qx) = g∩ (sb⊆ P⊆Q px) (sb⊆ P⊆Q qx) | |
137 | |
1119 | 138 -- An open set generate from a base |
139 -- | |
1161 | 140 -- OS = { U ⊆ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊆ U } |
1114 | 141 |
1115 | 142 record Base (L P : HOD) (u x : Ordinal) : Set n where |
1114 | 143 field |
1150 | 144 b : Ordinal |
1161 | 145 u⊆L : * u ⊆ L |
1114 | 146 sb : Subbase P b |
147 b⊆u : * b ⊆ * u | |
148 bx : odef (* b) x | |
1150 | 149 x⊆L : odef L x |
1161 | 150 x⊆L = u⊆L (b⊆u bx) |
1114 | 151 |
1115 | 152 SO : (L P : HOD) → HOD |
1119 | 153 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where |
154 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | |
1150 | 155 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) |
1114 | 156 |
1111 | 157 record IsSubBase (L P : HOD) : Set (suc n) where |
1110 | 158 field |
1122 | 159 P⊆PL : P ⊆ Power L |
1116 | 160 -- we may need these if OS ∋ L is necessary |
161 -- p : {x : HOD} → L ∋ x → HOD | |
1161 | 162 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx |
1116 | 163 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x |
1110 | 164 |
1152 | 165 InducedTopology : (L P : HOD) → IsSubBase L P → Topology L |
166 InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00 | |
1122 | 167 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where |
168 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x | |
1150 | 169 tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) |
1115 | 170 tp00 : SO L P ⊆ Power L |
171 tp00 {u} ou x ux with ou ux | |
1161 | 172 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊆L (b⊆u bx) |
1115 | 173 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
1161 | 174 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊆L = subst (λ k → k ⊆ L) (sym *iso) ul |
1116 | 175 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
1115 | 176 px : odef (* (& p)) x |
177 px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) | |
178 qx : odef (* (& q)) x | |
179 qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) ) | |
180 b : Ordinal | |
181 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
1116 | 182 tp08 : * b ⊆ * (& (p ∩ q) ) |
1150 | 183 tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where |
1116 | 184 tp11 : * (Base.b (op px)) ⊆ * (& p ) |
185 tp11 = Base.b⊆u (op px) | |
186 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
187 tp12 = Base.b⊆u (oq qx) | |
1150 | 188 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p |
1116 | 189 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) |
1150 | 190 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q |
1116 | 191 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) |
192 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x | |
193 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
|
194 ul : (p ∩ q) ⊆ L |
1161 | 195 ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq → (Base.u⊆L (op px)) (pz pq) ) where |
1116 | 196 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
197 pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) ) | |
1161 | 198 tp02 : { q : HOD} → q ⊆ SO L P → SO L P ∋ Union q |
199 tp02 {q} q⊆O {x} ux with subst (λ k → odef k x) *iso ux | |
200 ... | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx | |
201 ... | 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 | 202 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where |
203 tp05 : Union q ⊆ L | |
1161 | 204 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx |
205 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
1116 | 206 = 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
|
207 tp04 : Union q ⊆ L |
1150 | 208 tp04 = tp05 |
1116 | 209 tp06 : * b ⊆ Union q |
1150 | 210 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } |
1110 | 211 |
1142 | 212 -- Product Topology |
213 | |
214 open ZFProduct | |
215 | |
1150 | 216 -- Product Topology is not |
1142 | 217 -- ZFP (OS TP) (OS TQ) (box) |
218 | |
219 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where | |
220 field | |
221 p q : Ordinal | |
222 op : odef (OS TP) p | |
223 prod : x ≡ & (ZFP (* p) Q ) | |
224 | |
225 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where | |
226 field | |
227 p q : Ordinal | |
228 oq : odef (OS TQ) q | |
229 prod : x ≡ & (ZFP P (* q )) | |
230 | |
231 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 | |
232 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 | |
233 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) | |
234 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
235 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where | |
236 tp03 : odef P a | |
237 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa | |
238 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 | |
239 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) | |
240 tp01 w wz with subst (λ k → odef k w ) *iso wz | |
241 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where | |
242 tp03 : odef Q b | |
243 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb | |
244 | |
245 pbase : {P Q : HOD} → Topology P → Topology Q → HOD | |
246 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 | |
247 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) | |
1150 | 248 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) |
1142 | 249 |
250 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) | |
1152 | 251 ProductTopology {P} {Q} TP TQ = InducedTopology (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } |
1142 | 252 |
1152 | 253 -- covers ( q ⊆ Union P ) |
1101 | 254 |
1120 | 255 record _covers_ ( P q : HOD ) : Set n where |
431 | 256 field |
1120 | 257 cover : {x : Ordinal } → odef q x → Ordinal |
1145 | 258 P∋cover : {x : Ordinal } → (lt : odef q x) → odef P (cover lt) |
259 isCover : {x : Ordinal } → (lt : odef q x) → odef (* (cover lt)) x | |
1120 | 260 |
261 open _covers_ | |
431 | 262 |
263 -- Finite Intersection Property | |
264 | |
1120 | 265 record FIP {L : HOD} (top : Topology L) : Set n where |
431 | 266 field |
1150 | 267 limit : {X : Ordinal } → * X ⊆ CS top |
1120 | 268 → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal |
1150 | 269 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
270 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) | |
1143 | 271 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) |
1150 | 272 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
273 → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) | |
274 → {x : Ordinal } → odef (* X) x | |
1143 | 275 → odef L (limit CX fip) |
276 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 | 277 |
278 -- Compact | |
279 | |
1119 | 280 data Finite-∪ (S : HOD) : Ordinal → Set n where |
1150 | 281 fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x |
1119 | 282 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) |
431 | 283 |
1120 | 284 record Compact {L : HOD} (top : Topology L) : Set n where |
431 | 285 field |
1120 | 286 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal |
287 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L | |
1150 | 288 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) |
431 | 289 |
290 -- FIP is Compact | |
291 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
292 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
1150 | 293 FIP→Compact {L} top fip with trio< (& L) o∅ |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
294 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1148 | 295 ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where |
296 -- L is empty | |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
297 fip02 : {x : Ordinal } → ¬ odef L x |
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
298 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) ) |
1148 | 299 fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
300 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } |
1148 | 301 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅ |
1150 | 302 fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) ) |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
303 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where |
1121 | 304 -- set of coset of X |
305 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal | |
306 CX {X} ox = & ( Replace' (* X) (λ z xz → L \ z )) | |
1150 | 307 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top |
1143 | 308 CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox |
309 ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L \ * z) | |
310 fip07 : z ≡ & (L \ * x) | |
311 fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L \ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where | |
312 fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L \ * z))) x) → odef (* z) x | |
1150 | 313 fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ |
1143 | 314 ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ ) |
315 fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L \ * z))) x) | |
316 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 | |
317 fip10 : ¬ (odef (L \ * z) w) | |
318 fip10 ⟪ Lw , nzw ⟫ = nzw zw | |
319 fip06 : odef (OS top) (& (L \ * x)) | |
320 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) | |
321 fip05 : * x ⊆ L | |
322 fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw ) | |
323 -- | |
324 -- X covres L means Intersection of (CX X) contains nothing | |
1152 | 325 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) |
1143 | 326 -- it means there is a finite cover |
327 -- | |
1150 | 328 record CFIP (X x : Ordinal) : Set n where |
1143 | 329 field |
1150 | 330 is-CS : * x ⊆ Replace' (* X) (λ z xz → L \ z) |
331 sx : Subbase (* x) o∅ | |
332 Cex : (X : Ordinal ) → HOD | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
333 Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L \ z))) ; <odmax = fip05 } where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
334 fip05 : {y : Ordinal} → CFIP X y → y o< osuc (& (Replace' (* X) (λ z xz → L \ z))) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
335 fip05 {y} cf = subst₂ (λ j k → j o< osuc k ) &iso refl ( ⊆→o≤ ( CFIP.is-CS cf ) ) |
1150 | 336 fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ ) |
337 fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where | |
1148 | 338 -- CX is finite intersection |
339 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x | |
1150 | 340 fip02 {C} {x} C<CX sc with trio< x o∅ |
1148 | 341 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
342 ... | tri> ¬a ¬b c = c | |
343 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* C) k) b sc } )) where | |
1150 | 344 fip10 : * C ⊆ Replace' (* X) (λ z xz → L \ z) |
345 fip10 {w} cw = subst (λ k → odef k w) *iso ( C<CX cw ) | |
346 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) | |
1148 | 347 fip26 : odef (* (CX ox)) (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) |
1150 | 348 fip26 = subst (λ k → odef k (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) |
349 record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } | |
1148 | 350 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) |
351 fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26 | |
352 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) | |
353 fip20 {y} Xy yl = proj2 fip21 yl where | |
354 fip22 : odef (* (CX ox)) (& ( L \ * y )) | |
1150 | 355 fip22 = subst (λ k → odef k (& ( L \ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } |
1148 | 356 fip21 : odef (L \ * y) ( FIP.limit fip (CCX ox) fip02 ) |
357 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) | |
1150 | 358 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) |
1148 | 359 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) |
1121 | 360 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal |
1152 | 361 cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc)) -- this will be the finite cover |
1150 | 362 CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc) |
363 CXfip {X} ox oc = ODC.x∋minimal O (Cex X) (fip00 ox oc) | |
1149 | 364 -- |
1121 | 365 -- this defines finite cover |
1120 | 366 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
1121 | 367 finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L \ z )) |
1150 | 368 -- create Finite-∪ from cex |
1120 | 369 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
1150 | 370 isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where |
371 fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L \ z) → Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L \ z ))) | |
372 fip30 x y x⊆cs (gi sb) = fip31 where | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
373 fip32 : Replace' (* x) (λ z xz → L \ z) ⊆ * X -- x⊆cs :* x ⊆ Replace' (* X) (λ z₁ xz → L \ z₁) , x=ψz : w ≡ & (L \ * z) , odef (* x) z |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
374 fip32 {w} record { z = z ; az = xz ; x=ψz = x=ψz } with x⊆cs xz |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
375 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
376 fip34 : * z1 ⊆ L |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
377 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1 |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
378 fip33 : z1 ≡ w |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
379 fip33 = begin |
1152 | 380 z1 ≡⟨ sym &iso ⟩ |
381 & (* z1) ≡⟨ cong (&) (sym (L\Lx=x fip34 )) ⟩ | |
382 & (L \ ( L \ * z1)) ≡⟨ cong (λ k → & ( L \ k )) (sym *iso) ⟩ | |
383 & (L \ * (& ( L \ * z1))) ≡⟨ cong (λ k → & ( L \ * k )) (sym x=ψz1) ⟩ | |
384 & (L \ * z) ≡⟨ sym x=ψz ⟩ | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
385 w ∎ where open ≡-Reasoning |
1150 | 386 fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L \ z))) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
387 fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 ) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
388 fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
389 fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L \ z₁))) |
1152 | 390 fip35 = subst (λ k → Finite-∪ (* X) k) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
391 (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L \ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _ x⊆cs sy) (fip30 _ _ x⊆cs sz) ) |
1120 | 392 -- is also a cover |
393 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | |
1152 | 394 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L \ k ≡ L) (sym o∅≡od∅) L\0=L) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
395 ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
396 fip45 : {L a b : HOD} → (L \ (a ∩ b)) ⊆ ( (L \ a) ∪ (L \ b)) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
397 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
398 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
399 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
400 fip43 : {A L a b : HOD } → A covers (L \ a) → A covers (L \ b ) → A covers ( L \ ( a ∩ b ) ) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
401 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
402 fip44 : {x : Ordinal} → odef (L \ (a ∩ b)) x → Ordinal |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
403 fip44 {x} Lab with fip45 {L} {a} {b} Lab |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
404 ... | case1 La = cover ca La |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
405 ... | case2 Lb = cover cb Lb |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
406 fip46 : {x : Ordinal} (lt : odef (L \ (a ∩ b)) x) → odef A (fip44 lt) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
407 fip46 {x} Lab with fip45 {L} {a} {b} Lab |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
408 ... | case1 La = P∋cover ca La |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
409 ... | case2 Lb = P∋cover cb Lb |
1152 | 410 fip47 : {x : Ordinal} (lt : odef (L \ (a ∩ b)) x) → odef (* (fip44 lt)) x |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
411 fip47 {x} Lab with fip45 {L} {a} {b} Lab |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
412 ... | case1 La = isCover ca La |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
413 ... | case2 Lb = isCover cb Lb |
1150 | 414 fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L \ z) → Subbase (* x) y |
415 → (Replace' (* x) (λ z xz → L \ z )) covers (L \ * y ) | |
1152 | 416 fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L \ z)) covers ( L \ k ) ) (sym *iso) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
417 ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
418 fip41 : Replace' (* x) (λ z xz → L \ z) covers (L \ * a) |
1152 | 419 fip41 = fip40 x a x⊆r sa |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
420 fip42 : Replace' (* x) (λ z xz → L \ z) covers (L \ * b) |
1152 | 421 fip42 = fip40 x b x⊆r sb |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
422 fip40 x y x⊆r (gi sb) with x⊆r sb |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
423 ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where |
1152 | 424 fip51 : {w : Ordinal} (Lyw : odef (L \ * y) w) → Ordinal |
425 fip51 {w} Lyw = z | |
426 fip52 : {w : Ordinal} (Lyw : odef (L \ * y) w) → odef (* X) z | |
427 fip52 {w} Lyw = az | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
428 fip55 : * z ⊆ L |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
429 fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1 |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
430 fip56 : * z ≡ L \ * y |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
431 fip56 = begin |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
432 * z ≡⟨ sym (L\Lx=x fip55 ) ⟩ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
433 L \ ( L \ * z ) ≡⟨ cong (λ k → L \ k) (sym *iso) ⟩ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
434 L \ * ( & ( L \ * z )) ≡⟨ cong (λ k → L \ * k) (sym x=ψz) ⟩ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
435 L \ * y ∎ where open ≡-Reasoning |
1152 | 436 fip53 : {w : Ordinal} (Lyw : odef (L \ * y) w) → odef (Replace' (* x) (λ z₁ xz → L \ z₁)) z |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
437 fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
438 fip54 : z ≡ & ( L \ * y ) |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
439 fip54 = begin |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
440 z ≡⟨ sym &iso ⟩ |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
441 & (* z) ≡⟨ cong (&) fip56 ⟩ |
1152 | 442 & (L \ * y ) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
443 ∎ where open ≡-Reasoning |
1152 | 444 fip50 : {w : Ordinal} (Lyw : odef (L \ * y) w) → odef (* z) w |
445 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
446 |
1158 | 447 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
448 Compact→FIP = ? | |
431 | 449 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
450 -- existence of Ultra Filter |
431 | 451 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
452 open Filter |
1102 | 453 |
431 | 454 -- Ultra Filter has limit point |
455 | |
1159 | 456 record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where |
457 field | |
458 u : Ordinal | |
459 ou : odef (OS TP) u | |
460 ux : odef (* u) x | |
461 v⊆P : * v ⊆ P | |
462 o⊆u : * u ⊆ * v | |
463 | |
1150 | 464 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) |
1155 | 465 (ultra : ultra-filter F ) : Set (suc (suc n)) where |
1102 | 466 field |
467 limit : Ordinal | |
468 P∋limit : odef P limit | |
1159 | 469 is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v) |
1102 | 470 |
431 | 471 -- FIP is UFL |
472 | |
1159 | 473 -- filter Base |
474 record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where | |
1153 | 475 field |
1161 | 476 b x : Ordinal |
1155 | 477 b⊆X : * b ⊆ * X |
1161 | 478 sb : Subbase (* b) x |
1158 | 479 u⊆P : * u ⊆ P |
1154 | 480 x⊆u : * x ⊆ * u |
1155 | 481 |
482 open import maximum-filter O | |
1153 | 483 |
1161 | 484 UFLP→FIP : {P : HOD} (TP : Topology P) → |
1155 | 485 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP |
1163 | 486 UFLP→FIP {P} TP uflp with trio< (& P) o∅ |
487 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
488 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where | |
489 -- P is empty | |
490 fip02 : {x : Ordinal } → ¬ odef P x | |
491 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) ) | |
492 ... | tri> ¬a ¬b 0<P = record { limit = uf00 ; is-limit = {!!} } where | |
1143 | 493 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
1153 | 494 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x |
1154 | 495 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
1161 | 496 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
1159 | 497 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
1158 | 498 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
1159 | 499 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
1158 | 500 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) |
501 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where | |
502 f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q | |
1161 | 503 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = |
504 record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → | |
1158 | 505 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where |
506 f10 : q ⊆ P | |
507 f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) | |
508 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) | |
509 f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where | |
510 p∩q⊆p : * (& (p ∩ q)) ⊆ P | |
511 p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) | |
1159 | 512 Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) |
513 xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) | |
1155 | 514 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) |
1159 | 515 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) |
1155 | 516 f20 : * (& Np+Nq) ⊆ * X |
517 f20 {x} npq with subst (λ k → odef k x) *iso npq | |
1159 | 518 ... | case1 np = FBase.b⊆X Np np |
519 ... | case2 nq = FBase.b⊆X Nq nq | |
1155 | 520 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q)) |
1161 | 521 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq |
1159 | 522 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) |
1155 | 523 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅) |
524 proper = ? | |
1158 | 525 CAP : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q) |
526 CAP {X} CSX fp {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) *iso pqx | |
527 ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px ) | |
528 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) | |
529 maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp) | |
1143 | 530 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
1161 | 531 uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x) |
1155 | 532 ( MaximumFilter.mf (maxf CSX fp) ) |
1158 | 533 (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp))) |
1142 | 534 |
1158 | 535 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
536 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF | |
1162 | 537 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where |
1160 | 538 CF : HOD |
1162 | 539 CF = Replace' (filter F) (λ x fx → Cl TP x ) |
1160 | 540 CF⊆CS : CF ⊆ CS TP |
1162 | 541 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) |
542 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x | |
543 ufl01 = ? | |
1159 | 544 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v |
545 ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ? | |
1102 | 546 |
1163 | 547 FilterProduct : {P Q LP LQ : HOD } |
548 → (LPP : LP ⊆ Power P) (FP : Filter {LP} LPP) | |
549 → (LPQ : LQ ⊆ Power Q) (FQ : Filter {LQ} LPQ) | |
550 → Filter {ZFP LP LQ} ? | |
551 FilterProduct = ? | |
552 | |
553 FilterProj : {P Q LPQ : HOD } | |
554 → ( LPPQ : LPQ ⊆ Power (ZFP P Q)) | |
555 → Filter {LPQ} LPPQ | |
556 → (Filter {Proj1PP LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2PP LPQ (Power P) (Power Q)} ?) | |
557 FilterProj = ? | |
558 | |
559 ProuctLimit→ProjLimit : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) | |
560 → ( {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF ) | |
561 → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TP LP F UF) | |
562 ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TQ LP F UF) | |
563 ProuctLimit→ProjLimit = ? | |
564 | |
565 ProjLimit→ProductLimit : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) | |
566 → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TP LP F UF) | |
567 ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) → UFLP TQ LP F UF) | |
568 → {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF | |
569 ProjLimit→ProductLimit = ? | |
570 | |
1124 | 571 -- product topology of compact topology is compact |
431 | 572 |
1142 | 573 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) |
1158 | 574 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where |
1159 | 575 uflP : {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) |
1158 | 576 → UFLP TP LP F UF |
1159 | 577 uflP {L} LP F UF = FIP→UFLP TP (Compact→FIP TP CP) LP F UF |
578 uflQ : {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) | |
1158 | 579 → UFLP TQ LP F UF |
1159 | 580 uflQ {L} LP F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) LP F UF |
581 -- Product of UFL has limit point | |
582 uflPQ : {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) | |
1158 | 583 → UFLP (ProductTopology TP TQ) LPQ F UF |
1159 | 584 uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , {!!} > ; P∋limit = {!!} ; is-limit = {!!} } where |
585 LP : HOD -- proj1 of LPQ | |
586 LP = Proj1PP L (Power P) (Power Q) | |
587 LPP : LP ⊆ Power P | |
588 LPP {x} ⟪ Px , p1 ⟫ = Px | |
589 FP : Filter {LP} {P} LPP | |
590 FP = record { filter = Proj1PP (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where | |
591 ty00 : Proj1PP (filter F) (Power P) (Power Q) ⊆ LP | |
592 ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = PProj1.pq (ppf y) | |
593 ; opq = PProj1.opq (ppf y) ; Lpq = f⊆L F (PProj1.Lpq (ppf y)) ; x=pi1 = PProj1.x=pi1 (ppf y) } ) ⟫ | |
1161 | 594 UFP : ultra-filter FP |
1159 | 595 UFP = record { proper = ? ; ultra = ? } |
1158 | 596 uflp : UFLP TP LPP FP UFP |
1159 | 597 uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP |
1154 | 598 |
599 | |
600 |