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

changeset 1222:9f955d49e162

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proj P of Filter F done
author kono
date Tue, 07 Mar 2023 09:00:03 +0900
parents 0e8306b146f6
children 4b6c3ed64dd1
files src/Tychonoff.agda
diffstat 1 files changed, 40 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Mon Mar 06 20:13:00 2023 +0900
+++ b/src/Tychonoff.agda	Tue Mar 07 09:00:03 2023 +0900
@@ -407,67 +407,74 @@
          ... | 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))  )
+         X=F : (x : Ordinal) (p : HOD) (fx : odef (filter F) x) → Set n
+         X=F x p fx = & p ≡ & (Replace' (* x) (λ y xy →
+           * (zπ1 (f⊆L F
+             (subst (odef (filter F)) (sym &iso) fx)
+             (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))))
+         x⊆pxq : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F x p fx → * x ⊆ ZFP p Q
+         x⊆pxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
+         ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
+              ty21 : ZFProduct P Q (& (* (& < * a , * b >)))
+              ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw)  
+              ty32 : ZFProduct P Q (& (* (& < * a , * b >)))
+              ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx)
+                    (& (* (& < * a , * b >))) (subst (λ k → odef k 
+                    (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw))
+              ty07 : odef (* x) (& < * a , * b >) 
+              ty07 = xw
+              ty08 : odef p a
+              ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))  
+                   record { z = _ ; az = xw ;  x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where
+                 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
+                 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
+                 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
+         p⊆P : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F x p fx → p ⊆ P
+         p⊆P {x} {p} fx x=ψz {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 ))  )
          FP : Filter {Power P} {P} (λ x → x)
          FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } 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 = FPSet∋zpq q⊆P (ty10 ty05 ty06 )
                 where
-                  --  p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter.Filter.filter F)) (sym &iso) fx) xy))
+                  --  p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (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 ))  )
                   q⊆P : q ⊆ P
                   q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
-                  x⊆pxq : * x ⊆ ZFP p Q
-                  x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
-                  ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
-                      ty21 : ZFProduct P Q (& (* (& < * a , * b >)))
-                      ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw)  
-                      ty32 : ZFProduct P Q (& (* (& < * a , * b >)))
-                      ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx)
-                            (& (* (& < * a , * b >))) (subst (λ k → odef k 
-                            (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw))
-                      ty07 : odef (* x) (& < * a , * b >) 
-                      ty07 = xw
-                      ty08 : odef p a
-                      ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))  
-                           record { z = _ ; az = xw ;  x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where
-                         ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
-                         ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
-                         ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
                   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
+                  ty05 = filter1 F (λ z wz → isP→PxQ (p⊆P fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆pxq fx x=ψz)
                   ty06 : ZFP p Q ⊆ ZFP q Q
                   ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
                   ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋  ZFP q Q
                   ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
              ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q)
-             ty02 {p} {q} record { z = zp ; az = azp ; x=ψz = x=ψzp } record { z = zq ; az = azq ; x=ψz = x=ψzq } Ppq 
+             ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp }
+                          record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq 
                 = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where
-                  x⊆pxq : * ? ⊆ ZFP p Q
-                  x⊆pxq = ?
                   ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
                   ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
                      pqz :  odef (ZFP (p ∩ q) Q)  z
                      pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
-                     pqz1 :  odef P (zπ1 pqz)
-                     pqz1 = ?
-                     pqz2 :  odef Q (zπ2 pqz)
-                     pqz2 = ?
+                     pqz1 : odef P (zπ1 pqz)
+                     pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz))
+                     pqz2 : odef Q (zπ2 pqz)
+                     pqz2 = zp2 pqz
                   ty53 : filter F ∋ ZFP p Q 
-                  ty53 = filter1 F (λ z wz → isP→PxQ ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq
+                  ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) 
+                     (subst (λ k → odef k z) *iso wz)) 
+                     (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
                   ty52 : filter F ∋ ZFP q Q 
-                  ty52 = ?
+                  ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) 
+                     (subst (λ k → odef k z) *iso wz)) 
+                     (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
                   ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
                   ty51 = filter2 F ty53 ty52 ty54
                   ty50 : filter F ∋ ZFP (p ∩ q) Q
                   ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
 
-
          UFP : ultra-filter FP
          UFP = record { proper = {!!} ; ultra = {!!} }
          uflp : UFLP TP FP UFP