Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1225:5c4a088ae95b
Proj2 of F
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Mar 2023 18:24:42 +0900 |
| parents | e1a1161df14c |
| children | c8f5376a9623 |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 135 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Tue Mar 07 15:43:30 2023 +0900 +++ b/src/Tychonoff.agda Tue Mar 07 18:24:42 2023 +0900 @@ -325,11 +325,6 @@ 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 @@ -495,10 +490,143 @@ uflp : UFLP TP FP UFP uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP + isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q + isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) + fx→qx : {x : HOD } → filter F ∋ x → HOD + fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) + fx→qx1 : {q : HOD } {p : Ordinal } → odef P p → (fq : filter F ∋ ZFP P q ) → fx→qx fq ≡ q + fx→qx1 {q} {p} qq fq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where + ty21 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → ZFProduct P Q (& (* (& < * a , * b >))) + ty21 qz pz = F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz )) + ty32 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → zπ2 (ty21 qz pz) ≡ b + ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where + ty33 : {a b x : Ordinal } ( q : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 q ≡ b + 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 (&) b=d) + ty20 : {x : Ordinal} → odef (fx→qx fq) x → odef q x + ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef q k) b=x qz where + ty24 : * x ≡ * b + ty24 = begin + * x ≡⟨ cong (*) x=ψz ⟩ + _ ≡⟨ *iso ⟩ + * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 qz pz) ⟩ + * b ∎ where open ≡-Reasoning + b=x : b ≡ x + b=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) + ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x + ty22 {x} qx = record { z = _ ; az = ab-pair ? ? ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where + ty12 : * x ≡ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) + ty12 = begin + * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩ + * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ∎ where open ≡-Reasoning + FQSet : HOD + FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) ))) + FQSet∋zpq : {q : HOD} → q ⊆ Q → filter F ∋ ZFP P q → FQSet ∋ q + FQSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where + -- brain damaged one + ty11 : {y : HOD} {xy : (* (& (ZFP P q ))) ∋ y } → + * (zπ2 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ2 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) + ty11 {y} {xy} = cong (λ k → * (zπ2 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where + a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy + b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) + ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q + ty10 = begin + Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) + ≡⟨ + cong (λ k → Replace' (* (& (ZFP P q ))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) + ⟩ + Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) + ≡⟨ Replace'-iso _ ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ⟩ + Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ + fx→qx fq ≡⟨ fx→qx1 ? fq ⟩ + q ∎ where open ≡-Reasoning + FQSet⊆PP : FQSet ⊆ Power Q + FQSet⊆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 Q k) (sym (trans x=ψz1 &iso)) + (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) + X=F2 : (x : Ordinal) (q : HOD) (fx : odef (filter F) x) → Set n + X=F2 x q fx = & q ≡ & (Replace' (* x) (λ y xy → + * (zπ2 (f⊆L F + (subst (odef (filter F)) (sym &iso) fx) + (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy))))) + x⊆qxq : {x : Ordinal} {q : HOD} (fx : odef (filter F) x) → X=F2 x q fx → * x ⊆ ZFP P q + x⊆qxq {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 pw ty08 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 b + ty08 = subst (λ k → odef k b ) (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π2 p ≡ b + 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 (&) b=d) + q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ P + q⊆Q {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)) + ? -- (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) FQ : Filter {Power Q} {Q} (λ x → x) - FQ = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = {!!} } + FQ = record { filter = FQSet ; f⊆L = FQSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where + ty01 : {p q : HOD} → Power Q ∋ q → FQSet ∋ p → p ⊆ q → FQSet ∋ q + ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq ? ? -- q⊆P (ty10 ty05 ty06 ) + where + -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy)) + -- x = ( qx , qx ) , qx ⊆ q + ty03 : Power (ZFP P Q) ∋ ZFP P q + ty03 z zpq = isQ→PxQ {* (& q)} ? ? -- ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) (Pq _) + q⊆P : q ⊆ Q + q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) + ty05 : filter F ∋ ZFP P p + ty05 = filter1 F (λ z wz → isQ→PxQ ? ? ) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆qxq fx x=ψz) + ty06 : ZFP P p ⊆ ZFP P q + ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) + ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q + ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq + ty02 : {p q : HOD} → FQSet ∋ p → FQSet ∋ q → Power Q ∋ (p ∩ q) → FQSet ∋ (p ∩ q) + ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } + record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq + = FQSet∋zpq ? ? where -- (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where + ty54 : Power (ZFP P Q) ∋ (ZFP P q ∩ ZFP P q ) + ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where + pqz : odef (ZFP P (p ∩ q) ) z + pqz = ? -- subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz + pqz1 : odef P (zπ1 pqz) + pqz1 = zp1 pqz + pqz2 : odef Q (zπ2 pqz) + pqz2 = ? -- q⊆Q fzp x=ψzp (proj2 (zp2 pqz)) + ty53 : filter F ∋ ZFP P q + ty53 = ? -- filter1 F (λ z wz → isQ→PxQ ? -- (q⊆Q fzp x=ψzp) + -- (subst (λ k → odef k z) *iso wz)) + -- (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp) + ty52 : filter F ∋ ZFP P q + ty52 = ? -- filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) + -- (subst (λ k → odef k z) *iso wz)) + -- (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq) + ty51 : filter F ∋ ( ZFP P q ∩ ZFP q Q ) + ty51 = ? -- filter2 F ty53 ty52 ty54 + ty50 : filter F ∋ ZFP P (p ∩ q) + ty50 = ? -- subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 UFQ : ultra-filter FQ - UFQ = record { proper = {!!} ; ultra = {!!} } + UFQ = record { proper = ty61 ; ultra = ty60 } where + ty61 : ¬ (FQSet ∋ od∅) + ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where + ty63 : {x : Ordinal} → ¬ odef (* z) x + ty63 {x} zx with x⊆qxq az x=ψz zx + ... | ab-pair xp xq = ¬x<0 xq + ty62 : odef (filter F) (& od∅) + ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az + ty60 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (FQSet ∋ p) ∨ (FQSet ∋ (Q ＼ p)) + ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q} + (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) ? + ... | case1 fq = case1 (FQSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fq ) + ... | case2 fnp = case2 (FQSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj2 ZFP\Q)) fnp )) + uflq : UFLP TQ FQ UFQ uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ