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

changeset 1224:e1a1161df14c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Tue, 07 Mar 2023 15:43:30 +0900
parents 4b6c3ed64dd1
children 5c4a088ae95b
files src/Tychonoff.agda src/ZProduct.agda
diffstat 2 files changed, 24 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Tue Mar 07 12:13:21 2023 +0900
+++ b/src/Tychonoff.agda	Tue Mar 07 15:43:30 2023 +0900
@@ -325,6 +325,11 @@
      uflQ : (F : Filter {Power Q} {Q} (λ x → x))  (UF : ultra-filter F)
              → UFLP TQ F UF
      uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF
+     FPQ→FQP :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power (ZFP Q P)} {ZFP Q P } (λ x → x) 
+     FPQ→FQP F = record { filter =  ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
+     projFP :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
+             → Filter {Power P} {P} (λ x → x)
+     projFP = ?
      -- Product of UFL has a limit point
      uflPQ :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
              → UFLP (ProductTopology TP TQ) F UF
@@ -473,15 +478,6 @@
                   ty51 = filter2 F ty53 ty52 ty54
                   ty50 : filter F ∋ ZFP (p ∩ q) Q
                   ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
-         ZFP\Q : {P Q p : HOD} → ( ZFP P Q ＼ ZFP p Q ) ≡ ZFP (P ＼ p) Q
-         ZFP\Q {P} {Q} {p} = ==→o≡ record { eq→ = ty70 ; eq← = ty71 } where
-            ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x →  odef (ZFP (P ＼ p) Q) x
-            ty70 ⟪ ab-pair {a} {b} Pa pb  , npq ⟫ = ab-pair ty72 pb  where
-               ty72 : odef (P ＼ p ) a
-               ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫
-            ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x 
-            ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb 
-                , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ 
          UFP : ultra-filter FP
          UFP = record { proper = ty61 ; ultra = ty60 } where
             ty61 : ¬ (FPSet ∋ od∅)
@@ -495,7 +491,7 @@
             ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} 
                 (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ?
             ... | case1 fp  = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp )
-            ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp)  (subst (λ k → odef (filter F) k) (cong (&) ZFP\Q) fnp ))
+            ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp)  (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp ))
          uflp : UFLP TP FP UFP
          uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
 
--- a/src/ZProduct.agda	Tue Mar 07 12:13:21 2023 +0900
+++ b/src/ZProduct.agda	Tue Mar 07 15:43:30 2023 +0900
@@ -270,6 +270,24 @@
        zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx)
        zfp04 (ab-pair x x₁) = x 
 
+open import BAlgebra O
+
+ZFP\Q : {P Q p : HOD} → (( ZFP P Q ＼ ZFP p Q ) ≡ ZFP (P ＼ p) Q ) ∧ (( ZFP P Q ＼ ZFP P p ) ≡ ZFP P (Q ＼ p) )
+ZFP\Q {P} {Q} {p} = ⟪ ==→o≡ record { eq→ = ty70 ; eq← = ty71 } , ==→o≡ record { eq→ = ty73 ; eq← = ty75 } ⟫ where
+    ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x →  odef (ZFP (P ＼ p) Q) x
+    ty70 ⟪ ab-pair {a} {b} Pa pb  , npq ⟫ = ab-pair ty72 pb  where
+       ty72 : odef (P ＼ p ) a
+       ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫
+    ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x 
+    ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb 
+        , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ 
+    ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x →  odef (ZFP P (Q ＼ p) ) x
+    ty73 ⟪ ab-pair {a} {b} pa Qb  , npq ⟫ = ab-pair pa ty72  where
+       ty72 : odef (Q ＼ p ) b
+       ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫
+    ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x 
+    ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb 
+        , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫