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

changeset 1213:22de2d4f7271

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, 05 Mar 2023 12:16:07 +0900
parents 3922fc5c6f9e
children 93e1869bb57c
files src/Tychonoff.agda
diffstat 1 files changed, 69 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Sat Mar 04 11:39:52 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 12:16:07 2023 +0900
@@ -35,7 +35,7 @@
 open import filter O
 open import OPair O
 open import Topology O
-open import maximum-filter O
+-- open import maximum-filter O
 
 open Filter
 open Topology
@@ -152,11 +152,11 @@
      -- then we have maximum ultra filter
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     maxf {X} 0<X CSX fp = {!!} -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
      ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     ultraf {X} 0<X CSX fp = {!!} -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      --
      -- so i has a limit as a limit of UIP
      --
@@ -193,6 +193,9 @@
         uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x
         uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
            ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  ; u⊆P = x⊆P ; x⊆u = λ x → x  }
+        uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x ))))
+        uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03
+        -- uf06 (same as uf061) have yellow if zorn lemma is not imported
         uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x ))
         uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso (UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03  )
         uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
@@ -321,30 +324,72 @@
      uflPQ :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
              → UFLP (ProductTopology TP TQ) F UF
      uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
+         F∋PQ : odef (filter F) (& (ZFP P Q))
+         F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) )  (λ z az → proj1 (subst (λ k → odef k z) *iso az ) )
+         ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp )
+         ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
+             fl20 :  (ZFP P Q ＼ Ord o∅) =h=  ZFP P Q
+             fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  }
+         0<P : o∅ o< & (ZFP P Q)
+         0<P with trio< o∅ (& (ZFP P Q))
+         ... | tri< a ¬b ¬c = a
+         ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) )
+         ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+         isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q 
+         isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q
+         F⊆pxq : {x : HOD } → filter F ∋ x →  x ⊆ ZFP P Q
+         F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
+         FPSet : HOD
+         FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
+         FPSet⊆PP :  FPSet  ⊆ Power P
+         FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
+         ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } 
+            = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
+               (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1))  )
          FP : Filter {Power P} {P} (λ x → x)
-         FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
-             ty00 {x} ⟪ PPx , ppf ⟫ = PPx
+         FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = {!!} } where
+             ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q
+             ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = record { z = _ ; az = ty02 ; x=ψz = cong (&) ty04 }  where
+                  --  p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter.Filter.filter F)) (sym &iso) fx) xy))
+                  --  x = ( px , qx )  , px ⊆ q
+                  ty03 : Power (ZFP P Q) ∋ ZFP q Q
+                  ty03 z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq )
+                  p⊆P : p ⊆ P
+                  p⊆P {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz))  pw
+                  ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
+                       (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 ))  )
+                  x⊆pxq : * x ⊆ ZFP p Q
+                  x⊆pxq = ?
+                  ty05 : filter F ∋  ZFP p Q
+                  ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq
+                  ty06 : ZFP p Q ⊆ ZFP q Q
+                  ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
+                  ty02 : filter F ∋  ZFP q Q
+                  ty02 = filter1 F ty03 ty05 ty06
+                  ty04 : q ≡ Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 
+                       (F⊆pxq (subst (odef (filter F)) (sym &iso) ty02) xy)))
+                  ty04 = ?
+
          UFP : ultra-filter FP
-         UFP = record { proper = ? ; ultra = ? }
+         UFP = record { proper = {!!} ; ultra = {!!} }
          uflp : UFLP TP FP UFP
          uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
 
          FQ : Filter {Power Q} {Q} (λ x → x)
-         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = {!!} ; filter2 = {!!} } where
              ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
              ty00 {x} ⟪ QPx , ppf ⟫ = QPx
          UFQ : ultra-filter FQ
-         UFQ = record { proper = ? ; ultra = ? }
+         UFQ = record { proper = {!!} ; ultra = {!!} }
          uflq : UFLP TQ FQ UFQ
          uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
-         Pf = ?
-         pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F
-         pq⊆F = ?
+         Pf = {!!}
+         pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → {!!} ⊆ filter F
+         pq⊆F = {!!}
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v
-         isL {v} npq = ? where
+         isL {v} npq = {!!} where
              bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
              bpq = Neighbor.ou npq (Neighbor.ux npq)
              pqb : Subbase (pbase TP TQ) (Base.b bpq )
@@ -359,27 +404,27 @@
                  --    BaseP ∩ F is not empty
                  --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F ,
                  il1 : odef (Power P) z ∧ ZProj1 (filter F) z
-                 il1 = ? -- UFLP.is-limit uflp ? bz
+                 il1 = {!!} -- UFLP.is-limit uflp ? bz
                  nei1 : HOD
                  nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
                  plimit : Ordinal
                  plimit = UFLP.limit uflp
                  nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
-                 nproper = ?
+                 nproper = {!!}
                  b∋z : odef nei1 z
-                 b∋z = ?
+                 b∋z = {!!}
                  bp : BaseP {P} TP Q z
-                 bp = record { p = ? ; op = ? ; prod = ? }
+                 bp = record { p = {!!} ; op = {!!} ; prod = {!!} }
                  neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
-                 neip = ?
+                 neip = {!!}
                  il2 : * z ⊆ ZFP (Power P) (Power Q)
-                 il2 = ?
-                 il3 : filter F ∋ ?
-                 il3 = ?
+                 il2 = {!!}
+                 il3 : filter F ∋ {!!}
+                 il3 = {!!}
                  fz : odef (filter F) z
-                 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)
-             base⊆F (gi (case2 qx)) b⊆u {z} bz = ?
-             base⊆F (g∩ b1 b2) b⊆u {z} bz = ?
+                 fz = subst (λ k → odef (filter F) k) &iso (filter1 F {!!} {!!} {!!})
+             base⊆F (gi (case2 qx)) b⊆u {z} bz = {!!}
+             base⊆F (g∩ b1 b2) b⊆u {z} bz = {!!}