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

changeset 1122:1c7474446754

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add OS ∋ od∅
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Jan 2023 09:39:25 +0900
parents 98af35c9711f
children 256a3ba634f6
files src/Topology.agda
diffstat 1 files changed, 53 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Tue Jan 03 14:17:53 2023 +0900
+++ b/src/Topology.agda	Wed Jan 04 09:39:25 2023 +0900
@@ -39,6 +39,7 @@
        OS⊆PL :  OS ⊆ Power L
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q      → OS ∋ (p ∩ q)
        o∪ : { P : HOD }  →  P ⊂ OS                → OS ∋ Union P
+       OS∋od∅ : OS ∋ od∅
 -- closed Set
    CS : HOD
    CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where
@@ -46,9 +47,20 @@
        tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx ))
    os⊆L :  {x : HOD} → OS ∋ x → x ⊆ L
    os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy  )
+   cs⊆L :  {x : HOD} → CS ∋ x → x ⊆ L
+   cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy )
+   CS∋L : CS ∋ L
+   CS∋L = ⟪ ? , ? ⟫
+--- we may add
+--     OS∋L   :  OS ∋ L
+--     OS∋od∅ :  OS ∋ od∅
 
 open Topology
 
+Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD
+Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x  } 
+  ; odmax = & L ; <odmax = ? }
+
 -- Subbase P
 --   A set of countable intersection of P will be a base (x ix an element of the base)
 
@@ -88,7 +100,7 @@
 
 record IsSubBase (L P : HOD) : Set (suc n) where
    field
-       P⊆PL  : P ⊆ Power L
+       P⊆PL   : P ⊆ Power L
 --  we may need these if OS ∋ L is necessary
 --     p    : {x : HOD} → L ∋ x → HOD
 --     Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
@@ -96,7 +108,9 @@
 
 GeneratedTopogy : (L P : HOD) → IsSubBase L P  → Topology L
 GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00
-         ; o∪ = tp02 ; o∩ = tp01 } where
+         ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where
+    tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x
+    tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) 
     tp00 : SO L P ⊆ Power L
     tp00 {u} ou x ux  with ou ux
     ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx)
@@ -153,11 +167,15 @@
 
 record FIP {L : HOD} (top : Topology L) : Set n where
    field
-       finite : {X : Ordinal } → * X ⊆ CS top 
+       limit : {X : Ordinal } → * X ⊆ CS top → * X ∋ L
           →       ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
-       limit : {X : Ordinal } → (CX : * X ⊆ CS top )
+       is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L )
           → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) 
-          →  {x : Ordinal } → odef (* X) x → odef (* x) (finite CX fip)
+          →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX XL fip)
+   L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L)
+          → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) 
+          →  odef L (limit CX XL fip)
+   L∋limit {X} CX XL fip = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX XL)) (is-limit CX XL fip XL)
 
 -- Compact
 
@@ -196,7 +214,7 @@
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
           fip02 = ?
           fip01 : Ordinal
-          fip01 = FIP.finite fip (CCX ox) fip02
+          fip01 = FIP.limit fip (CCX ox) ? fip02
    ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 
    ¬CXfip {X} ox oc = ? where
       fip04 : odef (Cex ox) (cex ox oc)
@@ -262,7 +280,8 @@
 
 -- Ultra Filter has limit point
 
-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
+record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  
+      (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
    field
        limit : Ordinal
        P∋limit : odef P limit
@@ -271,20 +290,38 @@
 -- FIP is UFL
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
-   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf
-FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FL uf
+FIP→UFLP {P} TP fip {L} LP F FL uf = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
+    where
+      CF : Ordinal
+      CF = & ( Replace' (filter F) (λ z fz → Cl TP z (fip03 fz)) ) where
+         fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
+         fip03 {z} fz {x} zx with LP ( f⊆L F fz )
+         ... | pw = pw x (subst (λ k → odef k x) (sym *iso) zx  )
+      CFP : * CF ∋ P  -- filter F ∋ P
+      CFP = ?
+      fip00 : * CF ⊆ CS TP -- replaced
+      fip00 = ?
+      fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x
+      fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅
+      fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ?
+      fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 ? fip01) → * o ⊆ filter F
+      fip02 {p} oo ol = ? where
+         fip04 : odef ? (FIP.limit fip fip00 ? fip01) 
+         fip04 = FIP.is-limit fip fip00 CFP fip01 ?
+
 
 UFLP→FIP : {P : HOD} (TP : Topology P) →
-   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP
-UFLP→FIP {P} TP uflp = record { fip≠φ = ? }
+   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F ? uf ) → FIP TP
+UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? }
 
 -- Product of UFL has limit point (Tychonoff)
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (TP Top⊗ TQ)
 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 = & < * ( UFLP.limit uflpp) , ? >  ; P∋limit = ? ; is-limit = ? } where
+    uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (LF : filter F ∋ ZFP P Q)
+            (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F ? uf
+    uflp {L} LPQ F LF 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
@@ -301,8 +338,8 @@
              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
+         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