Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/Topology.agda @ 1102:a9a7ad7784cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix topology
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Dec 2022 10:54:03 +0900
parents 7ce2cc622c92
children 81b859b678a8
comparison
equal deleted inserted replaced
1101:7ce2cc622c92 1102:a9a7ad7784cc
28 open ODUtil O 28 open ODUtil O
29 29
30 import ODC 30 import ODC
31 open ODC O 31 open ODC O
32 32
33 open import filter 33 open import filter O
34 open import OPair O 34 open import OPair O
35 35
36 36
37 record Topology ( L : HOD ) : Set (suc n) where 37 record Topology ( L : HOD ) : Set (suc n) where
38 field 38 field
76 76
77 data Finite-∩ (S : HOD) : HOD → Set (suc n) where 77 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
78 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x 78 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
79 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y) 79 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
80 80
81 record FIP {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where 81 record FIP {L : HOD} (top : Topology L) : Set (suc n) where
82 field 82 field
83 fipS⊆PL : P ⊆ CS top 83 fipS⊆PL : L ⊆ CS top
84 fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ ) 84 fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )
85 85
86 -- Compact 86 -- Compact
87 87
88 data Finite-∪ (S : HOD) : HOD → Set (suc n) where 88 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
89 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x 89 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
90 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y) 90 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
91 91
92 record Compact {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where 92 record Compact {L : HOD} (top : Topology L) : Set (suc n) where
93 field 93 field
94 finCover : {X : HOD} → X ⊆ OS top → X covers P → HOD 94 finCover : {X : HOD} → X ⊆ OS top → X covers L → HOD
95 isFinCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → (finCover xo xcp ) covers P 95 isCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
96 isFiniteCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → Finite-∪ X (finCover xo xcp ) 96 isFinite : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp )
97 97
98 -- FIP is Compact 98 -- FIP is Compact
99 99
100 FIP→Compact : {L P : HOD} → (top : Topology L ) → FIP top P → Compact top P 100 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top
101 FIP→Compact {L} {P} TL fip = record { finCover = ? ; isFinCover = ? ; isFiniteCover = ? } 101 FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }
102 102
103 Compact→FIP : {L P : HOD} → (top : Topology L ) → Compact top P → FIP top P 103 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
104 Compact→FIP = {!!} 104 Compact→FIP = {!!}
105 105
106 -- Product Topology 106 -- Product Topology
107 107
108 open ZFProduct 108 open ZFProduct
109
110 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
111 field
112 p : Ordinal
113 q : Ordinal
114 op : odef (OS TP) p
115 qq : odef Q q
116 prod : x ≡ & < * p , * q >
117
118 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
119 field
120 p : Ordinal
121 q : Ordinal
122 oq : odef (OS TQ) q
123 pp : odef P p
124 prod : x ≡ & < * p , * q >
109 125
110 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) 126 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
111 _Top⊗_ {P} {Q} TP TQ = record { 127 _Top⊗_ {P} {Q} TP TQ = record {
112 OS = POS 128 OS = POS
113 ; OS⊆PL = ? 129 ; OS⊆PL = ?
114 ; o∪ = ? 130 ; o∪ = ?
115 ; o∩ = ? 131 ; o∩ = ?
116 } where 132 } where
117 box : HOD 133 box : HOD
118 box = ZFP (OS TP) (OS TQ) 134 box = ZFP (OS TP) (OS TQ)
119 POS : HOD 135 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y )
120 POS = ? 136 -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U )
137 base : HOD
138 base = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
139 POS : HOD
140 POS = record { od = record { def = λ x → {b : Ordinal } → odef (Power base) b ∧ odef (Union (* b)) x }
141 ; odmax = & (ZFP P Q) ; <odmax = ? }
121 142
122 -- existence of Ultra Filter 143 -- existence of Ultra Filter
123 144
145 open Filter
146
124 -- Ultra Filter has limit point 147 -- Ultra Filter has limit point
148
149 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
150 field
151 limit : Ordinal
152 P∋limit : odef P limit
153 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
125 154
126 -- FIP is UFL 155 -- FIP is UFL
127 156
157 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
158 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf
159 FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
160
161 UFLP→FIP : {P : HOD} (TP : Topology P) →
162 ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP
163 UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? }
164
128 -- Product of UFL has limit point (Tychonoff) 165 -- Product of UFL has limit point (Tychonoff)
129 166
167 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (TP Top⊗ TQ)
168 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
169 uflp : {L : HOD} (LP : L ⊆ Power (ZFP P Q)) (F : Filter LP)
170 (uf : ultra-filter {L} {_} {LP} F) → UFLP (TP Top⊗ TQ) LP F uf
171 uflp {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
172
173
174
175
176
177