Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Topology.agda @ 1485:5dacb669f13b
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 01 Jul 2024 15:43:35 +0900 |
parents | 0b30bb7c7501 |
children | 49c3ef1e9b4f |
rev | line source |
---|---|
1476 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
2 open import Level | |
3 open import Ordinals | |
4 open import logic | |
5 open import Relation.Nullary | |
1170 | 6 |
431 | 7 open import Level |
8 open import Ordinals | |
1476 | 9 import HODBase |
10 import OD | |
11 open import Relation.Nullary | |
12 module Topology {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) | |
13 (AC : OD.AxiomOfChoice O HODAxiom ) where | |
14 | |
15 | |
16 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
17 open import Relation.Binary.Definitions | |
18 | |
19 open import Data.Empty | |
20 | |
21 import OrdUtil | |
22 | |
23 open Ordinals.Ordinals O | |
24 open Ordinals.IsOrdinals isOrdinal | |
25 import ODUtil | |
431 | 26 |
27 open import logic | |
1476 | 28 open import nat |
29 | |
30 open OrdUtil O | |
31 open ODUtil O HODAxiom ho< | |
32 | |
431 | 33 open _∧_ |
34 open _∨_ | |
35 open Bool | |
36 | |
1476 | 37 open HODBase._==_ |
38 | |
39 open HODBase.ODAxiom HODAxiom | |
40 open OD O HODAxiom | |
41 | |
42 open HODBase.HOD | |
43 | |
44 open AxiomOfChoice AC | |
45 open import ODC O HODAxiom AC as ODC | |
46 | |
47 open import Level | |
48 open import Ordinals | |
49 | |
50 import filter | |
51 | |
52 open import Relation.Nullary | |
53 -- open import Relation.Binary hiding ( _⇔_ ) | |
54 open import Data.Empty | |
431 | 55 open import Relation.Binary.PropositionalEquality |
1476 | 56 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
57 import BAlgebra | |
431 | 58 |
1476 | 59 open import ZProduct O HODAxiom ho< |
60 open import filter O HODAxiom ho< AC | |
431 | 61 |
1484 | 62 import Relation.Binary.Reasoning.Setoid as EqHOD |
63 | |
64 LDec : (L : HOD) (P : HOD) → P ⊆ L → (x : HOD) → Dec (x ∈ P) | |
65 LDec L P _ x = ∋-p P x | |
1101 | 66 |
482 | 67 record Topology ( L : HOD ) : Set (suc n) where |
431 | 68 field |
69 OS : HOD | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
70 OS⊆PL : OS ⊆ Power L |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
71 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) |
1161 | 72 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P |
1210 | 73 OS∋od∅ : OS ∋ od∅ -- OS ∋ Union od∅ |
1160 | 74 --- we may add |
75 -- OS∋L : OS ∋ L | |
1101 | 76 -- closed Set |
1484 | 77 open BAlgebra O HODAxiom ho< L (LDec L) |
1101 | 78 CS : HOD |
1119 | 79 CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L \ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where |
80 tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L \ * y)) → y o< osuc (& L) | |
81 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
|
82 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L |
1484 | 83 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (eq← *iso xy) |
1122 | 84 cs⊆L : {x : HOD} → CS ∋ x → x ⊆ L |
1484 | 85 cs⊆L {x} Cx {y} xy = proj1 Cx (eq← *iso xy) |
1122 | 86 CS∋L : CS ∋ L |
1484 | 87 CS∋L = ⟪ (λ lt → eq→ *iso lt) , subst (λ k → odef OS k) (sym lem0) OS∋od∅ ⟫ where |
88 lem0 : & (L \ * (& L)) ≡ & od∅ | |
1485 | 89 lem0 = ==→o≡ ( ==-trans (\-cong L L (* (& L)) L ==-refl *iso ) L\L=0 ) |
1154 | 90 CS⊆PL : CS ⊆ Power L |
1161 | 91 CS⊆PL {x} Cx y xy = proj1 Cx xy |
1160 | 92 P\CS=OS : {cs : HOD} → CS ∋ cs → OS ∋ ( L \ cs ) |
1485 | 93 P\CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (==→o≡ (\-cong L L (* (& cs)) cs ==-refl *iso)) olcs |
1160 | 94 P\OS=CS : {cs : HOD} → OS ∋ cs → CS ∋ ( L \ cs ) |
1484 | 95 P\OS=CS {os} oos = ⟪ (λ lt → proj1 (eq→ *iso lt)) |
96 , subst (λ k → odef OS k) (==→o≡ (==-sym (==-trans ( | |
1485 | 97 \-cong L L (* ( & (L \ os))) (L \ os) ==-refl *iso ) (L\Lx=x {os} (os⊆L oos)) ))) oos ⟫ |
1484 | 98 |
431 | 99 |
482 | 100 open Topology |
431 | 101 |
1163 | 102 -- Closure ( Intersection of Closed Set which include A ) |
103 | |
1162 | 104 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD |
105 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } | |
1150 | 106 ; odmax = & L ; <odmax = odef∧< } |
1122 | 107 |
1476 | 108 ClL : {L : HOD} → (top : Topology L) → Cl top L =h= L |
109 ClL {L} top = record { eq→ = λ {x} ic | |
1484 | 110 → eq→ *iso ((proj2 ic) (& L) (CS∋L top) (λ lt → eq← *iso lt)) |
1476 | 111 ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } |
1123 | 112 |
1163 | 113 -- Closure is Closed Set |
114 | |
1484 | 115 |
1162 | 116 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A |
1484 | 117 CS∋Cl {L} top A = subst (λ k → odef (CS top) k) (==→o≡ cc00) (P\OS=CS top UOCl-is-OS) where |
118 open BAlgebra O HODAxiom ho< L (LDec L) | |
1163 | 119 OCl : HOD -- set of open set which it not contains A |
1162 | 120 OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L \ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< } |
121 OCl⊆OS : OCl ⊆ OS top | |
122 OCl⊆OS ox = proj1 ox | |
123 UOCl-is-OS : OS top ∋ Union OCl | |
124 UOCl-is-OS = o∪ top OCl⊆OS | |
125 cc00 : (L \ Union OCl) =h= Cl top A | |
126 cc00 = record { eq→ = cc01 ; eq← = cc03 } where | |
127 cc01 : {x : Ordinal} → odef (L \ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) | |
128 cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where | |
129 cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x → odef (* c) x | |
1476 | 130 cc02 c cc ac nox with ODC.∋-p (* c) (* x) |
1162 | 131 ... | yes y = subst (λ k → odef (* c) k) &iso y |
1484 | 132 ... | no ncx = ⊥-elim ( nox record { owner = & ( L \ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = eq← *iso cc06 } ) where |
1162 | 133 cc06 : odef (L \ * c) x |
134 cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫ | |
135 cc08 : * c ⊆ L | |
136 cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc ) | |
1484 | 137 cc09 : (L \ * (& (L \ * c))) =h= (* c) |
138 cc09 = begin | |
1485 | 139 L \ * (& (L \ * c)) ≈⟨ \-cong L L (* (& (L \ * c))) (L \ * c) ==-refl *iso ⟩ |
1484 | 140 L \ (L \ * c) ≈⟨ L\Lx=x {* c} cc08 ⟩ |
141 * c ∎ | |
142 where open EqHOD ==-Setoid | |
1162 | 143 cc07 : A ⊆ (L \ * (& (L \ * c))) |
1484 | 144 cc07 {z} az = eq← cc09 ( ac az ) |
1162 | 145 cc03 : {x : Ordinal} → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L \ Union OCl) x |
146 cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where | |
1163 | 147 -- 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 | 148 cc04 : ¬ odef (Union OCl) x |
1484 | 149 cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( eq→ *iso cc05) ox where |
1162 | 150 cc05 : odef (* (& (L \ * o))) x |
1484 | 151 cc05 = ccx (& (L \ * o)) (P\OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (λ lt → eq← *iso (A⊆L-o lt)) |
1161 | 152 |
1476 | 153 CS∋x→Clx=x : {L x : HOD} → (top : Topology L) → CS top ∋ x → Cl top x =h= x |
154 CS∋x→Clx=x {L} {x} top cx = record { eq→ = cc10 ; eq← = cc11 } where | |
1210 | 155 cc10 : {y : Ordinal} → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) → odef x y |
1484 | 156 cc10 {y} ⟪ Ly , cc ⟫ = eq→ *iso ( cc (& x) cx (λ {z} xz → eq← *iso xz ) ) |
1210 | 157 cc11 : {y : Ordinal} → odef x y → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) |
158 cc11 {y} xy = ⟪ cs⊆L top cx xy , (λ c oc x⊆c → x⊆c xy ) ⟫ | |
1160 | 159 |
1119 | 160 -- Subbase P |
161 -- A set of countable intersection of P will be a base (x ix an element of the base) | |
1107 | 162 |
163 data Subbase (P : HOD) : Ordinal → Set n where | |
164 gi : {x : Ordinal } → odef P x → Subbase P x | |
165 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) | |
166 | |
1119 | 167 -- |
1150 | 168 -- if y is in a Subbase, some element of P contains it |
1119 | 169 |
1111 | 170 sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal |
171 sbp P {x} (gi {y} px) = x | |
172 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb | |
1107 | 173 |
1111 | 174 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y |
175 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ | |
1484 | 176 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (eq→ *iso xy)) |
1107 | 177 |
1155 | 178 sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x |
179 sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px) | |
180 sb⊆ {P} {Q} P⊆Q (g∩ px qx) = g∩ (sb⊆ P⊆Q px) (sb⊆ P⊆Q qx) | |
181 | |
1119 | 182 -- An open set generate from a base |
183 -- | |
1161 | 184 -- OS = { U ⊆ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊆ U } |
1114 | 185 |
1115 | 186 record Base (L P : HOD) (u x : Ordinal) : Set n where |
1114 | 187 field |
1150 | 188 b : Ordinal |
1161 | 189 u⊆L : * u ⊆ L |
1114 | 190 sb : Subbase P b |
191 b⊆u : * b ⊆ * u | |
192 bx : odef (* b) x | |
1150 | 193 x⊆L : odef L x |
1161 | 194 x⊆L = u⊆L (b⊆u bx) |
1114 | 195 |
1115 | 196 SO : (L P : HOD) → HOD |
1119 | 197 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where |
198 tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) | |
1150 | 199 tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) |
1114 | 200 |
1111 | 201 record IsSubBase (L P : HOD) : Set (suc n) where |
1110 | 202 field |
1122 | 203 P⊆PL : P ⊆ Power L |
1116 | 204 -- we may need these if OS ∋ L is necessary |
205 -- p : {x : HOD} → L ∋ x → HOD | |
1161 | 206 -- Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx |
1116 | 207 -- px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x |
1110 | 208 |
1152 | 209 InducedTopology : (L P : HOD) → IsSubBase L P → Topology L |
210 InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00 | |
1122 | 211 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where |
212 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x | |
1484 | 213 tp03 {x} 0x = ⊥-elim ( empty (* x) (eq→ *iso ( subst (λ k → odef (* (& od∅)) k ) (sym &iso) 0x ))) |
1115 | 214 tp00 : SO L P ⊆ Power L |
215 tp00 {u} ou x ux with ou ux | |
1161 | 216 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊆L (b⊆u bx) |
1115 | 217 tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) |
1484 | 218 tp01 {p} {q} op oq {x} ux = record { b = b ; u⊆L = λ lt → ul (eq→ *iso lt) |
1116 | 219 ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where |
1115 | 220 px : odef (* (& p)) x |
1484 | 221 px = eq← *iso ( proj1 (eq→ *iso ux) ) |
1115 | 222 qx : odef (* (& q)) x |
1484 | 223 qx = eq← *iso ( proj2 (eq→ *iso ux) ) |
1115 | 224 b : Ordinal |
225 b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) | |
1116 | 226 tp08 : * b ⊆ * (& (p ∩ q) ) |
1484 | 227 tp08 = λ lt → ( eq← *iso ((⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) (eq→ *iso lt))) where |
1116 | 228 tp11 : * (Base.b (op px)) ⊆ * (& p ) |
229 tp11 = Base.b⊆u (op px) | |
230 tp12 : * (Base.b (oq qx)) ⊆ * (& q ) | |
231 tp12 = Base.b⊆u (oq qx) | |
1150 | 232 tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p |
1484 | 233 tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (λ lt → eq→ *iso (tp11 lt)) |
1150 | 234 tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q |
1484 | 235 tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (λ lt → eq→ *iso (tp12 lt)) |
1116 | 236 tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x |
1484 | 237 tp14 = eq← *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
|
238 ul : (p ∩ q) ⊆ L |
1484 | 239 ul = λ pq → (Base.u⊆L (op px)) (pz (eq← *iso pq)) where |
1116 | 240 pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z |
1484 | 241 pz {z} pq = eq← *iso ( proj1 (eq→ *iso pq ) ) |
1161 | 242 tp02 : { q : HOD} → q ⊆ SO L P → SO L P ∋ Union q |
1484 | 243 tp02 {q} q⊆O {x} ux with eq→ *iso ux |
244 ... | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx | |
245 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊆L = λ lt → tp04 (eq→ *iso lt) | |
246 ; sb = sb ; b⊆u = λ lt → eq← *iso (tp06 lt) ; bx = bx } where | |
247 tp05 : Union q ⊆ L | |
248 tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx | |
249 ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } | |
250 = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) | |
251 tp04 : Union q ⊆ L | |
252 tp04 = tp05 | |
253 tp06 : * b ⊆ Union q | |
254 tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } | |
1110 | 255 |
1142 | 256 -- Product Topology |
257 | |
258 open ZFProduct | |
259 | |
1150 | 260 -- Product Topology is not |
1142 | 261 -- ZFP (OS TP) (OS TQ) (box) |
262 | |
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
263 -- Rectangle subset (zπ1 ⁻¹ p) |
1142 | 264 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where |
265 field | |
1172 | 266 p : Ordinal |
1142 | 267 op : odef (OS TP) p |
268 prod : x ≡ & (ZFP (* p) Q ) | |
269 | |
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
270 -- Rectangle subset (zπ12⁻¹ q ) |
1142 | 271 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where |
272 field | |
1172 | 273 q : Ordinal |
1142 | 274 oq : odef (OS TQ) q |
275 prod : x ≡ & (ZFP P (* q )) | |
276 | |
277 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 | |
1172 | 278 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where |
1142 | 279 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) |
1485 | 280 tp01 w wz with eq→ *iso wz |
281 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where | |
282 tp03 : odef P a | |
283 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa | |
1172 | 284 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where |
1142 | 285 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) |
1485 | 286 tp01 w wz with eq→ *iso wz |
287 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where | |
288 tp03 : odef Q b | |
289 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb | |
1142 | 290 |
291 pbase : {P Q : HOD} → Topology P → Topology Q → HOD | |
292 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 | |
293 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) | |
1150 | 294 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) |
1142 | 295 |
296 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) | |
1152 | 297 ProductTopology {P} {Q} TP TQ = InducedTopology (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } |
1142 | 298 |
1152 | 299 -- covers ( q ⊆ Union P ) |
1101 | 300 |
1120 | 301 record _covers_ ( P q : HOD ) : Set n where |
431 | 302 field |
1120 | 303 cover : {x : Ordinal } → odef q x → Ordinal |
1145 | 304 P∋cover : {x : Ordinal } → (lt : odef q x) → odef P (cover lt) |
305 isCover : {x : Ordinal } → (lt : odef q x) → odef (* (cover lt)) x | |
1120 | 306 |
307 open _covers_ | |
431 | 308 |
1485 | 309 cong-covers : (P Q R S : HOD) → P =h= Q → R =h= S → P covers R → Q covers S |
310 cong-covers P Q R S P=Q R=S record { cover = cover ; P∋cover = P∋cover ; isCover = isCover } | |
311 = record { cover = λ {x} px → cover (eq← R=S px) ; P∋cover = λ {x} px → eq→ P=Q (P∋cover (eq← R=S px)) | |
312 ; isCover = λ {x} px → isCover (eq← R=S px) } | |
313 | |
314 | |
431 | 315 -- Finite Intersection Property |
316 | |
1120 | 317 record FIP {L : HOD} (top : Topology L) : Set n where |
431 | 318 field |
1150 | 319 limit : {X : Ordinal } → * X ⊆ CS top |
1187 | 320 → ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → Ordinal |
1150 | 321 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
1187 | 322 → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) |
1143 | 323 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) |
1150 | 324 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
1187 | 325 → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) |
1150 | 326 → {x : Ordinal } → odef (* X) x |
1143 | 327 → odef L (limit CX fip) |
328 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 | 329 |
330 -- Compact | |
331 | |
1119 | 332 data Finite-∪ (S : HOD) : Ordinal → Set n where |
1188 | 333 fin-e : Finite-∪ S o∅ |
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
334 fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) -- an element of S |
1188 | 335 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) |
1198 | 336 -- Finite-∪ S y → Union y ⊆ S |
431 | 337 |
1120 | 338 record Compact {L : HOD} (top : Topology L) : Set n where |
431 | 339 field |
1120 | 340 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal |
341 isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L | |
1150 | 342 isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) |
431 | 343 |
344 -- FIP is Compact | |
345 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
346 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top |
1150 | 347 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
|
348 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1148 | 349 ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where |
350 -- L is empty | |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
351 fip02 : {x : Ordinal } → ¬ odef L x |
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
352 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) ) |
1148 | 353 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
|
354 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } |
1148 | 355 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅ |
1188 | 356 fip00 {X} xo xcp = fin-e |
1146
1966127fc14f
wrong cover definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1145
diff
changeset
|
357 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where |
1121 | 358 -- set of coset of X |
1484 | 359 open BAlgebra O HODAxiom ho< L (LDec L) |
1121 | 360 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal |
1293 | 361 CX {X} ox = & ( Replace (* X) (λ z → L \ z ) RC\ ) |
1150 | 362 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top |
1485 | 363 CCX {X} os {x} ox with eq→ *iso ox |
364 ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L \ * z) | |
365 fip07 : z ≡ & (L \ * x) | |
366 fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L \ k )) (cong (*) (sym x=ψz))) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } ) where | |
367 fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L \ * z))) x) → odef (* z) x | |
368 fip08 {x} ⟪ Lx , not ⟫ = double-neg-elim ( λ nz → not (eq← *iso ⟪ Lx , nz ⟫) ) -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ | |
369 fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L \ * z))) x) | |
370 fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , (λ lt → fip10 (eq→ *iso lt)) ⟫ where | |
371 fip10 : ¬ (odef (L \ * z) w) | |
372 fip10 ⟪ Lw , nzw ⟫ = nzw zw | |
373 fip06 : odef (OS top) (& (L \ * x)) | |
374 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) | |
375 fip05 : * x ⊆ L | |
376 fip05 {w} xw = proj1 ( eq→ (begin | |
377 * x ≈⟨ o≡→== x=ψz ⟩ | |
378 * (& ( L \ * z )) ≈⟨ *iso ⟩ | |
379 L \ * z ∎ ) xw ) where | |
380 open EqHOD ==-Setoid | |
1143 | 381 -- |
382 -- X covres L means Intersection of (CX X) contains nothing | |
1152 | 383 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) |
1143 | 384 -- it means there is a finite cover |
385 -- | |
1293 | 386 finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Subbase (Replace (* X) (λ z → L \ z) RC\ ) o∅ |
1476 | 387 finCoverBase {X} ox oc with p∨¬p (Subbase (Replace (* X) (λ z → L \ z) RC\ ) o∅) |
1189 | 388 ... | case1 sb = sb |
1199 | 389 ... | case2 ¬sb = ⊥-elim (¬¬cover fip25 fip20) where |
390 ¬¬cover : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) | |
391 ¬¬cover {z} Lz nc = nc ( P∋cover oc Lz ) (isCover oc _ ) | |
392 -- ¬sb → we have finite intersection | |
1187 | 393 fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x |
394 fip02 {x} sc with trio< x o∅ | |
1148 | 395 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
396 ... | tri> ¬a ¬b c = c | |
1485 | 397 ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (sb⊆ (eq→ *iso) (subst (λ k → Subbase (* (CX ox)) k ) b sc ))) |
1150 | 398 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) |
1476 | 399 fip26 : odef (* (CX ox)) (& (L \ * ( cover oc ( x∋minimal L (0<P→ne 0<L) ) ))) |
1485 | 400 fip26 = eq← *iso 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 | 401 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) |
402 fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26 | |
403 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) | |
404 fip20 {y} Xy yl = proj2 fip21 yl where | |
405 fip22 : odef (* (CX ox)) (& ( L \ * y )) | |
1485 | 406 fip22 = eq← *iso record { z = y ; az = Xy ; x=ψz = refl } |
1148 | 407 fip21 : odef (L \ * y) ( FIP.limit fip (CCX ox) fip02 ) |
1485 | 408 fip21 = eq→ *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) |
1199 | 409 -- create HOD from Subbase ( finite intersection ) |
1293 | 410 finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L \ z) RC\ ) x → HOD |
1190 | 411 finCoverSet {X} x (gi rx) = ( L \ * x ) , ( L \ * x ) |
1189 | 412 finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy |
1149 | 413 -- |
1121 | 414 -- this defines finite cover |
1120 | 415 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
1189 | 416 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) |
1199 | 417 -- create Finite-∪ from finCoverSet |
1120 | 418 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
1189 | 419 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where |
1293 | 420 fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L \ z) RC\ ) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) |
1190 | 421 fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where |
422 fip62 : & (* (& (L \ * x)) , * (& (L \ * x))) ≡ & ((L \ * x) , (L \ * x)) | |
1485 | 423 fip62 = ==→o≡ (pair-subst2 *iso *iso ) |
1293 | 424 fip61 : odef (Replace (* X) (_\_ L) RC\ ) x → odef (* X) ( & ((L \ * x ) )) |
1189 | 425 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
426 fip34 : * z1 ⊆ L |
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
427 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1 |
1189 | 428 fip33 : z1 ≡ & (L \ * x) |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
429 fip33 = begin |
1152 | 430 z1 ≡⟨ sym &iso ⟩ |
1485 | 431 & (* z1) ≡⟨ sym ( ==→o≡ (L\Lx=x {* z1} fip34)) ⟩ |
432 & (L \ ( L \ * z1)) ≡⟨ ==→o≡ ( \-cong L L ( L \ * z1) (* (& ( L \ * z1))) ==-refl (==-sym *iso) ) ⟩ | |
1152 | 433 & (L \ * (& ( L \ * z1))) ≡⟨ cong (λ k → & ( L \ * k )) (sym x=ψz1) ⟩ |
1189 | 434 & (L \ * x ) ∎ where open ≡-Reasoning |
435 fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx) (fip60 y sy) ) where | |
436 fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy) | |
1485 | 437 fip62 = ==→o≡ (begin |
438 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) | |
439 ≈⟨ ∪-cong {* (& (finCoverSet x sx))} {finCoverSet x sx} {* (& (finCoverSet y sy))} {finCoverSet y sy} *iso *iso ⟩ | |
440 finCoverSet x sx ∪ finCoverSet y sy ∎ ) | |
441 where open EqHOD ==-Setoid | |
1120 | 442 -- is also a cover |
443 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | |
1485 | 444 isCover1 {X} xo xcp = cong-covers _ _ _ _ (==-sym *iso) (==-trans (\-cong L L (* o∅) od∅ ==-refl o∅==od∅) L\0=L) |
445 -- subst₂ (λ j k → j covers k ) ? (subst (λ k → L \ k ≡ L) ? ? ) -- L\0=L) | |
1190 | 446 (fip70 o∅ (finCoverBase xo xcp)) where |
1293 | 447 fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L \ z) RC\ ) x ) → (finCoverSet {X} x sb) covers (L \ * x) |
1199 | 448 fip70 x (gi rx) = fip73 where |
449 fip73 : ((L \ * x) , (L \ * x)) covers (L \ * x) -- obvious | |
450 fip73 = record { cover = λ _ → & (L \ * x) ; P∋cover = λ _ → case1 refl | |
1485 | 451 ; isCover = λ {x} lt → eq← *iso lt } |
452 fip70 x∩y (g∩ {x} {y} sx sy) = cong-covers _ _ _ _ ==-refl (\-cong L L (* x ∩ * y) (* (& (* x ∩ * y))) ==-refl (==-sym *iso)) | |
453 ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where | |
1194 | 454 fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c |
455 fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) | |
456 ; isCover = isCover cov } | |
457 fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c | |
458 fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) | |
459 ; isCover = isCover cov } | |
1190 | 460 fip45 : {L a b : HOD} → (L \ (a ∩ b)) ⊆ ( (L \ a) ∪ (L \ b)) |
1476 | 461 fip45 {L} {a} {b} {x} Lab with ∋-p b (* x) |
1190 | 462 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ |
463 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ | |
464 fip43 : {A L a b : HOD } → A covers (L \ a) → A covers (L \ b ) → A covers ( L \ ( a ∩ b ) ) | |
465 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where | |
466 fip44 : {x : Ordinal} → odef (L \ (a ∩ b)) x → Ordinal | |
467 fip44 {x} Lab with fip45 {L} {a} {b} Lab | |
468 ... | case1 La = cover ca La | |
469 ... | case2 Lb = cover cb Lb | |
470 fip46 : {x : Ordinal} (lt : odef (L \ (a ∩ b)) x) → odef A (fip44 lt) | |
471 fip46 {x} Lab with fip45 {L} {a} {b} Lab | |
472 ... | case1 La = P∋cover ca La | |
473 ... | case2 Lb = P∋cover cb Lb | |
474 fip47 : {x : Ordinal} (lt : odef (L \ (a ∩ b)) x) → odef (* (fip44 lt)) x | |
475 fip47 {x} Lab with fip45 {L} {a} {b} Lab | |
476 ... | case1 La = isCover ca La | |
477 ... | case2 Lb = isCover cb Lb | |
1151
8a071bf52407
Finite intersection property to Compact done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1150
diff
changeset
|
478 |
1485 | 479 |
480 | |
1158 | 481 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top |
1180 | 482 Compact→FIP {L} top compact with trio< (& L) o∅ |
1175 | 483 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
1198 | 484 ... | tri≈ ¬a L=0 ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX fip xx) } where |
485 -- empty L case | |
486 -- if 0 < X then 0 < x ∧ L ∋ xfrom fip | |
487 -- if 0 ≡ X then ¬ odef X x | |
488 fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ({y : Ordinal} → Subbase (* X) y → o∅ o< y) → ¬ odef (* X) x | |
489 fip000 {X} {x} CX fip xx with trio< o∅ X | |
1485 | 490 ... | tri< 0<X ¬b ¬c = ¬∅∋ (eq→ (begin |
491 L ≈⟨ ==-sym *iso ⟩ | |
492 * (& L) ≈⟨ o≡→== L=0 ⟩ | |
493 * o∅ ≈⟨ o∅==od∅ ⟩ | |
494 od∅ ∎ ) (subst (λ k → odef L k ) (sym &iso) | |
495 ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) Xe ))) where | |
496 open EqHOD ==-Setoid | |
1198 | 497 0<x : o∅ o< x |
498 0<x = fip (gi xx ) | |
499 e : HOD -- we have an element of x | |
1476 | 500 e = minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) |
1198 | 501 Xe : odef (* x) (& e) |
1476 | 502 Xe = x∋minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) |
1485 | 503 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (eq→ ( begin |
504 * X ≈⟨ o≡→== (sym 0=X) ⟩ | |
505 * o∅ ≈⟨ o∅==od∅ ⟩ | |
506 od∅ ∎ ) (subst (λ k → odef (* X) k ) (sym &iso) xx ) )) where open EqHOD ==-Setoid | |
1198 | 507 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
1175 | 508 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where |
509 -- set of coset of X | |
1484 | 510 open BAlgebra O HODAxiom ho< L (LDec L) |
1175 | 511 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal |
1293 | 512 OX {X} ox = & ( Replace (* X) (λ z → L \ z ) RC\) |
1175 | 513 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top |
1485 | 514 OOX {X} cs {x} ox with eq→ *iso ox |
515 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P\CS=OS top (cs comp01)) where | |
516 comp01 : odef (* X) (& (* z)) | |
517 comp01 = subst (λ k → odef (* X) k) (sym &iso) az | |
518 -- if all finite intersection of X contains something, | |
519 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) | |
520 -- it means there is a limit | |
1199 | 521 record NC {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) (0<X : o∅ o< X) : Set n where |
522 field -- find an element x, which is not covered (which is a limit point) | |
523 x : Ordinal | |
524 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x | |
1187 | 525 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) |
1199 | 526 → (0<X : o∅ o< X ) → NC CX fip 0<X |
527 has-intersection {X} CX fip 0<X = intersection where | |
1198 | 528 e : HOD -- we have an element of X |
1476 | 529 e = minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) |
1198 | 530 Xe : odef (* X) (& e) |
1476 | 531 Xe = x∋minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) |
1183 | 532 no-cover : ¬ ( (* (OX CX)) covers L ) |
1198 | 533 no-cover cov = ⊥-elim (no-finite-cover (Compact.isCover compact (OOX CX) cov)) where |
534 -- construct Subase from Finite-∪ | |
1180 | 535 fp01 : Ordinal |
536 fp01 = Compact.finCover compact (OOX CX) cov | |
1194 | 537 record SB (t : Ordinal) : Set n where |
538 field | |
539 i : Ordinal | |
540 sb : Subbase (* X) (& (L \ * i)) | |
1198 | 541 t⊆i : (L \ * i) ⊆ (L \ Union ( * t ) ) |
1194 | 542 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t |
1198 | 543 fp02 t fin-e = record { i = & ( L \ e) ; sb = gi (subst (λ k → odef (* X) k) fp21 Xe) ; t⊆i = fp23 } where |
544 -- t ≡ o∅, no cover. Any subst of L is ok and we have e ⊆ L | |
545 fp22 : e ⊆ L | |
546 fp22 {x} lt = cs⊆L top (CX Xe) lt | |
547 fp21 : & e ≡ & (L \ * (& (L \ e))) | |
1485 | 548 fp21 = ==→o≡ ( ==-trans (==-sym (L\Lx=x {e} fp22 )) (\-cong L L (L \ e) (* (& (L \ e))) ==-refl (==-sym *iso ))) |
1198 | 549 fp23 : (L \ * (& (L \ e))) ⊆ (L \ Union (* o∅)) |
1485 | 550 fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (eq→ (begin |
551 (* o∅) ≈⟨ o∅==od∅ ⟩ | |
552 od∅ ∎ ) (subst (λ k → odef (* o∅) k ) (sym &iso) (Own.ao lt ))))) ⟫ | |
553 where open EqHOD ==-Setoid | |
1198 | 554 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; t⊆i = fp24 } where |
555 -- we have a single cover x, L \ * x is single finite intersection | |
1197 | 556 fp24 : (L \ * x) ⊆ (L \ Union (* (& (* x , * x)))) |
1485 | 557 fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , fp26 ⟫ where |
558 fp26 : ¬ odef (Union (* (& (* x , * x)))) y | |
559 fp26 record { owner = owner ; ao = ao ; ox = ox } with eq→ *iso ao | |
560 ... | case1 refl = not (eq→ *iso ox ) | |
561 ... | case2 refl = not (eq→ *iso ox ) | |
1198 | 562 fp03 : odef (* X) (& (L \ * x)) -- becase x is an element of Replace (* X) (λ z → L \ z ) |
1485 | 563 fp03 with eq→ *iso tx |
564 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where | |
565 fip34 : * z1 ⊆ L | |
566 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 | |
567 fip33 : z1 ≡ & (L \ * x) | |
568 fip33 = trans (sym &iso ) (==→o≡ ( begin | |
569 (* z1) ≈⟨ ==-sym (L\Lx=x {* z1} fip34 ) ⟩ | |
570 (L \ ( L \ * z1)) ≈⟨ \-cong L L ( L \ * z1) (* x) ==-refl (==-trans (==-sym *iso) (o≡→== (sym x=ψz1)) ) ⟩ | |
571 (L \ * x ) ∎ ) ) where open EqHOD ==-Setoid | |
1198 | 572 fp02 t (fin-∪ {tx} {ty} ux uy ) = record { i = & (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ; sb = fp11 ; t⊆i = fp35 } where |
573 fp35 : (L \ * (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) ⊆ (L \ Union (* (& (* tx ∪ * ty)))) | |
1485 | 574 fp35 = λ lt → eq← fp42 ( fp36 (eq→ ( \-cong L L (* (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) |
575 (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ==-refl *iso ) lt ) ) where | |
576 fp43 : (P : HOD ) → Union (* (& P)) =h= Union P | |
577 eq← (fp43 P) record { owner = owner ; ao = ao ; ox = ox } = record { owner = owner ; ao = eq← *iso ao ; ox = ox } | |
578 eq→ (fp43 P) record { owner = owner ; ao = ao ; ox = ox } = record { owner = owner ; ao = eq→ *iso ao ; ox = ox } | |
579 fp42 : ( L \ Union (* (& (* tx ∪ * ty)))) =h= (L \ Union (* tx ∪ * ty)) | |
580 eq→ fp42 {x} ⟪ lx , nux ⟫ = ⟪ lx , (λ lt → nux (eq← (fp43 _) lt) ) ⟫ | |
581 eq← fp42 {x} ⟪ lx , nux ⟫ = ⟪ lx , (λ lt → nux (eq→ (fp43 _) lt) ) ⟫ | |
1197 | 582 fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z |
1199 | 583 fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } |
1485 | 584 = ⊥-elim ( ¬∅∋ (eq→ o∅==od∅ (subst (λ k → odef (* o∅) k ) (sym &iso) ao ))) |
585 fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (eq→ (fp43 _) uz) where | |
1197 | 586 fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z |
587 fp41 x record { owner = .(& (* w)) ; ao = (case1 refl) ; ox = ox } = | |
1485 | 588 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (eq→ *iso ox ) |
1197 | 589 fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } = |
1485 | 590 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (eq→ *iso ox ) |
591 fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with eq→ (fp43 _ ) uz | |
592 ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } | |
593 ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } | |
1198 | 594 fp36 : (L \ (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))) ⊆ (L \ Union (* tx ∪ * ty)) |
1197 | 595 fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where |
596 fp37 : ¬ odef (Union (* tx ∪ * ty)) z | |
597 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where | |
1198 | 598 fp38 : (L \ (* (SB.i (fp02 tx ux)))) ⊆ (L \ Union (* tx)) |
599 fp38 = SB.t⊆i (fp02 tx ux) | |
600 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux))) | |
1485 | 601 fp39 {w} txw with ∨L\X {L} {(SB.i (fp02 tx ux))} (fp40 ux ?) |
602 ... | t = ? | |
1476 | 603 -- ... | case1 sb = sb |
604 -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) | |
1197 | 605 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where |
1198 | 606 fp38 : (L \ (* (SB.i (fp02 ty uy)))) ⊆ (L \ Union (* ty)) |
607 fp38 = SB.t⊆i (fp02 ty uy) | |
608 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy))) | |
1476 | 609 fp39 {w} tyw = ? -- with ∨L\X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw) |
610 -- ... | case1 sb = sb | |
611 -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) | |
1194 | 612 fp04 : {tx ty : Ordinal} → & (* (& (L \ * tx)) ∩ * (& (L \ * ty))) ≡ & (L \ * (& (* tx ∪ * ty))) |
1485 | 613 fp04 {tx} {ty} = ==→o≡ record { eq→ = fp05 ; eq← = fp09 } where |
1187 | 614 fp05 : {x : Ordinal} → odef (* (& (L \ * tx)) ∩ * (& (L \ * ty))) x → odef (L \ * (& (* tx ∪ * ty))) x |
1485 | 615 fp05 {x} lt with eq← *iso∩ lt |
616 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = eq→ (\-cong L L (* tx ∪ * ty) (* (& (* tx ∪ * ty))) ==-refl (==-sym *iso) ) ⟪ Lx , fp06 ⟫ where | |
617 fp06 : ¬ odef (* tx ∪ * ty) x | |
618 fp06 (case1 tx) = ¬tx tx | |
619 fp06 (case2 ty) = ¬ty ty | |
1187 | 620 fp09 : {x : Ordinal} → odef (L \ * (& (* tx ∪ * ty))) x → odef (* (& (L \ * tx)) ∩ * (& (L \ * ty))) x |
1485 | 621 fp09 {x} lt with eq→ (\-cong L L (* (& (* tx ∪ * ty))) (* tx ∪ * ty) ==-refl *iso ) lt |
622 ... | ⟪ Lx , ¬tx∨ty ⟫ = eq→ *iso∩ | |
1187 | 623 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ |
1198 | 624 fp11 : Subbase (* X) (& (L \ * (& ((* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))))) |
625 fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx ux)) (SB.sb (fp02 ty uy )) ) | |
626 -- | |
627 -- becase of fip, finite cover cannot be a cover | |
628 -- | |
1195 | 629 fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov) |
630 fcov = Compact.isFinite compact (OOX CX) cov | |
1196 | 631 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L \ * i))) → o∅ o< & (L \ * i) |
632 0<sb {i} sb = fip sb | |
633 sb : SB (Compact.finCover compact (OOX CX) cov) | |
634 sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) | |
1198 | 635 no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) |
1476 | 636 no-finite-cover fcovers = ? where -- ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where |
1196 | 637 f23 : (L \ * (SB.i sb)) ⊆ ( L \ Union (* (Compact.finCover compact (OOX CX) cov))) |
1198 | 638 f23 = SB.t⊆i sb |
1196 | 639 f22 : (L \ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ |
640 f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where | |
641 f24 : {x : Ordinal } → ¬ ( odef (L \ Union (* (Compact.finCover compact (OOX CX) cov))) x ) | |
642 f24 {x} ⟪ Lx , not ⟫ = not record { owner = cover fcovers Lx ; ao = P∋cover fcovers Lx ; ox = isCover fcovers Lx } | |
643 f25 : & od∅ o< (& (L \ Union (* (Compact.finCover compact (OOX CX) cov))) ) | |
644 f25 = ordtrans<-≤ (subst (λ k → k o< & (L \ * (SB.i sb))) (sym ord-od∅) (0<sb (SB.sb sb) ) ) ( begin | |
645 & (L \ * (SB.i sb)) ≤⟨ ⊆→o≤ f23 ⟩ | |
646 & (L \ Union (* (Compact.finCover compact (OOX CX) cov))) ∎ ) where open o≤-Reasoning O | |
1199 | 647 -- if we have no cover, we can consruct NC |
648 intersection : NC CX fip 0<X | |
1476 | 649 intersection with p∨¬p (NC CX fip 0<X) |
1184 | 650 ... | case1 nc = nc |
1185 | 651 ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → & (L \ coverf Lx) ; P∋cover = fp22 ; isCover = fp23 } ) where |
652 coverSet : {x : Ordinal} → odef L x → HOD | |
1186 | 653 coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L \ * y) x } ; odmax = X |
654 ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) } | |
1185 | 655 fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ ) |
1187 | 656 fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where |
1185 | 657 fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x |
1476 | 658 fp19 {y} Xy = ? -- with ∨L\X {L} {* y} {x} Lx |
659 -- ... | case1 yx = yx | |
660 -- ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where | |
661 -- fp20 : odef (* X) y ∧ odef (L \ * y) x | |
662 -- fp20 = ⟪ Xy , lyx ⟫ | |
1185 | 663 coverf : {x : Ordinal} → (Lx : odef L x ) → HOD |
1476 | 664 coverf Lx = minimal (coverSet Lx) (fp17 Lx) |
1186 | 665 fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L \ coverf lt)) |
1476 | 666 fp22 {x} Lx = subst (λ k → odef k (& (L \ coverf Lx ))) ? record { z = _ ; az = fp25 ; x=ψz = fp24 } where |
1186 | 667 fp24 : & (L \ coverf Lx) ≡ & (L \ * (& (coverf Lx))) |
1476 | 668 fp24 = cong (λ k → & ( L \ k )) ? |
1185 | 669 fp25 : odef (* X) (& (coverf Lx)) |
1476 | 670 fp25 = proj1 ( x∋minimal (coverSet Lx) (fp17 Lx) ) |
1186 | 671 fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (L \ coverf lt))) x |
1476 | 672 fp23 {x} Lx = subst (λ k → odef k x) ? ⟪ Lx , fp26 ⟫ where |
1186 | 673 fp26 : ¬ odef (coverf Lx) x |
1476 | 674 fp26 = subst (λ k → ¬ odef k x ) ? (proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) )) ) |
1199 | 675 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal |
1180 | 676 limit {X} CX fip with trio< X o∅ |
677 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
678 ... | tri≈ ¬a b ¬c = o∅ | |
1199 | 679 ... | tri> ¬a ¬b c = NC.x ( has-intersection CX fip c) |
1175 | 680 fip00 : {X : Ordinal} (CX : * X ⊆ CS top) |
1187 | 681 (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) |
1175 | 682 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) |
1180 | 683 fip00 {X} CX fip {x} Xx with trio< X o∅ |
684 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
685 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) ) | |
1199 | 686 ... | tri> ¬a ¬b c = NC.yx ( has-intersection CX fip c ) Xx |
431 | 687 |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
688 open Filter |
1102 | 689 |
1228
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
690 -- |
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
691 -- {v | Neighbor lim v} set of u ⊆ v ⊆ P where u is an open set u ∋ x |
e3f20bc4fac9
last part of Tychonoff
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1218
diff
changeset
|
692 -- |
1159 | 693 record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where |
694 field | |
695 u : Ordinal | |
696 ou : odef (OS TP) u | |
697 ux : odef (* u) x | |
698 v⊆P : * v ⊆ P | |
1170 | 699 u⊆v : * u ⊆ * v |
1102 | 700 |
1169 | 701 -- |
702 -- Neighbor on x is a Filter (on Power P) | |
703 -- | |
1170 | 704 NeighborF : {P : HOD} (TP : Topology P) (x : Ordinal ) → Filter {Power P} {P} (λ x → x) |
1169 | 705 NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = f2 } where |
1168 | 706 nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v |
707 nf00 {v} nei y vy = Neighbor.v⊆P nei vy | |
1167 | 708 NF : HOD |
1168 | 709 NF = record { od = record { def = λ v → Neighbor TP x v } ; odmax = & (Power P) ; <odmax = λ lt → odef< (nf00 lt) } |
1167 | 710 NF⊆PP : NF ⊆ Power P |
1168 | 711 NF⊆PP = nf00 |
712 f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q | |
1170 | 713 f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where |
1168 | 714 f11 : * (Neighbor.u Np) ⊆ * (& q) |
1476 | 715 f11 {x} ux = subst (λ k → odef k x ) ? ( p⊆q (subst (λ k → odef k x) ? (Neighbor.u⊆v Np ux)) ) |
1168 | 716 f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q) |
1170 | 717 f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where |
1168 | 718 upq : Ordinal |
719 upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) ) | |
720 ou : odef (OS TP) upq | |
721 ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq)) | |
722 ux : odef (* upq) x | |
1476 | 723 ux = subst ( λ k → odef k x ) ? ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ |
1168 | 724 f20 : * upq ⊆ * (& (p ∩ q)) |
1476 | 725 f20 = subst₂ (λ j k → j ⊆ k ) ? ? ( λ {x} pq |
726 → ⟪ subst (λ k → odef k x) ? (Neighbor.u⊆v Np (proj1 pq)) , subst (λ k → odef k x) ? (Neighbor.u⊆v Nq (proj2 pq)) ⟫ ) | |
1153 | 727 |
1165 | 728 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q) |
1476 | 729 CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) ? pqx |
1484 | 730 ... | t = ? |
731 -- ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) ? px ) | |
1165 | 732 |
1170 | 733 NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P \ p ) |
1476 | 734 NEG P {p} Pp x vx with subst (λ k → odef k x) ? vx |
1484 | 735 ... | t = ? |
736 -- ... | ⟪ Px , npx ⟫ = Px | |
1142 | 737 |
1484 | 738 |
739 |