Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/Topology.agda @ 1169:46dc298bdd77
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 22 Jan 2023 10:38:52 +0900 |
parents | 938ada7fd66c |
children | b2ca37e81ad0 |
line wrap: on
line diff
--- a/src/Topology.agda Sat Jan 21 20:20:43 2023 +0900 +++ b/src/Topology.agda Sun Jan 22 10:38:52 2023 +0900 @@ -461,15 +461,18 @@ v⊆P : * v ⊆ P o⊆u : * u ⊆ * v -record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) +record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) ) (ultra : ultra-filter F ) : Set (suc (suc n)) where field limit : Ordinal P∋limit : odef P limit is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v) +-- +-- Neighbor on x is a Filter (on Power P) +-- NeighborF : {P : HOD} (TP : Topology P) (x : Ordinal ) → Filter {Power P} {P} (λ x → x) -NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = ? } where +NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = f2 } where nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v nf00 {v} nei y vy = Neighbor.v⊆P nei vy NF : HOD @@ -491,6 +494,7 @@ f20 : * upq ⊆ * (& (p ∩ q)) f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq → ⟪ subst (λ k → odef k x) *iso (Neighbor.o⊆u Np (proj1 pq)) , subst (λ k → odef k x) *iso (Neighbor.o⊆u Nq (proj2 pq)) ⟫ ) + -- FIP is UFL -- filter Base @@ -509,7 +513,7 @@ ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px ) UFLP→FIP : {P : HOD} (TP : Topology P) → - ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP + ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP UFLP→FIP {P} TP uflp with trio< (& P) o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where @@ -557,70 +561,60 @@ proper = ? maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) + ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( MaximumFilter.mf (maxf CSX fp)) + ultraf {X} CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal - uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x) - ( MaximumFilter.mf (maxf CSX fp) ) - (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp))) + uf00 {X} CSX fp = UFLP.limit ( uflp ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp)) uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CSX fip) - uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp (λ x → x) - ( MaximumFilter.mf (maxf CSX fp) ) - (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp))) - record { u = ? ; ou = ? ; ux = ? ; v⊆P = ? ; o⊆u = ? } ? + uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp)) ? ? + FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP - → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF -FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where + → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF +FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where CF : HOD CF = Replace' (filter F) (λ x fx → Cl TP x ) CF⊆CS : CF ⊆ CS TP CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x ufl01 = ? + ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ) + ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ufl00 : {v : Ordinal} → Neighbor TP (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ) v → filter F ⊆ * v - ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } {x} fx = ? + ufl00 {v} nei {x} fx = ? -- product topology of compact topology is compact Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where - uflP : {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP) (UF : ultra-filter F) - → UFLP TP LP F UF - uflP {L} LP F UF = FIP→UFLP TP (Compact→FIP TP CP) LP F UF - uflQ : {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP) (UF : ultra-filter F) - → UFLP TQ LP F UF - uflQ {L} LP F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) LP F UF + uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F) + → UFLP TP F UF + uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF + 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 -- Product of UFL has limit point - uflPQ : {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ) (UF : ultra-filter F) - → UFLP (ProductTopology TP TQ) LPQ F UF - uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where - LP : HOD -- proj1 of LPQ - LP = Proj1 L (Power P) (Power Q) - LPP : LP ⊆ Power P - LPP {x} ⟪ Px , p1 ⟫ = Px - FP : Filter {LP} {P} LPP + 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 + 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) ⊆ LP - ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = ZProj1.pq (ppf y) - ; opq = ZProj1.opq (ppf y) ; Lpq = f⊆L F (ZProj1.Lpq (ppf y)) ; x=pi1 = ZProj1.x=pi1 (ppf y) } ) ⟫ + ty00 : Proj1 (filter F) (Power P) (Power Q) ⊆ Power P + ty00 {x} ⟪ PPx , ppf ⟫ = PPx UFP : ultra-filter FP UFP = record { proper = ? ; ultra = ? } - uflp : UFLP TP LPP FP UFP - uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP + uflp : UFLP TP FP UFP + uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP - LQ : HOD -- proj1 of LPQ - LQ = Proj2 L (Power P) (Power Q) - LQP : LQ ⊆ Power Q - LQP {x} ⟪ Qx , q1 ⟫ = Qx - FQ : Filter {LQ} {Q} LQP + FQ : Filter {Power Q} {Q} (λ x → x) FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where - ty00 : Proj2 (filter F) (Power P) (Power Q) ⊆ LQ - ty00 {x} ⟪ QPx , ppf ⟫ = ⟪ QPx , ( λ y → record { pq = ZProj2.pq (ppf y) - ; opq = ZProj2.opq (ppf y) ; Lpq = f⊆L F (ZProj2.Lpq (ppf y)) ; x=pi2 = ZProj2.x=pi2 (ppf y) } ) ⟫ + ty00 : Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q + ty00 {x} ⟪ QPx , ppf ⟫ = QPx UFQ : ultra-filter FQ UFQ = record { proper = ? ; ultra = ? } - uflq : UFLP TQ LQP FQ UFQ - uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) LQP FQ UFQ + 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 = ?