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

changeset 1106:3b894bbefe92

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Dec 2022 00:28:24 +0900
parents fabcb7d9f50c
children f4c398c60c67
files src/ODUtil.agda src/Topology.agda
diffstat 2 files changed, 43 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODUtil.agda	Fri Dec 30 20:59:14 2022 +0900
+++ b/src/ODUtil.agda	Sat Dec 31 00:28:24 2022 +0900
@@ -198,3 +198,11 @@
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
 ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso  
 
+Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD } 
+   → ( {z : Ordinal  } → (az : odef A z ) →  (ψa (* z) (subst (odef A) (sym &iso) az) ≡ ψb (* z) (subst (odef B) (sym &iso) (A⊆B az))))
+   → Replace' A ψa ⊆ Replace' B ψb 
+Repl⊆ {A} {B} A⊆B {ψa} {ψb} eq  record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = A⊆B az  
+         ; x=ψz = trans  x=ψz (cong (&) (eq az) ) }
+
+
+
--- a/src/Topology.agda	Fri Dec 30 20:59:14 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 00:28:24 2022 +0900
@@ -102,24 +102,32 @@
 
 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
    field
-       p : Ordinal
-       q : Ordinal
+       p q : Ordinal
        op : odef (OS TP) p
-       qq : odef Q q
-       prod : x ≡ & < * p , * q >
+       prod : x ≡ & (ZFP (* p) Q )
 
 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
    field
-       p : Ordinal
-       q : Ordinal
+       p q  : Ordinal
        oq : odef (OS TQ) q
-       pp : odef P p
-       prod : x ≡ & < * p , * q >
+       prod : x ≡ & (ZFP P (* q ))
+
+base : {P Q : HOD} → Topology P → Topology Q → HOD
+base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
+
+record BU {P Q : HOD} (TP : Topology P) (TQ : Topology Q) (x : Ordinal ) : Set n where
+   field
+       b  : Ordinal
+       pb : odef (Power (base TP TQ)) b
+       pu : odef (Union (* b)) x 
+
+POS : {P Q : HOD} → Topology P → Topology Q → HOD
+POS {P} {Q} TP TQ = record { od = record { def = λ x → BU TP TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
 
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
 _Top⊗_ {P} {Q} TP TQ = record {
-       OS    = POS
-    ;  OS⊆PL = ?
+       OS    = POS TP TQ
+    ;  OS⊆PL = tp10
     ;  o∪ = ?
     ;  o∩ = ?
   } where
@@ -127,11 +135,12 @@
         box = ZFP (OS TP) (OS TQ) 
         --  B : (OS P ∋ x →  proj⁻¹ x ) ∨ (OS Q ∋ y  →  proj⁻¹ y )
         --  U ⊂ ZFP P Q  ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧  b ⊂ U )
-        base : HOD
-        base = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
-        POS : HOD
-        POS = record { od = record { def = λ x → {b : Ordinal } → odef (Power base) b ∧ odef (Union (* b)) x } 
-            ; odmax = & (ZFP P Q) ; <odmax = ? }
+        tp10 : POS TP TQ ⊆ Power (ZFP P Q)
+        tp10 {x} record { b = b ; pb = pb ; pu = record { owner = z ; ao = bz ; ox = zx } } y xy = tp11 where
+             tp11 : odef (ZFP P Q) y
+             tp11 with pb _ bz
+             ... | case1 record { p = p ; q = q ; op = op ; prod = prod } = ?
+             ... | case2 x =  ?
 
 -- existence of Ultra Filter 
 
@@ -161,27 +170,29 @@
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
     uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
             (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
-    uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where
-         LP : HOD  
-         LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
-         LPP : LP ⊆ Power P
-         LPP record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) 
+    uflp {L} LPQ F uf = record { limit = & < * ( UFLP.limit uflpp) , ? >  ; P∋limit = ? ; is-limit = ? } where
+         LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD  
+         LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
+         LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P
+         LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) 
            (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) )  xw) where
              tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P
              tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1)  ) 
                   (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where
                     tp03 : odef (* z) z1 →  odef (* (& (* z))) (& (* z1)) 
                     tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
-         FP : Filter LPP
-         FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
+         FP : Filter (LPP L LPQ)
+         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where
+             tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ
+             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } 
          uFP : ultra-filter FP
          uFP = record { proper = ? ; ultra = ? }
+         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP
+         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP 
          LQ : HOD  
          LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LQQ : LQ ⊆ Power Q
          LQQ = ?
-         uflpp : UFLP {P} TP {LP} LPP FP uFP
-         uflpp = record { limit = ? ; P∋limit = ? ; is-limit = ? }