Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 1197:0a88fcd5d1c9
... almost
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 01 Mar 2023 00:37:34 +0900 |
parents | 6216562a2bce |
children | 5223f0b40d91 |
rev | line source |
---|---|
457 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
2 | |
431 | 3 open import Level |
4 open import Ordinals | |
5 module filter {n : Level } (O : Ordinals {n}) where | |
6 | |
7 open import zf | |
8 open import logic | |
9 import OD | |
10 | |
11 open import Relation.Nullary | |
12 open import Data.Empty | |
13 open import Relation.Binary.Core | |
14 open import Relation.Binary.PropositionalEquality | |
1124 | 15 import BAlgebra |
431 | 16 |
1124 | 17 open BAlgebra O |
431 | 18 |
19 open inOrdinal O | |
20 open OD O | |
21 open OD.OD | |
22 open ODAxiom odAxiom | |
23 | |
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 | |
33 import ODC | |
34 open ODC O | |
35 | |
36 open _∧_ | |
37 open _∨_ | |
38 open Bool | |
39 | |
1133 | 40 -- L is a boolean algebra, but we don't assume this explicitly |
41 -- | |
42 -- NEG : {p : HOD} → L ∋ p → L ∋ (P \ p) | |
43 -- CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q ) | |
44 -- | |
431 | 45 -- Kunen p.76 and p.53, we use ⊆ |
1124 | 46 record Filter { L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 47 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
48 filter : HOD |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
49 f⊆L : filter ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
50 filter1 : { p q : HOD } → L ∋ q → filter ∋ p → p ⊆ q → filter ∋ q |
461 | 51 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → L ∋ (p ∩ q) → filter ∋ (p ∩ q) |
431 | 52 |
53 open Filter | |
54 | |
1124 | 55 record prime-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where |
431 | 56 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
57 proper : ¬ (filter F ∋ od∅) |
1157 | 58 prime : {p q : HOD } → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
431 | 59 |
1124 | 60 record ultra-filter { L P : HOD } {LP : L ⊆ Power P} (F : Filter {L} {P} LP) : Set (suc (suc n)) where |
431 | 61 field |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
62 proper : ¬ (filter F ∋ od∅) |
461 | 63 ultra : {p : HOD } → L ∋ p → L ∋ ( P \ p) → ( filter F ∋ p ) ∨ ( filter F ∋ ( P \ p) ) |
431 | 64 |
1124 | 65 ∈-filter : {L P p : HOD} → {LP : L ⊆ Power P} → (F : Filter {L} {P} LP ) → filter F ∋ p → L ∋ p |
1096 | 66 ∈-filter {L} {p} {LP} F lt = ( f⊆L F) lt |
458 | 67 |
1124 | 68 ⊆-filter : {L P p q : HOD } → {LP : L ⊆ Power P } → (F : Filter {L} {P} LP) → L ∋ q → q ⊆ P |
1096 | 69 ⊆-filter {L} {P} {p} {q} {LP} F lt = power→⊆ P q ( LP lt ) |
431 | 70 |
71 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L | |
1096 | 72 ∪-lemma1 {L} {p} {q} lt p∋x = lt (case1 p∋x) |
431 | 73 |
74 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L | |
1096 | 75 ∪-lemma2 {L} {p} {q} lt p∋x = lt (case2 p∋x) |
431 | 76 |
77 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | |
1096 | 78 q∩q⊆q lt = proj1 lt |
431 | 79 |
1140 | 80 ∩→≡1 : {p q : HOD } → p ⊆ q → (q ∩ p) ≡ p |
81 ∩→≡1 {p} {q} p⊆q = ==→o≡ record { eq→ = c00 ; eq← = c01 } where | |
82 c00 : {x : Ordinal} → odef (q ∩ p) x → odef p x | |
83 c00 {x} qpx = proj2 qpx | |
84 c01 : {x : Ordinal} → odef p x → odef (q ∩ p) x | |
85 c01 {x} px = ⟪ p⊆q px , px ⟫ | |
86 | |
87 ∩→≡2 : {p q : HOD } → q ⊆ p → (q ∩ p) ≡ q | |
88 ∩→≡2 {p} {q} q⊆p = ==→o≡ record { eq→ = c00 ; eq← = c01 } where | |
89 c00 : {x : Ordinal} → odef (q ∩ p) x → odef q x | |
90 c00 {x} qpx = proj1 qpx | |
91 c01 : {x : Ordinal} → odef q x → odef (q ∩ p) x | |
92 c01 {x} qx = ⟪ qx , q⊆p qx ⟫ | |
93 | |
431 | 94 open HOD |
95 | |
96 ----- | |
97 -- | |
98 -- ultra filter is prime | |
99 -- | |
100 | |
461 | 101 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) |
102 → ({p : HOD} → L ∋ p → L ∋ (P \ p)) | |
103 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) | |
1124 | 104 → (F : Filter {L} {P} LP) → ultra-filter F → prime-filter F |
1157 | 105 filter-lemma1 {P} {L} LNEG NEG CAP F u = record { |
431 | 106 proper = ultra-filter.proper u |
107 ; prime = lemma3 | |
108 } where | |
1157 | 109 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
110 lemma3 {p} {q} Lp Lq lt with ultra-filter.ultra u Lp (NEG Lp) | |
458 | 111 ... | case1 p∈P = case1 p∈P |
112 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P \ p)} Lq lemma7 lemma8) where | |
113 lemma5 : ((p ∪ q ) ∩ (P \ p)) =h= (q ∩ (P \ p)) | |
431 | 114 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ |
115 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
116 } where | |
458 | 117 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P \ p)) x → odef q x |
431 | 118 lemma4 x lt with proj1 lt |
119 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
120 lemma4 x lt | case2 qx = qx | |
461 | 121 lemma9 : L ∋ ((p ∪ q ) ∩ (P \ p)) |
1157 | 122 lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (CAP Lq (NEG Lp)) |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
123 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P \ p)) |
461 | 124 lemma6 = filter2 F lt ¬p∈P lemma9 |
458 | 125 lemma7 : filter F ∋ (q ∩ (P \ p)) |
126 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6 | |
127 lemma8 : (q ∩ (P \ p)) ⊆ q | |
1124 | 128 lemma8 lt = proj1 lt |
431 | 129 |
130 ----- | |
131 -- | |
1124 | 132 -- if Filter {L} {P} contains L, prime filter is ultra |
431 | 133 -- |
134 | |
461 | 135 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) |
136 → ({p : HOD} → L ∋ p → L ∋ ( P \ p)) | |
1124 | 137 → (F : Filter {L} {P} LP) → filter F ∋ P → prime-filter F → ultra-filter F |
1157 | 138 filter-lemma2 {P} {L} LP NEG F f∋P prime = record { |
458 | 139 proper = prime-filter.proper prime |
1157 | 140 ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (NEG L∋p) (lemma p (p⊆L L∋p )) |
431 | 141 } where |
142 open _==_ | |
459 | 143 p⊆L : {p : HOD} → L ∋ p → p ⊆ P |
1096 | 144 p⊆L {p} lt = power→⊆ P p ( LP lt ) |
459 | 145 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P \ p)) |
146 eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x) | |
147 eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x | |
148 eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
1096 | 149 eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x )) |
459 | 150 eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p ) = proj1 ¬p |
458 | 151 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P \ p)) |
459 | 152 lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P |
431 | 153 |
458 | 154 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 155 field |
156 dense : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
157 d⊆P : dense ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
158 dense-f : {p : HOD} → L ∋ p → HOD |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
159 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
160 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
431 | 161 |
458 | 162 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
431 | 163 field |
164 ideal : HOD | |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
165 i⊆L : ideal ⊆ L |
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
166 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
431 | 167 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
168 | |
169 open Ideal | |
170 | |
1124 | 171 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n |
458 | 172 proper-ideal {L} {P} LP I = ideal I ∋ od∅ |
431 | 173 |
1124 | 174 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n |
458 | 175 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q ) |
431 | 176 |
1131 | 177 open import Relation.Binary.Definitions |
431 | 178 |
461 | 179 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where |
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
180 field |
1124 | 181 genf : Filter {L} {P} LP |
182 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) | |
431 | 183 |
1135 | 184 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where |
478 | 185 field |
1124 | 186 mf : Filter {L} {P} LP |
1136 | 187 F⊆mf : filter F ⊆ filter mf |
478 | 188 proper : ¬ (filter mf ∋ od∅) |
1140 | 189 is-maximum : ( f : Filter {L} {P} LP ) → ¬ (filter f ∋ od∅) → filter F ⊆ filter f → ¬ ( filter mf ⊂ filter f ) |
478 | 190 |
1135 | 191 record Fp {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) (mx : MaximumFilter {L} {P} LP F ) (p x : Ordinal ) : Set n where |
1131 | 192 field |
193 y : Ordinal | |
194 mfy : odef (filter (MaximumFilter.mf mx)) y | |
195 y-p⊂x : ( * y \ * p ) ⊆ * x | |
196 | |
1125 | 197 max→ultra : {L P : HOD} (LP : L ⊆ Power P) |
1127 | 198 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
1136 | 199 → (F0 : Filter {L} {P} LP) → {y : Ordinal } → odef (filter F0) y |
1135 | 200 → (mx : MaximumFilter {L} {P} LP F0 ) → ultra-filter ( MaximumFilter.mf mx ) |
1136 | 201 max→ultra {L} {P} LP CAP F0 {y} mfy mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where |
479 | 202 mf = MaximumFilter.mf mx |
203 ultra : {p : HOD} → L ∋ p → L ∋ (P \ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P \ p)) | |
1131 | 204 ultra {p} Lp Lnp with ODC.∋-p O (filter mf) p |
479 | 205 ... | yes y = case1 y |
1132 | 206 ... | no np = case2 (subst (λ k → k ∋ (P \ p)) F=mf F∋P-p) where |
1129 | 207 F : HOD |
1135 | 208 F = record { od = record { def = λ x → odef L x ∧ Fp {L} {P} LP F0 mx (& p) x } |
1129 | 209 ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } |
1124 | 210 mu01 : {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q |
1130 | 211 mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = mu03 } ⟫ where |
212 mu05 : (* y \ p) ⊆ r | |
1131 | 213 mu05 = subst₂ (λ j k → (* y \ j ) ⊆ k ) *iso *iso y-p⊂x |
1130 | 214 mu04 : (* y \ * (& p)) ⊆ * (& q) |
215 mu04 {x} ⟪ yx , npx ⟫ = subst (λ k → odef k x ) (sym *iso) (r⊆q (mu05 ⟪ yx , (λ px1 → npx (subst (λ k → odef k x) (sym *iso) px1 )) ⟫ ) ) | |
1131 | 216 mu03 : (* y \ * (& p)) ⊆ * (& q) |
217 mu03 = mu04 | |
1125 | 218 mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q) |
1129 | 219 mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ |
1130 | 220 ⟪ Lq , record { y = qy ; mfy = mfqy ; y-p⊂x = qy-p⊂x } ⟫ Lrq = ⟪ Lrq , record { y = & (* qy ∩ * ry) ; mfy = mu20 ; y-p⊂x = mu22 } ⟫ where |
221 mu21 : L ∋ (* qy ∩ * ry) | |
222 mu21 = CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) | |
223 mu20 : odef (filter mf) (& (* qy ∩ * ry)) | |
224 mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry) mu21 | |
225 mu24 : ((* qy ∩ * ry) \ * (& p)) ⊆ (r ∩ q) | |
1131 | 226 mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( ry-p⊂x ⟪ proj2 qry , npx ⟫ ) |
227 , subst (λ k → odef k x) *iso ( qy-p⊂x ⟪ proj1 qry , npx ⟫ ) ⟫ | |
228 mu23 : ((* qy ∩ * ry) \ * (& p) ) ⊆ (r ∩ q) | |
229 mu23 = mu24 | |
230 mu22 : (* (& (* qy ∩ * ry)) \ * (& p)) ⊆ * (& (r ∩ q)) | |
231 mu22 = subst₂ (λ j k → (j \ * (& p)) ⊆ k ) (sym *iso) (sym *iso) mu23 | |
1124 | 232 FisFilter : Filter {L} {P} LP |
1131 | 233 FisFilter = record { filter = F ; f⊆L = λ {x} lt → proj1 lt ; filter1 = mu01 ; filter2 = mu02 } |
1124 | 234 FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx)) x → odef (filter FisFilter ) x |
1129 | 235 FisGreater {x} mfx = ⟪ f⊆L mf mfx , record { y = x ; mfy = mfx ; y-p⊂x = mu03 } ⟫ where |
1131 | 236 mu03 : (* x \ * (& p)) ⊆ * x |
237 mu03 {z} ⟪ xz , _ ⟫ = xz | |
238 F∋P-p : F ∋ (P \ p ) | |
1136 | 239 F∋P-p = ⟪ Lnp , record { y = y ; mfy = mxy ; y-p⊂x = mu30 } ⟫ where |
240 mxy : odef (filter (MaximumFilter.mf mx)) y | |
241 mxy = MaximumFilter.F⊆mf mx mfy | |
242 mu30 : (* y \ * (& p)) ⊆ * (& (P \ p)) | |
1132 | 243 mu30 {z} ⟪ yz , ¬pz ⟫ = subst (λ k → odef k z) (sym *iso) ( ⟪ Pz , (λ pz → ¬pz (subst (λ k → odef k z) (sym *iso) pz )) ⟫ ) where |
244 Pz : odef P z | |
1136 | 245 Pz = LP (f⊆L mf mxy ) _ yz |
1133 | 246 FisProper : ¬ (filter FisFilter ∋ od∅) -- if F contains p, p is in mf which contract np |
247 FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = | |
248 ⊥-elim ( np (filter1 mf Lp (subst (λ k → odef (filter mf) k) (sym &iso) mfz) mu31) ) where | |
249 mu31 : * z ⊆ p | |
250 mu31 {x} zx with ODC.decp O (odef p x) | |
251 ... | yes px = px | |
252 ... | no npx = ⊥-elim ( ¬x<0 (subst (λ k → odef k x) *iso (z-p⊂x ⟪ zx , (λ px → npx (subst (λ k → odef k x) *iso px) ) ⟫ ) ) ) | |
1141
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
253 F0⊆F : filter F0 ⊆ F |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
254 F0⊆F {x} fx = ⟪ f⊆L F0 fx , record { y = _ ; mfy = MaximumFilter.F⊆mf mx fx ; y-p⊂x = mu42 } ⟫ where |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
255 mu42 : (* x \ * (& p)) ⊆ * x |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
256 mu42 {z} ⟪ xz , ¬p ⟫ = xz |
1132 | 257 F=mf : F ≡ filter mf |
258 F=mf with osuc-≡< ( ⊆→o≤ FisGreater ) | |
259 ... | case1 eq = &≡&→≡ (sym eq) | |
1141
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
260 ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper F0⊆F ⟪ lt , FisGreater ⟫ ) |
478 | 261 |
480 | 262 open _==_ |
263 | |
1124 | 264 ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} |
265 → L ∋ p → L ∋ ( P \ p)) | |
266 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | |
1135 | 267 → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP U |
1157 | 268 ultra→max {L} {P} LP NEG CAP U u = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where |
1140 | 269 is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → filter U ⊆ filter F → (U⊂F : filter U ⊂ filter F ) → ⊥ |
270 is-maximum F Prop F⊆U ⟪ U<F , U⊆F ⟫ = Prop f0 where | |
480 | 271 GT : HOD |
1124 | 272 GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where |
273 um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L | |
274 um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) ) | |
480 | 275 GT≠∅ : ¬ (GT =h= od∅) |
1124 | 276 GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where |
277 U≠F : ¬ ( filter U ≡ filter F ) | |
278 U≠F eq = o<¬≡ (cong (&) eq) U<F | |
279 gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x)) | |
480 | 280 gt01 x not = ¬x<0 ( eq→ eq not ) |
281 p : HOD | |
282 p = ODC.minimal O GT GT≠∅ | |
283 ¬U∋p : ¬ ( filter U ∋ p ) | |
284 ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅) | |
1124 | 285 L∋p : L ∋ p |
286 L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅)) | |
287 um00 : ¬ odef (filter U) (& p) | |
288 um00 = proj2 (ODC.x∋minimal O GT GT≠∅) | |
289 L∋-p : L ∋ ( P \ p ) | |
1157 | 290 L∋-p = NEG L∋p |
480 | 291 U∋-p : filter U ∋ ( P \ p ) |
1124 | 292 U∋-p with ultra-filter.ultra u {p} L∋p L∋-p |
480 | 293 ... | case1 ux = ⊥-elim ( ¬U∋p ux ) |
294 ... | case2 u-x = u-x | |
295 F∋p : filter F ∋ p | |
296 F∋p = proj1 (ODC.x∋minimal O GT GT≠∅) | |
297 F∋-p : filter F ∋ ( P \ p ) | |
1096 | 298 F∋-p = U⊆F U∋-p |
480 | 299 f0 : filter F ∋ od∅ |
1124 | 300 f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) ) |
516 | 301 |
1133 | 302 -- if there is a filter , there is a ultra filter under the axiom of choise |
303 -- Zorn Lemma | |
304 | |
1138 | 305 record IsFilter { L P : HOD } (LP : L ⊆ Power P) (filter : Ordinal ) : Set n where |
1133 | 306 field |
307 f⊆L : (* filter) ⊆ L | |
308 filter1 : { p q : Ordinal } → odef L q → odef (* filter) p → (* p) ⊆ (* q) → odef (* filter) q | |
309 filter2 : { p q : Ordinal } → odef (* filter) p → odef (* filter) q → odef L (& ((* p) ∩ (* q))) → odef (* filter) (& ((* p) ∩ (* q))) | |
310 proper : ¬ (odef (* filter ) o∅) | |
1126 | 311 |
1140 | 312 Filter-is-Filter : { L P : HOD } (LP : L ⊆ Power P) → (F : Filter {L} {P} LP) → (proper : ¬ (filter F) ∋ od∅ ) → IsFilter {L} {P} LP (& (filter F)) |
313 Filter-is-Filter {L} {P} LP F proper = record { | |
314 f⊆L = subst (λ k → k ⊆ L ) (sym *iso) (f⊆L F) | |
1141
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
315 ; filter1 = λ {p} {q} Lq Fp p⊆q → subst₂ (λ j k → odef j k ) (sym *iso) &iso |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
316 ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q ) |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
317 ; filter2 = λ {p} {q} Fp Fq Lpq → subst₂ (λ j k → odef j k ) (sym *iso) refl ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) |
e9a05e7c4e35
Maximal Filter and Ultra Filter generation done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1140
diff
changeset
|
318 (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq ) |
1140 | 319 ; proper = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper |
320 } |