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

changeset 1143:2fe1bc2b962f

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 Sun, 15 Jan 2023 19:30:21 +0900
parents 7b924ef65373
children 73b256c5474b
files src/Topology.agda
diffstat 1 files changed, 58 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sun Jan 15 09:05:22 2023 +0900
+++ b/src/Topology.agda	Sun Jan 15 19:30:21 2023 +0900
@@ -12,6 +12,7 @@
 open import Relation.Nullary
 open import Data.Empty
 open import Relation.Binary.Core
+open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 import BAlgebra
 open BAlgebra O
@@ -214,15 +215,16 @@
 
 record FIP {L : HOD} (top : Topology L) : Set n where
    field
-       limit : {X : Ordinal } → * X ⊆ CS top → * X ∋ L
+       limit : {X : Ordinal } → * X ⊆ CS top 
           →       ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
-       is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L )
+       is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) 
           → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) 
-          →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX XL fip)
-   L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top ) → (XL : * X ∋ L)
+          →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip)
+   L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top ) 
           → ( 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)
+          →  {x : Ordinal } → odef (* X) x 
+          →  odef L (limit CX fip)
+   L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
 
 -- Compact
 
@@ -244,27 +246,60 @@
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
    CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
    CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top 
-   CCX {X} ox = {!!}
+   CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox
+   ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06  ⟫ where --  x ≡ & (L ＼ * z)
+      fip07 : z ≡ & (L ＼ * x)
+      fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where
+          fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x
+          fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ 
+          ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ )
+          fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x)
+          fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw  , subst (λ k → ¬ odef k w) (sym *iso) fip10   ⟫ where
+             fip10 : ¬ (odef (L ＼ * z) w)
+             fip10 ⟪ Lw , nzw ⟫ = nzw zw
+      fip06 : odef (OS top) (& (L ＼ * x))
+      fip06 = os ( subst (λ k → odef (* X) k ) fip07 az )
+      fip05 : * x ⊆ L
+      fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw )
    -- CX has finite intersection
    CXfip : {X : Ordinal } → * X ⊆ OS top → Set n
    CXfip {X} ox =  { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 
-   Cex : {X : Ordinal } → * X ⊆ OS top → HOD
-   Cex {X} ox =  record { od = record { def = λ C → { x : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) o∅ } 
-       ; odmax = osuc ( & (Power L)) ; <odmax = {!!} }
-   -- a counter example of fip , some CX has no finite intersection
+   --
+   --   X covres L means Intersection of (CX X) contains nothing
+   --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP )
+   --     it means there is a finite cover
+   --
+   record CFIP (x : Ordinal) : Set n where
+      field
+         is-CS : * x ⊆ CS top
+         y : Ordinal 
+         ¬fip  : {y : Ordinal } →  Subbase (* x) y →  o∅ ≡ y 
+   Cex : HOD
+   Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → 
+        subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) }
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
-   cex {X} ox oc = & ( ODC.minimal O (Cex ox) fip00)  where
-      fip00 : ¬ ( Cex ox =h= od∅ ) 
-      fip00 cex=0 = fip03 {!!} {!!} where 
+   cex {X} ox oc = & ( ODC.minimal O Cex  fip00)  where
+      fip00 : ¬ ( Cex  =h= od∅ ) 
+      fip00 cex=0 = fip03 (FIP.is-limit fip (CCX ox) fip02 ?) {!!} where 
           fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
           fip03 {x} {z} xz nxz = nxz xz
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
-          fip02 = {!!}
+          fip02 {C} {x} C<CX sc with trio< x o∅ 
+          ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+          ... | tri> ¬a ¬b c = c
+          ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = x ; ¬fip = ? } )) where
+              fip10 : * C ⊆  CS top
+              fip10 {w} cw with subst (λ k → odef k w) *iso ( C<CX cw )
+              ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ ? , ? ⟫
           fip01 : Ordinal
-          fip01 = FIP.limit fip (CCX ox) {!!} fip02
+          fip01 = FIP.limit fip (CCX ox) fip02
+          fip05 : odef (CS top) fip01 
+          fip05 = ?
+          fip04 : Ordinal
+          fip04 = cover oc (cs⊆L top (subst₂ (λ j k → odef j k ) refl (sym &iso) fip05) (FIP.is-limit fip (CCX ox) ? ?) )
    ¬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)
+      fip04 : odef Cex (cex ox oc)
       fip04 = {!!}
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
@@ -298,12 +333,13 @@
 UFLP→FIP : {P : HOD} (TP : Topology P) → {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
 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where
-     fip : {X : Ordinal} → * X ⊆ CS TP → * X ∋ P → Set n
-     fip {X} CSX XP = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x
-     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (XP : * X ∋ P ) → fip {X} CSX XP → Filter {L} {P} LP
+     fip : {X : Ordinal} → * X ⊆ CS TP → Set n
+     fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x
+     F : Filter {L} {P} LP
      F = ?
-     uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (XP : * X ∋ P ) → fip {X} CSX XP → Ordinal
-     uf00 = ?
+     uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
+     uf00 {X} CSX fip = UFLP.limit ( uflp F ? (F→ultra LP ? ? F ? ? ? ) )
+
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  {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