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

comparison src/Topology.agda @ 1148:d39c79bb71f0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovered
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 Jan 2023 14:01:45 +0900
parents 1966127fc14f
children f8a30e568eca
comparison
equal deleted inserted replaced
1146:1966127fc14f 1148:d39c79bb71f0
227 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) 227 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
228 228
229 -- Compact 229 -- Compact
230 230
231 data Finite-∪ (S : HOD) : Ordinal → Set n where 231 data Finite-∪ (S : HOD) : Ordinal → Set n where
232 fin-e : {x : Ordinal } → odef S x → Finite-∪ S x 232 fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
233 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) 233 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
234 234
235 record Compact {L : HOD} (top : Topology L) : Set n where 235 record Compact {L : HOD} (top : Topology L) : Set n where
236 field 236 field
237 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal 237 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
241 -- FIP is Compact 241 -- FIP is Compact
242 242
243 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top 243 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top
244 FIP→Compact {L} top fip with trio< (& L) o∅ 244 FIP→Compact {L} top fip with trio< (& L) o∅
245 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 245 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
246 ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → & ( od∅ , od∅ ) ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where 246 ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where
247 -- L is empty
247 fip02 : {x : Ordinal } → ¬ odef L x 248 fip02 : {x : Ordinal } → ¬ odef L x
248 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) ) 249 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) )
249 fip01 : {X : Ordinal } → (xcp : * X covers L) → * (& ( od∅ , od∅ )) covers L 250 fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L
250 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } 251 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) }
251 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (& ( od∅ , od∅ )) 252 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅
252 fip00 {X} xo xcp = fin-e ? 253 fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) )
253 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where 254 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
254 -- set of coset of X 255 -- set of coset of X
255 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal 256 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
256 CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼ z )) 257 CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼ z ))
257 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top 258 CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top
268 fip10 ⟪ Lw , nzw ⟫ = nzw zw 269 fip10 ⟪ Lw , nzw ⟫ = nzw zw
269 fip06 : odef (OS top) (& (L ＼ * x)) 270 fip06 : odef (OS top) (& (L ＼ * x))
270 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) 271 fip06 = os ( subst (λ k → odef (* X) k ) fip07 az )
271 fip05 : * x ⊆ L 272 fip05 : * x ⊆ L
272 fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw ) 273 fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw )
273 -- CX has finite intersection
274 CXfip : {X : Ordinal } → * X ⊆ OS top → Set n
275 CXfip {X} ox = { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
276 -- 274 --
277 -- X covres L means Intersection of (CX X) contains nothing 275 -- X covres L means Intersection of (CX X) contains nothing
278 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP ) 276 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP )
279 -- it means there is a finite cover 277 -- it means there is a finite cover
280 -- 278 --
281 record CFIP (x : Ordinal) : Set n where 279 record CFIP (x : Ordinal) : Set n where
282 field 280 field
283 is-CS : * x ⊆ CS top 281 is-CS : * x ⊆ CS top
284 y : Ordinal 282 sx : Subbase (* x) o∅
285 sy : Subbase (* y) o∅
286 Cex : HOD 283 Cex : HOD
287 Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → 284 Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt →
288 subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) } 285 subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) }
286 fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex =h= od∅ )
287 fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
288 -- CX is finite intersection
289 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
290 fip02 {C} {x} C<CX sc with trio< x o∅
291 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
292 ... | tri> ¬a ¬b c = c
293 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* C) k) b sc } )) where
294 fip10 : * C ⊆ CS top
295 fip10 {w} cw = CCX ox ( C<CX cw )
296 -- we have some intersection because L is not empty
297 fip26 : odef (* (CX ox)) (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )))
298 fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso)
299 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 }
300 fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
301 fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26
302 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
303 fip20 {y} Xy yl = proj2 fip21 yl where
304 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
305 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
306 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
307 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
308 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z ))
309 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
289 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal 310 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
290 cex {X} ox oc = & ( ODC.minimal O Cex fip00) where 311 cex {X} ox oc = & ( ODC.minimal O Cex (fip00 ox oc))
291 fip00 : ¬ ( Cex =h= od∅ ) 312 CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP (cex ox oc)
292 fip00 cex=0 = ⊥-elim (fip09 fip25 fip20) where 313 CXfip {X} ox oc = ODC.x∋minimal O Cex (fip00 ox oc)
293 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥
294 fip03 {x} {z} xz nxz = nxz xz
295 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
296 fip02 {C} {x} C<CX sc with trio< x o∅
297 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
298 ... | tri> ¬a ¬b c = c
299 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where
300 fip10 : * C ⊆ CS top
301 fip10 {w} cw = CCX ox ( C<CX cw )
302 fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
303 fip25 = FIP.L∋limit fip (CCX ox) fip02 ?
304 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
305 fip20 {y} Xy yl = proj2 fip21 yl where
306 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
307 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
308 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
309 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
310 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z ))
311 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
312 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅
313 ¬CXfip {X} ox oc = {!!} where
314 fip04 : odef Cex (cex ox oc)
315 fip04 = {!!}
316 -- this defines finite cover 314 -- this defines finite cover
317 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal 315 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
318 finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼ z )) 316 finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼ z ))
319 -- create Finite-∪ from cex 317 -- create Finite-∪ from cex
320 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) 318 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
321 isFinite = {!!} 319 isFinite {X} xo xcp = {!!} where
320 fip30 : {y z : Ordinal } → Subbase (* y) o∅ → Finite-∪ (* X) z
321 fip30 = ?
322 -- is also a cover 322 -- is also a cover
323 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L 323 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
324 isCover1 = {!!} 324 isCover1 = {!!}
325 325
326 326