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

comparison src/Tychonoff.agda @ 1170:b2ca37e81ad0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Jan 2023 20:04:57 +0900
parents src/Topology.agda@46dc298bdd77
children a839fccdef47
comparison
equal deleted inserted replaced
1169:46dc298bdd77 1170:b2ca37e81ad0
1 open import Level
2 open import Ordinals
3 module Tychonoff {n : Level } (O : Ordinals {n}) where
4
5 open import zf
6 open import logic
7 open _∧_
8 open _∨_
9 open Bool
10
11 import OD
12 open import Relation.Nullary
13 open import Data.Empty
14 open import Relation.Binary.Core
15 open import Relation.Binary.Definitions
16 open import Relation.Binary.PropositionalEquality
17 import BAlgebra
18 open BAlgebra O
19 open inOrdinal O
20 open OD O
21 open OD.OD
22 open ODAxiom odAxiom
23 import OrdUtil
24 import ODUtil
25 open Ordinals.Ordinals O
26 open Ordinals.IsOrdinals isOrdinal
27 open Ordinals.IsNext isNext
28 open OrdUtil O
29 open ODUtil O
30
31 import ODC
32 open ODC O
33
34 open import filter O
35 open import OPair O
36 open import Topology O
37 open import maximum-filter O
38
39 open Filter
40 open Topology
41
42 -- FIP is UFL
43
44 -- filter Base
45 record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
46 field
47 b x : Ordinal
48 b⊆X : * b ⊆ * X
49 sb : Subbase (* b) x
50 u⊆P : * u ⊆ P
51 x⊆u : * x ⊆ * u
52
53 record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) )
54 (ultra : ultra-filter F ) : Set (suc (suc n)) where
55 field
56 limit : Ordinal
57 P∋limit : odef P limit
58 is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F
59
60 UFLP→FIP : {P : HOD} (TP : Topology P) →
61 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
62 UFLP→FIP {P} TP uflp with trio< (& P) o∅
63 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
64 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where
65 -- P is empty
66 fip02 : {x : Ordinal } → ¬ odef P x
67 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
68 ... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where
69 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
70 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
71 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
72 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
73 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) }
74 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
75 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb
76 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → HOD
77 nc = ?
78 N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → odef (N CSX fp) (& (nc CSX fp) )
79 N∋nc = ?
80 0<PP : o∅ o< & (Power P)
81 0<PP = ?
82 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
83 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
84 f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
85 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
86 record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
87 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where
88 f10 : q ⊆ P
89 f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx ))
90 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
91 f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
92 p∩q⊆p : * (& (p ∩ q)) ⊆ P
93 p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
94 Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
95 xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
96 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
97 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
98 f20 : * (& Np+Nq) ⊆ * X
99 f20 {x} npq with subst (λ k → odef k x) *iso npq
100 ... | case1 np = FBase.b⊆X Np np
101 ... | case2 nq = FBase.b⊆X Nq nq
102 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
103 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
104 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
105 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
106 proper = ?
107 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
108 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)
109 mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
110 mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp)
111 ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
112 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)
113 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
114 limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
115 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX)
116 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp )
117 uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx
118 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
119 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp))
120 ... | yes y = subst (λ k → odef (* x) k) &iso y
121 ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 ) where
122 uf03 : OS TP ∋ ( P ＼ (* x))
123 uf03 = ?
124 uf05 : odef ( P ＼ (* x)) (limit CSX fp)
125 uf05 = ⟪ ? , subst (λ k → ¬ odef (* x) k) ? nxl ⟫
126 uf04 : Neighbor TP (limit CSX fp) (& ( P ＼ (* (limit CSX fp))))
127 uf04 = record { u = & ( P ＼ (* x)) ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ? }
128 uf07 : odef (filter (mf CSX fp)) x
129 uf07 = ?
130 uf06 : odef (filter (mf CSX fp)) (& ( P ＼ (* x)) )
131 uf06 = ?
132 uf08 : (filter (mf CSX fp)) ∋ od∅
133 uf08 = ?
134
135
136 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
137 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
138 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
139 CF : HOD
140 CF = Replace' (filter F) (λ x fx → Cl TP x )
141 CF⊆CS : CF ⊆ CS TP
142 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))
143 ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
144 ufl01 = ?
145 limit : Ordinal
146 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
147 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
148 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
149 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅
150 ufl03 {f} {v} ff nei fv=0 = ?
151 pp : {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
152 pp {v} {x} nei vx z pz = ?
153 ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F
154 ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
155 ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
156 ... | case2 nfv = ?
157
158 -- product topology of compact topology is compact
159
160 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ)
161 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
162 uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F)
163 → UFLP TP F UF
164 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
165 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F)
166 → UFLP TQ F UF
167 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF
168 -- Product of UFL has limit point
169 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F)
170 → UFLP (ProductTopology TP TQ) F UF
171 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where
172 FP : Filter {Power P} {P} (λ x → x)
173 FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
174 ty00 : Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
175 ty00 {x} ⟪ PPx , ppf ⟫ = PPx
176 UFP : ultra-filter FP
177 UFP = record { proper = ? ; ultra = ? }
178 uflp : UFLP TP FP UFP
179 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
180
181 FQ : Filter {Power Q} {Q} (λ x → x)
182 FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
183 ty00 : Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
184 ty00 {x} ⟪ QPx , ppf ⟫ = QPx
185 UFQ : ultra-filter FQ
186 UFQ = record { proper = ? ; ultra = ? }
187 uflq : UFLP TQ FQ UFQ
188 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
189
190 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
191 Pf = ?
192 neip : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q >) v → Neighbor TP p ?
193 neip = ?
194 neiq : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q >) v → Neighbor TQ q ?
195 neiq = ?
196 pq⊆F : {p q : HOD} → Neighbor TP p ? → Neighbor TP q ? → ? ⊆ filter F
197 pq⊆F = ?
198 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F
199 isL {v} npq {x} fx = ?
200
201
202
203
204
205