Members/kono/Proof/ZF-in-agda: src/Topology.agda comparison

comparison src/Topology.agda @ 1152:e1c6719a8c38

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Wed, 18 Jan 2023 09:30:26 +0900
parents	8a071bf52407
children	5eb972738f9b

comparison

equal deleted inserted replaced

-:8a071bf52407
+:e1c6719a8c38
 --  we may need these if OS ∋ L is necessary
 --     p    : {x : HOD} → L ∋ x → HOD
 --     Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
 --     px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
-GeneratedTopogy : (L P : HOD) → IsSubBase L P  → Topology L
+InducedTopology : (L P : HOD) → IsSubBase L P  → Topology L
-GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00
+InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00
 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where
 tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x
 tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x ))
 tp00 : SO L P ⊆ Power L
 tp00 {u} ou x ux  with ou ux
 pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where
 tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q))
 tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq )
 ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-ProductTopology {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ }
+ProductTopology {P} {Q} TP TQ =  InducedTopology (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ }
--- covers
+-- covers  ( q ⊆ Union P )
 record _covers_ ( P q : HOD  ) : Set n where
 field
 cover   : {x : Ordinal } → odef q x → Ordinal
 P∋cover : {x : Ordinal } → (lt : odef q  x) → odef P (cover lt)
 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 )
 --
 --   X covres L means Intersection of (CX X) contains nothing
---     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP )
+--     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
 --     it means there is a finite cover
 --
 record CFIP (X x : Ordinal) : Set n where
 field
 is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z)
 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
 fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
 fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
-cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc))
+cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc))   -- this will be the finite cover
 CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc)
 CXfip {X} ox oc  = ODC.x∋minimal O (Cex X) (fip00 ox oc)
 --
 -- this defines finite cover
 finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
 fip34 : * z1 ⊆ L
 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
 fip33 : z1 ≡ w
 fip33 = begin
 z1 ≡⟨ sym &iso ⟩
 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
 & (L ＼ * z) ≡⟨ sym x=ψz ⟩
 w ∎ where open ≡-Reasoning
 fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z)))
 fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
 fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
 fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L ＼ z₁)))
 fip35 = subst (λ k → Finite-∪ (* X) k)
 (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
 -- is also a cover
 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
 ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
--- record { cover = λ {x} Lx → ?  ; P∋cover = ? ; isCover = ? }
 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ )  ⟫
 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx  ⟫
 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
 ... | case2 Lb = cover cb Lb
 fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt)
 fip46 {x} Lab with  fip45 {L} {a} {b} Lab
 ... | case1 La = P∋cover ca La
 ... | case2 Lb = P∋cover cb Lb
 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x
 fip47 {x} Lab with  fip45 {L} {a} {b} Lab
 ... | case1 La = isCover ca La
 ... | case2 Lb = isCover cb Lb
 fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y
 → (Replace' (* x) (λ z xz → L ＼  z )) covers (L ＼ * y )
 fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
 ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where
 fip41 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * a)
 fip41 = fip40 x a x⊆r sa
 fip42 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * b)
 fip42 = fip40 x b x⊆r sb
 fip40 x y x⊆r (gi sb) with x⊆r sb
 ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
 fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal
 fip51 {w} Lyw = z
 fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z
 fip52 {w} Lyw = az
 fip55 : * z ⊆ L
 fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1
 fip56 : * z ≡ L ＼ * y
 fip56 = begin
 * z ≡⟨ sym (L＼Lx=x fip55 ) ⟩
 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso)  ⟩
 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz)  ⟩
 L ＼ * y ∎  where open ≡-Reasoning
 fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z
 fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
 fip54 : z ≡ & ( L ＼ * y )
 fip54 = begin
 z ≡⟨ sym &iso ⟩
 & (* z) ≡⟨ cong (&) fip56 ⟩
 & (L ＼ * y )
 ∎ where open ≡-Reasoning
 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 -- some day
 Compact→FIP : Set (suc n)
 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 → Set n
 fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x
+N : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → HOD
+N {X} CSX fip = record { od = record { def = λ x → Base L P X x ∧ ( o∅ o< x ) } ; odmax = ? ; <odmax = ? }
 F : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → Filter {L} {P} LP
-F = ?
+F {X} CSX fip = record { filter = N CSX fip ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-uf00 {X} CSX fip = UFLP.limit ( uflp (F CSX fip)  ? (F→ultra LP ? ? (F CSX fip)  ? ? ? ) )
+uf00 {X} CSX fip = UFLP.limit ( uflp
+( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? ))
+?
+(F→ultra LP ? ? (F CSX fip)  ? ? ? ) )
 -- some day
 FIP→UFLP : Set (suc (suc n))
 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

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

comparison src/Topology.agda @ 1152:e1c6719a8c38