Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/Tychonoff.agda @ 1220:a8253c91f630
ZFP distr
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 06 Mar 2023 15:23:17 +0900 |
parents | 91740267e62d |
children | 0e8306b146f6 |
rev | line source |
---|---|
1175 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
431 | 2 open import Level |
3 open import Ordinals | |
1170 | 4 module Tychonoff {n : Level } (O : Ordinals {n}) where |
431 | 5 |
6 open import zf | |
7 open import logic | |
8 open _∧_ | |
9 open _∨_ | |
10 open Bool | |
11 | |
1113
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
12 import OD |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
13 open import Relation.Nullary |
384ba5a3c019
fix Topology definition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1112
diff
changeset
|
14 open import Data.Empty |
431 | 15 open import Relation.Binary.Core |
1143 | 16 open import Relation.Binary.Definitions |
431 | 17 open import Relation.Binary.PropositionalEquality |
1124 | 18 import BAlgebra |
19 open BAlgebra O | |
431 | 20 open inOrdinal O |
21 open OD O | |
22 open OD.OD | |
23 open ODAxiom odAxiom | |
24 import OrdUtil | |
25 import ODUtil | |
26 open Ordinals.Ordinals O | |
27 open Ordinals.IsOrdinals isOrdinal | |
28 open Ordinals.IsNext isNext | |
29 open OrdUtil O | |
30 open ODUtil O | |
31 | |
32 import ODC | |
33 open ODC O | |
34 | |
1102 | 35 open import filter O |
1218 | 36 open import ZProduct O |
1170 | 37 open import Topology O |
1213 | 38 -- open import maximum-filter O |
431 | 39 |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
40 open Filter |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
41 open Topology |
1169 | 42 |
431 | 43 -- FIP is UFL |
44 | |
1159 | 45 -- filter Base |
1205 | 46 record FBase (P : HOD ) (X : Ordinal ) (u : Ordinal) : Set n where |
1153 | 47 field |
1161 | 48 b x : Ordinal |
1155 | 49 b⊆X : * b ⊆ * X |
1161 | 50 sb : Subbase (* b) x |
1158 | 51 u⊆P : * u ⊆ P |
1154 | 52 x⊆u : * x ⊆ * u |
1155 | 53 |
1170 | 54 record UFLP {P : HOD} (TP : Topology P) (F : Filter {Power P} {P} (λ x → x) ) |
55 (ultra : ultra-filter F ) : Set (suc (suc n)) where | |
56 field | |
57 limit : Ordinal | |
58 P∋limit : odef P limit | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
59 is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v) |
1165 | 60 |
1161 | 61 UFLP→FIP : {P : HOD} (TP : Topology P) → |
1169 | 62 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP |
1163 | 63 UFLP→FIP {P} TP uflp with trio< (& P) o∅ |
64 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | |
1201 | 65 ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where |
1163 | 66 -- P is empty |
67 fip02 : {x : Ordinal } → ¬ odef P x | |
1201 | 68 fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) ) |
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 ) | |
1204 | 88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = uf01 } where |
1143 | 89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n |
1187 | 90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x |
1154 | 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD |
1161 | 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) |
1159 | 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } |
1158 | 94 N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P |
1159 | 95 N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb |
1205 | 96 -- filter base is not empty necessary for generating ultra filter |
1204 | 97 nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD |
1205 | 98 nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
99 N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) |
1204 | 100 → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) ) |
1205 | 101 N∋nc {X} 0<X CSX fip = record { b = X ; x = & e ; b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where |
1201 | 102 e : HOD -- we have an element of X |
103 e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
104 Xe : odef (* X) (& e) | |
105 Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
106 nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) |
1205 | 107 nn02 : * (& (nc 0<X CSX fip)) ⊆ P |
108 nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) ) | |
109 | |
1165 | 110 0<PP : o∅ o< & (Power P) |
1201 | 111 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where |
112 nn00 : odef (Power P) o∅ | |
113 nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt | |
114 ... | x<0 = ⊥-elim ( ¬x<0 x<0) | |
1174 | 115 -- |
116 -- FIP defines a filter | |
117 -- | |
1158 | 118 F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x) |
119 F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where | |
120 f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q | |
1161 | 121 f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = |
122 record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → | |
1158 | 123 subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where |
124 f10 : q ⊆ P | |
125 f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) | |
126 f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) | |
127 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 | |
128 p∩q⊆p : * (& (p ∩ q)) ⊆ P | |
129 p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) | |
1159 | 130 Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) |
131 xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) | |
1155 | 132 sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) |
1159 | 133 sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) |
1155 | 134 f20 : * (& Np+Nq) ⊆ * X |
135 f20 {x} npq with subst (λ k → odef k x) *iso npq | |
1159 | 136 ... | case1 np = FBase.b⊆X Np np |
137 ... | case2 nq = FBase.b⊆X Nq nq | |
1155 | 138 f22 : * (& xp∧xq) ⊆ * (& (p ∩ q)) |
1161 | 139 f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq |
1159 | 140 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) |
1174 | 141 -- |
1207 | 142 -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x ) |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
143 -- |
1207 | 144 proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅) |
145 proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where | |
146 x≤0 : x o< osuc o∅ | |
147 x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u)) | |
148 fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x | |
149 fp00 b y b<X (gi by ) = gi ( b<X by ) | |
150 fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz) | |
1174 | 151 -- |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
152 -- then we have maximum ultra filter |
1174 | 153 -- |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
154 maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) |
1213 | 155 maxf {X} 0<X CSX fp = {!!} -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
156 mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
157 mf {X} 0<X CSX fp = MaximumFilter.mf (maxf 0<X CSX fp) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
158 ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp) |
1213 | 159 ultraf {X} 0<X CSX fp = {!!} -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) |
1174 | 160 -- |
161 -- so i has a limit as a limit of UIP | |
162 -- | |
1170 | 163 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal |
1203 | 164 limit {X} CSX fp with trio< o∅ X |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
165 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
166 ... | tri≈ ¬a 0=X ¬c = o∅ |
1203 | 167 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
1174 | 168 -- |
1201 | 169 -- the limit is an limit of entire elements of X |
1174 | 170 -- |
1170 | 171 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) |
1204 | 172 uf01 {X} CSX fp {x} xx with trio< o∅ X |
1206 | 173 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) |
1205 | 174 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx ))) |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
175 ... | tri< 0<X ¬b ¬c with ∨L\X {P} {* x} {UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))} |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
176 (UFLP.P∋limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))) |
1206 | 177 ... | case1 lt = lt -- odef (* x) y |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
178 ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
179 y = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) |
1207 | 180 x⊆P : * x ⊆ P |
181 x⊆P = cs⊆L TP (CSX (subst (λ k → odef (* X) k) (sym &iso) xx)) | |
1206 | 182 uf10 : odef (P \ * x ) y |
183 uf10 = nlxy | |
184 uf03 : Neighbor TP y (& (P \ * x )) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
185 uf03 = record { u = _ ; ou = P\CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
186 ; ux = subst (λ k → odef k y) (sym *iso) uf10 |
1206 | 187 ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz ) |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
188 ; u⊆v = λ x → x } |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
189 uf07 : * (& (* x , * x)) ⊆ * X |
1207 | 190 uf07 {y} lt with subst (λ k → odef k y) *iso lt |
191 ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx | |
192 ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
193 uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
194 uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 |
1207 | 195 ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) ) ; u⊆P = x⊆P ; x⊆u = λ x → x } |
1213 | 196 uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P \ * x )))) |
197 uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P \ * x)} uf03 | |
198 -- uf06 (same as uf061) have yellow if zorn lemma is not imported | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
199 uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P \ * x )) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
200 uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso (UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P \ * x)} uf03 ) |
1206 | 201 uf13 : & ((* x) ∩ (P \ * x )) ≡ o∅ |
1207 | 202 uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) } ) ) where |
203 uf14 : {y : Ordinal} → odef (* x ∩ (P \ * x)) y → odef od∅ y | |
204 uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy ) | |
1206 | 205 uf12 : odef (Power P) (& ((* x) ∩ (P \ * x ))) |
1207 | 206 uf12 z pz with subst (λ k → odef k z) *iso pz |
207 ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
208 uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅ |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
209 uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅)) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
210 ( filter2 (MaximumFilter.mf (maxf 0<X CSX fp)) (subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) (sym &iso) uf05) uf06 uf12 ) |
1142 | 211 |
1208 | 212 x⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → x ⊆ Cl TP x |
213 x⊆Clx {P} TP {x} x<p {y} xy = ⟪ x<p xy , (λ c csc x<c → x<c xy ) ⟫ | |
214 P⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → Cl TP x ⊆ P | |
215 P⊆Clx {P} TP {x} x<p {y} xy = proj1 xy | |
216 | |
1158 | 217 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP |
1169 | 218 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
219 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
1209 | 220 ; P∋limit = ufl10 ; is-limit = ufl00 } where |
221 F∋P : odef (filter F) (& P) | |
222 F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) | |
223 ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) | |
224 ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where | |
225 fl20 : (P \ Ord o∅) =h= P | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
226 fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } |
1209 | 227 0<P : o∅ o< & P |
228 0<P with trio< o∅ (& P) | |
229 ... | tri< a ¬b ¬c = a | |
230 ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋P) ) | |
231 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
1174 | 232 -- |
233 -- take closure of given filter elements | |
234 -- | |
1160 | 235 CF : HOD |
1188 | 236 CF = Replace (filter F) (λ x → Cl TP x ) |
1160 | 237 CF⊆CS : CF ⊆ CS TP |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
238 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)) |
1174 | 239 -- |
240 -- it is set of closed set and has FIP ( F is proper ) | |
241 -- | |
1208 | 242 ufl08 : {z : Ordinal} → odef (Power P) (& (Cl TP (* z))) |
243 ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw | |
244 ... | t = proj1 t | |
245 fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x | |
246 fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz ) | |
247 F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x | |
248 F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where | |
249 ufl09 : * z ⊆ P | |
250 ufl09 {y} zy = f⊆L F az _ zy | |
251 ufl07 : odef (filter F) x | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
252 ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 ) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
253 (subst (λ k → odef (filter F) k) (sym &iso) az) |
1208 | 254 (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) )) |
255 F∋sb (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx)) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
256 (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
257 (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) ))) |
1187 | 258 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x |
1208 | 259 ufl01 {x} sb = ufl04 where |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
260 ufl04 : o∅ o< x |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
261 ufl04 with trio< o∅ x |
1208 | 262 ... | tri< a ¬b ¬c = a |
263 ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) ( | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
264 begin |
1208 | 265 x ≡⟨ sym b ⟩ |
266 o∅ ≡⟨ sym ord-od∅ ⟩ | |
267 & od∅ ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) )) where open ≡-Reasoning | |
268 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
1209 | 269 ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01) |
270 ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11 where | |
271 ufl11 : odef (* (& CF)) (& P) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
272 ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP))) } |
1174 | 273 -- |
274 -- so we have a limit | |
275 -- | |
1170 | 276 limit : Ordinal |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
277 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
1170 | 278 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
279 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 |
1174 | 280 -- |
281 -- Neigbor of limit ⊆ Filter | |
282 -- | |
1210 | 283 -- if odef (* X) x, Cl TP x contains limit (ufl02) |
284 -- in (nei : Neighbor TP limit v) , there is an open Set u which contains the limit | |
285 -- F contains u or P \ u because F is ultra | |
286 -- if F ∋ u, then F ∋ v from u ⊆ v which is a propetery of Neighbor | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
287 -- if F ∋ P \ u, it is a closed set (Cl (P \ u) ≡ P \ u) and it does not contains the limit |
1210 | 288 -- this contradicts ufl02 |
289 pp : {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei)) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
290 pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
291 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
292 ufl00 : {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
293 ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei )) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
294 ... | case1 fu = subst (λ k → odef (filter F) k) &iso |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
295 ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px) fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
296 u = * (Neighbor.u nei) |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
297 px : Power P ∋ * v |
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
298 px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz ) |
1210 | 299 ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where |
300 u = * (Neighbor.u nei) | |
301 P\u : HOD | |
302 P\u = P \ u | |
303 P\u∋limit : odef P\u limit | |
304 P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where | |
305 ufl04 : & P\u ≡ & (Cl TP (* (& P\u))) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
306 ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) |
1210 | 307 (CS∋x→Clx=x TP (P\OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))))) |
308 ufl03 : odef CF (& P\u ) | |
309 ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 } | |
310 ¬P\u∋limit : ¬ odef P\u limit | |
311 ¬P\u∋limit ⟪ Pl , nul ⟫ = nul ( Neighbor.ux nei ) | |
1163 | 312 |
1124 | 313 -- product topology of compact topology is compact |
431 | 314 |
1218 | 315 import Axiom.Extensionality.Propositional |
316 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m | |
317 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
318 | |
319 | |
1142 | 320 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) |
1158 | 321 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where |
1169 | 322 uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F) |
323 → UFLP TP F UF | |
324 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF | |
325 uflQ : (F : Filter {Power Q} {Q} (λ x → x)) (UF : ultra-filter F) | |
326 → UFLP TQ F UF | |
327 uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF | |
1201 | 328 -- Product of UFL has a limit point |
1169 | 329 uflPQ : (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) |
330 → UFLP (ProductTopology TP TQ) F UF | |
331 uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where | |
1213 | 332 F∋PQ : odef (filter F) (& (ZFP P Q)) |
333 F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) | |
334 ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) | |
335 ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where | |
336 fl20 : (ZFP P Q \ Ord o∅) =h= ZFP P Q | |
337 fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } | |
1218 | 338 0<PQ : o∅ o< & (ZFP P Q) |
339 0<PQ with trio< o∅ (& (ZFP P Q)) | |
1213 | 340 ... | tri< a ¬b ¬c = a |
341 ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) ) | |
342 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
1218 | 343 apq : HOD |
344 apq = ODC.minimal O (ZFP P Q) (0<P→ne 0<PQ) | |
345 is-apq : ZFP P Q ∋ apq | |
346 is-apq = ODC.x∋minimal O (ZFP P Q) (0<P→ne 0<PQ) | |
347 ap : odef P ( zπ1 is-apq ) | |
348 ap = zp1 is-apq | |
349 aq : odef Q ( zπ2 is-apq ) | |
350 aq = zp2 is-apq | |
1213 | 351 isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q |
352 isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q | |
353 F⊆pxq : {x : HOD } → filter F ∋ x → x ⊆ ZFP P Q | |
354 F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy) | |
1216 | 355 fx→px : {x : HOD } → filter F ∋ x → HOD |
356 fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) | |
1217 | 357 fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋ ZFP p Q ) → fx→px fp ≡ p |
358 fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where | |
359 ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) | |
360 ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz )) | |
361 ty32 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a | |
362 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where | |
363 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a | |
364 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
365 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
1216 | 366 ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x |
1217 | 367 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef p k) a=x pz where |
1216 | 368 ty24 : * x ≡ * a |
369 ty24 = begin | |
1217 | 370 * x ≡⟨ cong (*) x=ψz ⟩ |
371 _ ≡⟨ *iso ⟩ | |
372 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 pz qz) ⟩ | |
373 * a ∎ where open ≡-Reasoning | |
374 a=x : a ≡ x | |
375 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) | |
376 ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x | |
377 ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where | |
378 ty12 : * x ≡ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) | |
379 ty12 = begin | |
380 * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩ | |
381 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning | |
1218 | 382 |
383 | |
1213 | 384 FPSet : HOD |
385 FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))) | |
1215 | 386 FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋ ZFP q Q → FPSet ∋ q |
1217 | 387 FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where |
1218 | 388 -- brain damaged one |
389 ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } → | |
390 * (zπ1 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ1 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) | |
391 ty11 {y} {xy} = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where | |
392 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy | |
393 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) | |
1217 | 394 ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q |
395 ty10 = begin | |
1218 | 396 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) |
397 ≡⟨ | |
398 cong (λ k → Replace' (* (& (ZFP q Q))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) | |
399 ⟩ | |
400 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) | |
401 ≡⟨ Replace'-iso _ ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ⟩ | |
1217 | 402 Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ |
1218 | 403 fx→px fq ≡⟨ fx→px1 aq fq ⟩ |
1217 | 404 q ∎ where open ≡-Reasoning |
1213 | 405 FPSet⊆PP : FPSet ⊆ Power P |
406 FPSet⊆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 | |
407 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } | |
408 = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) | |
409 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) | |
1169 | 410 FP : Filter {Power P} {P} (λ x → x) |
1218 | 411 FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where |
1213 | 412 ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q |
1215 | 413 ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 ) |
414 where | |
1213 | 415 -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter.Filter.filter F)) (sym &iso) fx) xy)) |
416 -- x = ( px , qx ) , px ⊆ q | |
417 ty03 : Power (ZFP P Q) ∋ ZFP q Q | |
418 ty03 z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) | |
419 p⊆P : p ⊆ P | |
420 p⊆P {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw | |
421 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) | |
422 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) | |
1215 | 423 q⊆P : q ⊆ P |
424 q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) | |
1213 | 425 x⊆pxq : * x ⊆ ZFP p Q |
1214 | 426 x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw |
427 ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where | |
1217 | 428 ty21 : ZFProduct P Q (& (* (& < * a , * b >))) |
429 ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) | |
430 ty32 : ZFProduct P Q (& (* (& < * a , * b >))) | |
431 ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx) | |
432 (& (* (& < * a , * b >))) (subst (λ k → odef k | |
433 (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) | |
1214 | 434 ty07 : odef (* x) (& < * a , * b >) |
435 ty07 = xw | |
436 ty08 : odef p a | |
437 ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) | |
1217 | 438 record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where |
439 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a | |
440 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) | |
441 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) | |
1213 | 442 ty05 : filter F ∋ ZFP p Q |
443 ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq | |
444 ty06 : ZFP p Q ⊆ ZFP q Q | |
445 ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq | |
1215 | 446 ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q |
447 ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq | |
1218 | 448 ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q) |
1219 | 449 ty02 {p} {q} record { z = zp ; az = azp ; x=ψz = x=ψzp } record { z = zq ; az = azq ; x=ψz = x=ψzq } Ppq |
450 = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where | |
1220 | 451 x⊆pxq : * ? ⊆ ZFP p Q |
452 x⊆pxq = ? | |
453 ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q) | |
454 ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso ty55) (ab-pair ty551 ty552 ) where | |
455 ty55 : odef (ZFP (p ∩ q) Q) z | |
456 ty55 = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz | |
457 ty551 : odef P (zπ1 ty55) | |
458 ty551 = ? | |
459 ty552 : odef Q (zπ2 ty55) | |
460 ty552 = ? | |
461 ty53 : filter F ∋ ZFP p Q | |
462 ty53 = filter1 F (λ z wz → isP→PxQ ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq | |
463 ty52 : filter F ∋ ZFP q Q | |
1219 | 464 ty52 = ? |
465 ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q ) | |
1220 | 466 ty51 = filter2 F ty53 ty52 ty54 |
1219 | 467 ty50 : filter F ∋ ZFP (p ∩ q) Q |
1220 | 468 ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 |
1219 | 469 |
1213 | 470 |
1161 | 471 UFP : ultra-filter FP |
1213 | 472 UFP = record { proper = {!!} ; ultra = {!!} } |
1169 | 473 uflp : UFLP TP FP UFP |
474 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP | |
1154 | 475 |
1169 | 476 FQ : Filter {Power Q} {Q} (λ x → x) |
1218 | 477 FQ = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = {!!} } |
1166 | 478 UFQ : ultra-filter FQ |
1213 | 479 UFQ = record { proper = {!!} ; ultra = {!!} } |
1169 | 480 uflq : UFLP TQ FQ UFQ |
481 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ | |
1154 | 482 |
1166 | 483 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
1213 | 484 Pf = {!!} |
485 pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → {!!} ⊆ filter F | |
486 pq⊆F = {!!} | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
487 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v |
1213 | 488 isL {v} npq = {!!} where |
1172 | 489 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) |
490 bpq = Neighbor.ou npq (Neighbor.ux npq) | |
491 pqb : Subbase (pbase TP TQ) (Base.b bpq ) | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
492 pqb = Base.sb bpq |
1173 | 493 pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq ) |
494 pqb⊆opq = Base.b⊆u bpq | |
495 base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → * b ⊆ filter F | |
496 base⊆F (gi (case1 px)) b⊆u {z} bz = fz where | |
497 -- F contains no od∅, because it projection contains no od∅ | |
498 -- x is an element of BaseP, which is a subset of Neighbor npq | |
499 -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp) | |
500 -- BaseP ∩ F is not empty | |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
501 -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , |
1218 | 502 il1 : odef (Power P) z ∧ ? -- ZFPproj1 (filter F) z |
1213 | 503 il1 = {!!} -- UFLP.is-limit uflp ? bz |
1173 | 504 nei1 : HOD |
1218 | 505 nei1 = ? -- ZFPproj1 (* (Neighbor.u npq)) (Power P) (Power Q) |
1173 | 506 plimit : Ordinal |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
507 plimit = UFLP.limit uflp |
1173 | 508 nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b |
1213 | 509 nproper = {!!} |
1173 | 510 b∋z : odef nei1 z |
1213 | 511 b∋z = {!!} |
1173 | 512 bp : BaseP {P} TP Q z |
1213 | 513 bp = record { p = {!!} ; op = {!!} ; prod = {!!} } |
1211
f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1210
diff
changeset
|
514 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F |
1213 | 515 neip = {!!} |
1173 | 516 il2 : * z ⊆ ZFP (Power P) (Power Q) |
1213 | 517 il2 = {!!} |
518 il3 : filter F ∋ {!!} | |
519 il3 = {!!} | |
1173 | 520 fz : odef (filter F) z |
1213 | 521 fz = subst (λ k → odef (filter F) k) &iso (filter1 F {!!} {!!} {!!}) |
522 base⊆F (gi (case2 qx)) b⊆u {z} bz = {!!} | |
523 base⊆F (g∩ b1 b2) b⊆u {z} bz = {!!} | |
1154 | 524 |
1170 | 525 |
526 | |
527 | |
528 | |
529 |