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

changeset 1119:5b0525cb9a5d

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 Mon, 02 Jan 2023 10:15:20 +0900
parents 441ad880a45d
children e086a266c6b7
files src/Topology.agda
diffstat 1 files changed, 47 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 01 20:28:07 2023 +0900
+++ b/src/Topology.agda	Mon Jan 02 10:15:20 2023 +0900
@@ -41,23 +41,24 @@
        o∪ : { P : HOD }  →  P ⊂ OS                → OS ∋ Union P
 -- closed Set
    CS : HOD
-   CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
-       tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
-       tp02 {y} nop = ?
+   CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where
+       tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L ＼ * y)) → y o< osuc (& L)
+       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  )
-       -- ∈∅< ( proj1 nop )
 
 open Topology
 
--- Base
--- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
--- W ⊆ U ∩ V and x ∈ W .
+-- Subbase P
+--   A set of countable intersection of P will be a base (x ix an element of the base)
 
 data Subbase (P : HOD) : Ordinal → Set n where
    gi : {x : Ordinal } → odef P x → Subbase P x
    g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))
 
+--
+--   if y is in a Subbase, some element of P contains it 
+
 sbp :  (P : HOD) {x : Ordinal } → Subbase P x → Ordinal
 sbp P {x} (gi {y} px) = x
 sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb
@@ -66,6 +67,8 @@
 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫
 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso  xy))
 
+--  An open set generate from a base
+--
 --  OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →  x ∈ b ⊂ U }
 
 record Base (L P : HOD) (u x : Ordinal) : Set n where
@@ -75,14 +78,17 @@
        sb  : Subbase P b
        b⊆u : * b ⊆ * u
        bx  : odef (* b) x
+   x⊆L : odef L x 
+   x⊆L = u⊂L (b⊆u bx)
 
 SO : (L P : HOD) → HOD
-SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = ? ; <odmax = ? }
+SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where
+    tp00 :  {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L)
+    tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) 
 
 record IsSubBase (L P : HOD) : Set (suc n) where
    field
        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
@@ -143,31 +149,30 @@
 
 -- Finite Intersection Property
 
-data Finite-∩ (S : HOD) : HOD → Set (suc n) where
-   fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
-   fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
-
 record FIP {L : HOD} (top : Topology L) : Set (suc n) where
    field
-       fipS⊆PL :  L ⊆ CS top
-       fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )
+       fip≠φ : { C : HOD } { x : Ordinal } → C ⊆ CS top → Subbase C x → o∅ o< x 
 
 -- Compact
 
-data Finite-∪ (S : HOD) : HOD → Set (suc n) where
-   fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
-   fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
+data Finite-∪ (S : HOD) : Ordinal → Set n where
+   fin-e : {x : Ordinal } → odef S x → Finite-∪ S x
+   fin-∪  : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
 
 record Compact  {L : HOD} (top : Topology L)  : Set (suc n) where
    field
        finCover  : {X : HOD} → X ⊆ OS top → X covers L → HOD
        isCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
-       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp  )
+       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (& (finCover xo xcp  ) )
 
 -- FIP is Compact
 
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
-FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }
+FIP→Compact {L} top fip = record { finCover = finCover ; isCover = ? ; isFinite = ? } where
+    finCover  : {C : HOD} → C ⊆ OS top → C covers L → HOD
+    finCover {C} C<T CL = record { od = record { def = λ x → odef L x ∧ ( ¬ Subbase C x) } ; odmax = & L ; <odmax = odef∧< }
+    isConver : {C : HOD} (xo : C ⊆ OS top) (xcp : C covers L) → (finCover xo xcp) covers L
+    isConver {C} xo xcp = record { cover = λ lx → ? ; P∋cover = ? ; isCover = ? }
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
 Compact→FIP = {!!}
@@ -176,6 +181,9 @@
 
 open ZFProduct
 
+-- Product Topology is not 
+--     ZFP (OS TP) (OS TQ) (box)
+
 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
    field
        p q : Ordinal
@@ -188,27 +196,27 @@
        oq : odef (OS TQ) q
        prod : x ≡ & (ZFP P (* q ))
 
--- box : HOD
--- box = ZFP (OS TP) (OS TQ)
+pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x
+pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+    tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
+    tp01 w wz with subst (λ k → odef k w ) *iso wz
+    ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
+        tp03 : odef P a
+        tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
+pbase⊆PL {P} {Q} TP TQ {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+    tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
+    tp01 w wz with subst (λ k → odef k w ) *iso wz
+    ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
+        tp03 : odef Q b
+        tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
 
-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 = ? }
+pbase : {P Q : HOD} → Topology P → Topology Q → HOD
+pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where
+    tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q))
+    tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) 
 
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) record { P⊆PL = tp00 } where
-    tp00 : base TP TQ ⊆ Power (ZFP P Q)
-    tp00 {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
-        tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
-        tp01 w wz with subst (λ k → odef k w ) *iso wz
-        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
-            tp03 : odef P a
-            tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
-    tp00 {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
-        tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
-        tp01 w wz with subst (λ k → odef k w ) *iso wz
-        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
-            tp03 : odef Q b
-            tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
+_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ }
 
 -- existence of Ultra Filter
 
@@ -230,7 +238,7 @@
 
 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 { fipS⊆PL = ? ; fip≠φ = ? }
+UFLP→FIP {P} TP uflp = record { fip≠φ = ? }
 
 -- Product of UFL has limit point (Tychonoff)