Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Tychonoff.agda @ 1201:03684784bc5f
...
author | kono |
---|---|
date | Thu, 02 Mar 2023 11:09:02 +0800 |
parents | 42000f20fdbe |
children | d6781ad8149e |
comparison
equal
deleted
inserted
replaced
1200:42000f20fdbe | 1201:03684784bc5f |
---|---|
33 open ODC O | 33 open ODC O |
34 | 34 |
35 open import filter O | 35 open import filter O |
36 open import OPair O | 36 open import OPair O |
37 open import Topology O | 37 open import Topology O |
38 open import maximum-filter O | 38 -- open import maximum-filter O |
39 | 39 |
40 open Filter | 40 open Filter |
41 open Topology | 41 open Topology |
42 | 42 |
43 -- FIP is UFL | 43 -- FIP is UFL |
60 | 60 |
61 UFLP→FIP : {P : HOD} (TP : Topology P) → | 61 UFLP→FIP : {P : HOD} (TP : Topology P) → |
62 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP | 62 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP |
63 UFLP→FIP {P} TP uflp with trio< (& P) o∅ | 63 UFLP→FIP {P} TP uflp with trio< (& P) o∅ |
64 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 64 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
65 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where | 65 ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where |
66 -- P is empty | 66 -- P is empty |
67 fip02 : {x : Ordinal } → ¬ odef P x | 67 fip02 : {x : Ordinal } → ¬ odef P x |
68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) ) | 68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) ) |
69 ... | tri> ¬a ¬b 0<P = record { limit = ? ; is-limit = uf01 } where | 69 fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} → |
70 odef (* X) x → odef (* x) o∅ | |
71 -- empty P case | |
72 -- if 0 < X then 0 < x ∧ P ∋ xfrom fip | |
73 -- if 0 ≡ X then ¬ odef X x | |
74 fip03 {X} CX fip {x} xx with trio< o∅ X | |
75 ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) | |
76 ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where | |
77 0<x : o∅ o< x | |
78 0<x = fip (gi xx ) | |
79 e : HOD -- we have an element of x | |
80 e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
81 xe : odef (* x) (& e) | |
82 xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) | |
83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin | |
84 * X ≡⟨ cong (*) (sym 0=X) ⟩ | |
85 * o∅ ≡⟨ o∅≡od∅ ⟩ | |
86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning | |
87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → UFLP.limit (uflp (F CSX fip) (ultraf CSX fip)) ; is-limit = ? } where | |
70 fip : {X : Ordinal} → * X ⊆ CS TP → Set n | 89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
71 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x | 90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x |
72 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD | 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
73 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) | 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
74 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } | 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
75 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P | 94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
76 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb | 95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
77 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → HOD | 96 nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD |
78 nc = ? | 97 nc {X} CSX fip with trio< o∅ X |
79 N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → odef (N CSX fp) (& (nc CSX fp) ) | 98 ... | tri< 0<X ¬b ¬c = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where |
80 N∋nc = ? | 99 e : HOD -- we have an element of X |
100 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
101 Xe : odef (* X) (& e) | |
102 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
103 ... | tri≈ ¬a b ¬c = od∅ | |
104 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
105 N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc CSX fip) ) | |
106 N∋nc {X} CSX fip with trio< o∅ X | |
107 ... | tri< 0<X ¬b ¬c = record { b = ? ; x = ? ; b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where | |
108 e : HOD -- we have an element of X | |
109 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
110 Xe : odef (* X) (& e) | |
111 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
112 nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) | |
113 ... | tri≈ ¬a b ¬c = ? -- od∅ | |
114 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) | |
81 0<PP : o∅ o< & (Power P) | 115 0<PP : o∅ o< & (Power P) |
82 0<PP = ? | 116 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where |
117 nn00 : odef (Power P) o∅ | |
118 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt | |
119 ... | x<0 = ⊥-elim ( ¬x<0 x<0) | |
83 -- | 120 -- |
84 -- FIP defines a filter | 121 -- FIP defines a filter |
85 -- | 122 -- |
86 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) | 123 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) |
87 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where | 124 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where |
113 proper = ? | 150 proper = ? |
114 -- | 151 -- |
115 -- then we have maximum ultra filter | 152 -- then we have maximum ultra filter |
116 -- | 153 -- |
117 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) | 154 maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) |
118 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) | 155 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) |
119 mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) | 156 mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) |
120 mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp) | 157 mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp) |
121 ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp) | 158 ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp) |
122 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) | 159 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) |
123 -- | 160 -- |
124 -- so i has a limit as a limit of UIP | 161 -- so i has a limit as a limit of UIP |
125 -- | 162 -- |
126 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal | 163 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
127 limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) | 164 limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) |
128 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) | 165 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) |
129 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp ) | 166 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp ) |
130 uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx | 167 uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx |
131 -- | 168 -- |
132 -- the limit is an element of entire elements of X | 169 -- the limit is an limit of entire elements of X |
133 -- | 170 -- |
134 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) | 171 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) |
135 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp)) | 172 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp)) |
136 ... | yes y = subst (λ k → odef (* x) k) &iso y | 173 ... | yes y = subst (λ k → odef (* x) k) &iso y |
137 ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 ) where | 174 ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 ) where |
149 uf08 = ? | 186 uf08 = ? |
150 | 187 |
151 | 188 |
152 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP | 189 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
153 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF | 190 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF |
154 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 | 191 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where |
155 -- | 192 -- |
156 -- take closure of given filter elements | 193 -- take closure of given filter elements |
157 -- | 194 -- |
158 CF : HOD | 195 CF : HOD |
159 CF = Replace (filter F) (λ x → Cl TP x ) | 196 CF = Replace (filter F) (λ x → Cl TP x ) |
166 ufl01 = ? | 203 ufl01 = ? |
167 -- | 204 -- |
168 -- so we have a limit | 205 -- so we have a limit |
169 -- | 206 -- |
170 limit : Ordinal | 207 limit : Ordinal |
171 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 | 208 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 |
172 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit | 209 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit |
173 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 | 210 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 |
174 -- | 211 -- |
175 -- Neigbor of limit ⊆ Filter | 212 -- Neigbor of limit ⊆ Filter |
176 -- | 213 -- |
177 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF which is a closure | 214 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF which is a closure |
178 ufl03 {f} {v} ff nei fv=0 = ? | 215 ufl03 {f} {v} ff nei fv=0 = ? |
191 → UFLP TP F UF | 228 → UFLP TP F UF |
192 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF | 229 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF |
193 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) | 230 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) |
194 → UFLP TQ F UF | 231 → UFLP TQ F UF |
195 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF | 232 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF |
196 -- Product of UFL has limit point | 233 -- Product of UFL has a limit point |
197 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) | 234 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) |
198 → UFLP (ProductTopology TP TQ) F UF | 235 → UFLP (ProductTopology TP TQ) F UF |
199 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where | 236 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where |
200 FP : Filter {Power P} {P} (λ x → x) | 237 FP : Filter {Power P} {P} (λ x → x) |
201 FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where | 238 FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where |