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

changeset 1152:e1c6719a8c38

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 Wed, 18 Jan 2023 09:30:26 +0900
parents 8a071bf52407
children 5eb972738f9b
files src/Topology.agda
diffstat 1 files changed, 32 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Wed Jan 18 01:43:24 2023 +0900
+++ b/src/Topology.agda	Wed Jan 18 09:30:26 2023 +0900
@@ -113,8 +113,8 @@
 --     Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
 --     px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
 
-GeneratedTopogy : (L P : HOD) → IsSubBase L P  → Topology L
-GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00
+InducedTopology : (L P : HOD) → IsSubBase L P  → Topology L
+InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00
          ; 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 ))
@@ -199,9 +199,9 @@
     tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq )
 
 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-ProductTopology {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ }
+ProductTopology {P} {Q} TP TQ =  InducedTopology (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ }
 
--- covers
+-- covers  ( q ⊆ Union P )
 
 record _covers_ ( P q : HOD  ) : Set n where
    field
@@ -273,7 +273,7 @@
       fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw )
    --
    --   X covres L means Intersection of (CX X) contains nothing
-   --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP )
+   --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
    --     it means there is a finite cover
    --
    record CFIP (X x : Ordinal) : Set n where
@@ -309,7 +309,7 @@
        fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
        fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
-   cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc))
+   cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc))   -- this will be the finite cover
    CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc)
    CXfip {X} ox oc  = ODC.x∋minimal O (Cex X) (fip00 ox oc)
    --
@@ -328,23 +328,22 @@
                fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
                fip33 : z1 ≡ w
                fip33 = begin
-                 z1 ≡⟨ sym &iso ⟩ 
-                 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩ 
-                 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ 
-                 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ 
-                 & (L ＼ * z) ≡⟨ sym x=ψz ⟩ 
+                 z1 ≡⟨ sym &iso ⟩
+                 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
+                 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
+                 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
+                 & (L ＼ * z) ≡⟨ sym x=ψz ⟩
                  w ∎ where open ≡-Reasoning
             fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z)))
             fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
         fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
             fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L ＼ z₁)))
-            fip35 = subst (λ k → Finite-∪ (* X) k) 
+            fip35 = subst (λ k → Finite-∪ (* X) k)
                (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
-   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) 
+   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
      ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
-        -- record { cover = λ {x} Lx → ?  ; P∋cover = ? ; isCover = ? }
         fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
         fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
         ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ )  ⟫
@@ -359,24 +358,24 @@
             fip46 {x} Lab with  fip45 {L} {a} {b} Lab
             ... | case1 La = P∋cover ca La
             ... | case2 Lb = P∋cover cb Lb
-            fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x 
+            fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x
             fip47 {x} Lab with  fip45 {L} {a} {b} Lab
             ... | case1 La = isCover ca La
             ... | case2 Lb = isCover cb Lb
         fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y
            → (Replace' (* x) (λ z xz → L ＼  z )) covers (L ＼ * y )
-        fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso) 
+        fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
           ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where
             fip41 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * a)
-            fip41 = fip40 x a x⊆r sa  
+            fip41 = fip40 x a x⊆r sa
             fip42 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * b)
-            fip42 = fip40 x b x⊆r sb 
+            fip42 = fip40 x b x⊆r sb
         fip40 x y x⊆r (gi sb) with x⊆r sb
         ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
-            fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal 
-            fip51 {w} Lyw = z 
-            fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z 
-            fip52 {w} Lyw = az 
+            fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal
+            fip51 {w} Lyw = z
+            fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z
+            fip52 {w} Lyw = az
             fip55 : * z ⊆ L
             fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1
             fip56 : * z ≡ L ＼ * y
@@ -385,16 +384,16 @@
                 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso)  ⟩
                 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz)  ⟩
                 L ＼ * y ∎  where open ≡-Reasoning
-            fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z 
+            fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z
             fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
                fip54 : z ≡ & ( L ＼ * y )
                fip54 = begin
                  z ≡⟨ sym &iso ⟩
                  & (* z) ≡⟨ cong (&) fip56 ⟩
-                 & (L ＼ * y )  
+                 & (L ＼ * y )
                  ∎ where open ≡-Reasoning
-            fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w 
-            fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw 
+            fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
+            fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 
 
 
@@ -422,10 +421,15 @@
 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x
+     N : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → HOD
+     N {X} CSX fip = record { od = record { def = λ x → Base L P X x ∧ ( o∅ o< x ) } ; odmax = ? ; <odmax = ? }
      F : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → Filter {L} {P} LP
-     F = ?
+     F {X} CSX fip = record { filter = N CSX fip ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
      uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     uf00 {X} CSX fip = UFLP.limit ( uflp (F CSX fip)  ? (F→ultra LP ? ? (F CSX fip)  ? ? ? ) )
+     uf00 {X} CSX fip = UFLP.limit ( uflp
+         ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? ))
+         ?
+         (F→ultra LP ? ? (F CSX fip)  ? ? ? ) )
 
 -- some day
 FIP→UFLP : Set (suc (suc n))