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

comparison src/Topology.agda @ 1155:c4fd0bfdfbae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIP to Filter done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 19 Jan 2023 11:13:40 +0900
parents 0612874b815c
children 6216562a2bce
comparison
equal deleted inserted replaced
1154:0612874b815c 1155:c4fd0bfdfbae
85 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb 85 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb
86 86
87 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y 87 is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y
88 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ 88 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫
89 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) 89 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy))
90
91 sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x
92 sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px)
93 sb⊆ {P} {Q} P⊆Q (g∩ px qx) = g∩ (sb⊆ P⊆Q px) (sb⊆ P⊆Q qx)
90 94
91 -- An open set generate from a base 95 -- An open set generate from a base
92 -- 96 --
93 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U } 97 -- OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P → x ∈ b ⊂ U }
94 98
406 open Filter 410 open Filter
407 411
408 -- Ultra Filter has limit point 412 -- Ultra Filter has limit point
409 413
410 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) 414 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP )
411 (FL : filter F ∋ P) (ultra : ultra-filter F ) : Set (suc (suc n)) where 415 (ultra : ultra-filter F ) : Set (suc (suc n)) where
412 field 416 field
413 limit : Ordinal 417 limit : Ordinal
414 P∋limit : odef P limit 418 P∋limit : odef P limit
415 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F 419 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
416 420
417 -- FIP is UFL 421 -- FIP is UFL
418 422
419 record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where 423 record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where
420 field 424 field
421 b x : Ordinal 425 b x : Ordinal
426 b⊆X : * b ⊆ * X
427 sb : Subbase (* b) x
422 0<x : o∅ o< x 428 0<x : o∅ o< x
423 b⊆X : * b ⊆ * X 429 X∋u : odef (* X) u
424 u⊆X : * u ⊆ * X
425 x⊆u : * x ⊆ * u 430 x⊆u : * x ⊆ * u
426 sb : Subbase (* b) x 431
432 open import maximum-filter O
427 433
428 UFLP→FIP : {P : HOD} (TP : Topology P) → 434 UFLP→FIP : {P : HOD} (TP : Topology P) →
429 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP 435 ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP
430 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where 436 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
431 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 437 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
432 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x 438 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
433 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD 439 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
434 N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = ? ; <odmax = ? } 440 N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = X
441 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< k) refl &iso (odef< (NFIP.X∋u lt)) }
435 N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X 442 N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X
436 N⊆PX {X} CSX fp {z} nz = ? 443 N⊆PX {X} CSX fp {z} nz = NFIP.X∋u nz
437 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (λ lt → CS⊆PL TP (CSX lt)) 444 X⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → * X ⊆ Power P
438 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = ? ; filter2 = ? } where 445 X⊆PP CSX lt = CS⊆PL TP (CSX lt)
446 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (X⊆PP CSX)
447 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = f1 ; filter2 = f2 } where
439 f1 : {p q : HOD} → * X ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q 448 f1 : {p q : HOD} → * X ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
440 f1 {p} {q} Lq Np p⊆q = ? 449 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; 0<x = 0<x ; X∋u = Xp ; x⊆u = x⊆p } p⊆q =
450 record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; 0<x = 0<x ; X∋u = Xq ; x⊆u = λ {z} xp →
451 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) }
452 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → * X ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
453 f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; 0<x = f21 ; X∋u = Xpq ; x⊆u = f22 } where
454 Np+Nq = * (NFIP.b Np) ∪ * (NFIP.b Nq)
455 xp∧xq = * (NFIP.x Np) ∩ * (NFIP.x Nq)
456 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
457 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (NFIP.sb Np)) (sb⊆ case2 (NFIP.sb Nq)))
458 f20 : * (& Np+Nq) ⊆ * X
459 f20 {x} npq with subst (λ k → odef k x) *iso npq
460 ... | case1 np = NFIP.b⊆X Np np
461 ... | case2 nq = NFIP.b⊆X Nq nq
462 f21 : o∅ o< & xp∧xq
463 f21 = fp f20 sbpq
464 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
465 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
466 → ⟪ subst (λ k → odef k w) *iso ( NFIP.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( NFIP.x⊆u Nq (proj2 xpq)) ⟫ )
467 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
468 proper = ?
469 CAP : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → {p q : HOD } → * X ∋ p → * X ∋ q → * X ∋ (p ∩ q)
470 CAP = ?
471 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (X⊆PP CSX) (F CSX fp)
472 maxf {X} CSX fp = F→Maximum (X⊆PP CSX) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)
441 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal 473 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
442 uf00 {X} CSX fip = ? 474 uf00 {X} CSX fp = UFLP.limit ( uflp (X⊆PP CSX)
443 -- UFLP.limit ( uflp 475 ( MaximumFilter.mf (maxf CSX fp) )
444 -- ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? )) 476 (F→ultra (X⊆PP CSX) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)))
445 -- ?
446 -- (F→ultra LP ? ? (F CSX fip) ? ? ? ) )
447 477
448 -- some day 478 -- some day
449 FIP→UFLP : Set (suc (suc n)) 479 FIP→UFLP : Set (suc (suc n))
450 FIP→UFLP = {P : HOD} (TP : Topology P) → FIP TP 480 FIP→UFLP = {P : HOD} (TP : Topology P) → FIP TP
451 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF 481 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
452 482
453 -- product topology of compact topology is compact 483 -- product topology of compact topology is compact
454 484
455 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) 485 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ)
456 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflp ) where 486 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflp ) where
457 L = pbase TP TQ 487 L = pbase TP TQ
458 LPQ = pbase⊆PL TP TQ 488 LPQ = pbase⊆PL TP TQ
459 -- Product of UFL has limit point 489 -- Product of UFL has limit point
460 uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F) 490 uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP) (UF : ultra-filter F)
461 → UFLP (ProductTopology TP TQ) LP F LF UF 491 → UFLP (ProductTopology TP TQ) LP F UF
462 uflp {L} LP F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} } 492 uflp {L} LP F UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} }
463 493
464 494
465 495