Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate src/filter.agda @ 1138:dd18bb8d2893
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 13 Jan 2023 13:03:45 +0900 |
| parents | d618788852e5 |
| children | 4517d0721b59 |
| 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∅) |
| 461 | 58 prime : {p q : HOD } → L ∋ p → L ∋ q → L ∋ (p ∪ 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 |
| 80 open HOD | |
| 81 | |
| 82 ----- | |
| 83 -- | |
| 84 -- ultra filter is prime | |
| 85 -- | |
| 86 | |
| 461 | 87 filter-lemma1 : {P L : HOD} → (LP : L ⊆ Power P) |
| 88 → ({p : HOD} → L ∋ p → L ∋ (P ＼ p)) | |
| 89 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) | |
| 1124 | 90 → (F : Filter {L} {P} LP) → ultra-filter F → prime-filter F |
| 461 | 91 filter-lemma1 {P} {L} LP NG IN F u = record { |
| 431 | 92 proper = ultra-filter.proper u |
| 93 ; prime = lemma3 | |
| 94 } where | |
| 461 | 95 lemma3 : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q) → filter F ∋ (p ∪ q) → ( filter F ∋ p ) ∨ ( filter F ∋ q ) |
| 96 lemma3 {p} {q} Lp Lq _ lt with ultra-filter.ultra u Lp (NG Lp) | |
| 458 | 97 ... | case1 p∈P = case1 p∈P |
| 98 ... | case2 ¬p∈P = case2 (filter1 F {q ∩ (P ＼ p)} Lq lemma7 lemma8) where | |
| 99 lemma5 : ((p ∪ q ) ∩ (P ＼ p)) =h= (q ∩ (P ＼ p)) | |
| 431 | 100 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫ |
| 101 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫ | |
| 102 } where | |
| 458 | 103 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (P ＼ p)) x → odef q x |
| 431 | 104 lemma4 x lt with proj1 lt |
| 105 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) | |
| 106 lemma4 x lt | case2 qx = qx | |
| 461 | 107 lemma9 : L ∋ ((p ∪ q ) ∩ (P ＼ p)) |
| 108 lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (IN Lq (NG Lp)) | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
109 lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p)) |
| 461 | 110 lemma6 = filter2 F lt ¬p∈P lemma9 |
| 458 | 111 lemma7 : filter F ∋ (q ∩ (P ＼ p)) |
| 112 lemma7 = subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6 | |
| 113 lemma8 : (q ∩ (P ＼ p)) ⊆ q | |
| 1124 | 114 lemma8 lt = proj1 lt |
| 431 | 115 |
| 116 ----- | |
| 117 -- | |
| 1124 | 118 -- if Filter {L} {P} contains L, prime filter is ultra |
| 431 | 119 -- |
| 120 | |
| 461 | 121 filter-lemma2 : {P L : HOD} → (LP : L ⊆ Power P) |
| 122 → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) | |
| 1124 | 123 → (F : Filter {L} {P} LP) → filter F ∋ P → prime-filter F → ultra-filter F |
| 459 | 124 filter-lemma2 {P} {L} LP Lm F f∋P prime = record { |
| 458 | 125 proper = prime-filter.proper prime |
| 1096 | 126 ; ultra = λ {p} L∋p _ → prime-filter.prime prime L∋p (Lm L∋p) (lemma10 L∋p ((f⊆L F) f∋P) ) (lemma p (p⊆L L∋p )) |
| 431 | 127 } where |
| 128 open _==_ | |
| 459 | 129 p⊆L : {p : HOD} → L ∋ p → p ⊆ P |
| 1096 | 130 p⊆L {p} lt = power→⊆ P p ( LP lt ) |
| 459 | 131 p+1-p=1 : {p : HOD} → p ⊆ P → P =h= (p ∪ (P ＼ p)) |
| 132 eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x) | |
| 133 eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x | |
| 134 eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫ | |
| 1096 | 135 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 | 136 eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p ) = proj1 ¬p |
| 458 | 137 lemma : (p : HOD) → p ⊆ P → filter F ∋ (p ∪ (P ＼ p)) |
| 459 | 138 lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P |
| 461 | 139 lemma10 : {p : HOD} → L ∋ p → L ∋ P → L ∋ (p ∪ (P ＼ p)) |
| 140 lemma10 {p} L∋p lt = subst (λ k → L ∋ k ) (==→o≡ (p+1-p=1 {p} (p⊆L L∋p))) lt | |
| 431 | 141 |
| 458 | 142 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
| 431 | 143 field |
| 144 dense : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
145 d⊆P : dense ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
146 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
|
147 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
|
148 dense-p : { p : HOD} → (lt : L ∋ p) → (dense-f lt) ⊆ p |
| 431 | 149 |
| 458 | 150 record Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where |
| 431 | 151 field |
| 152 ideal : HOD | |
|
456
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
153 i⊆L : ideal ⊆ L |
|
9207b0c3cfe9
fix filter on subset of Power P
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
455
diff
changeset
|
154 ideal1 : { p q : HOD } → L ∋ q → ideal ∋ p → q ⊆ p → ideal ∋ q |
| 431 | 155 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) |
| 156 | |
| 157 open Ideal | |
| 158 | |
| 1124 | 159 proper-ideal : {L P : HOD} → (LP : L ⊆ Power P) → (P : Ideal {L} {P} LP ) → {p : HOD} → Set n |
| 458 | 160 proper-ideal {L} {P} LP I = ideal I ∋ od∅ |
| 431 | 161 |
| 1124 | 162 prime-ideal : {L P : HOD} → (LP : L ⊆ Power P) → Ideal {L} {P} LP → ∀ {p q : HOD } → Set n |
| 458 | 163 prime-ideal {L} {P} LP I {p} {q} = ideal I ∋ ( p ∩ q) → ( ideal I ∋ p ) ∨ ( ideal I ∋ q ) |
| 431 | 164 |
| 1131 | 165 open import Relation.Binary.Definitions |
| 431 | 166 |
| 461 | 167 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
|
168 field |
| 1124 | 169 genf : Filter {L} {P} LP |
| 170 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) | |
| 431 | 171 |
| 1135 | 172 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where |
| 478 | 173 field |
| 1124 | 174 mf : Filter {L} {P} LP |
| 1136 | 175 F⊆mf : filter F ⊆ filter mf |
| 478 | 176 proper : ¬ (filter mf ∋ od∅) |
| 1124 | 177 is-maximum : ( f : Filter {L} {P} LP ) → ¬ (filter f ∋ od∅) → ¬ ( filter mf ⊂ filter f ) |
| 478 | 178 |
| 1135 | 179 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 | 180 field |
| 181 y : Ordinal | |
| 182 mfy : odef (filter (MaximumFilter.mf mx)) y | |
| 183 y-p⊂x : ( * y ＼ * p ) ⊆ * x | |
| 184 | |
| 1125 | 185 max→ultra : {L P : HOD} (LP : L ⊆ Power P) |
| 1127 | 186 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
| 1136 | 187 → (F0 : Filter {L} {P} LP) → {y : Ordinal } → odef (filter F0) y |
| 1135 | 188 → (mx : MaximumFilter {L} {P} LP F0 ) → ultra-filter ( MaximumFilter.mf mx ) |
| 1136 | 189 max→ultra {L} {P} LP CAP F0 {y} mfy mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where |
| 479 | 190 mf = MaximumFilter.mf mx |
| 191 ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p)) | |
| 1131 | 192 ultra {p} Lp Lnp with ODC.∋-p O (filter mf) p |
| 479 | 193 ... | yes y = case1 y |
| 1132 | 194 ... | no np = case2 (subst (λ k → k ∋ (P ＼ p)) F=mf F∋P-p) where |
| 1129 | 195 F : HOD |
| 1135 | 196 F = record { od = record { def = λ x → odef L x ∧ Fp {L} {P} LP F0 mx (& p) x } |
| 1129 | 197 ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } |
| 1124 | 198 mu01 : {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q |
| 1130 | 199 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 |
| 200 mu05 : (* y ＼ p) ⊆ r | |
| 1131 | 201 mu05 = subst₂ (λ j k → (* y ＼ j ) ⊆ k ) *iso *iso y-p⊂x |
| 1130 | 202 mu04 : (* y ＼ * (& p)) ⊆ * (& q) |
| 203 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 | 204 mu03 : (* y ＼ * (& p)) ⊆ * (& q) |
| 205 mu03 = mu04 | |
| 1125 | 206 mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q) |
| 1129 | 207 mu02 {r} {q} ⟪ Lr , record { y = ry ; mfy = mfry ; y-p⊂x = ry-p⊂x } ⟫ |
| 1130 | 208 ⟪ 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 |
| 209 mu21 : L ∋ (* qy ∩ * ry) | |
| 210 mu21 = CAP (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfqy)) (subst (λ k → odef L k ) (sym &iso) (f⊆L mf mfry)) | |
| 211 mu20 : odef (filter mf) (& (* qy ∩ * ry)) | |
| 212 mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry) mu21 | |
| 213 mu24 : ((* qy ∩ * ry) ＼ * (& p)) ⊆ (r ∩ q) | |
| 1131 | 214 mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( ry-p⊂x ⟪ proj2 qry , npx ⟫ ) |
| 215 , subst (λ k → odef k x) *iso ( qy-p⊂x ⟪ proj1 qry , npx ⟫ ) ⟫ | |
| 216 mu23 : ((* qy ∩ * ry) ＼ * (& p) ) ⊆ (r ∩ q) | |
| 217 mu23 = mu24 | |
| 218 mu22 : (* (& (* qy ∩ * ry)) ＼ * (& p)) ⊆ * (& (r ∩ q)) | |
| 219 mu22 = subst₂ (λ j k → (j ＼ * (& p)) ⊆ k ) (sym *iso) (sym *iso) mu23 | |
| 1124 | 220 FisFilter : Filter {L} {P} LP |
| 1131 | 221 FisFilter = record { filter = F ; f⊆L = λ {x} lt → proj1 lt ; filter1 = mu01 ; filter2 = mu02 } |
| 1124 | 222 FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx)) x → odef (filter FisFilter ) x |
| 1129 | 223 FisGreater {x} mfx = ⟪ f⊆L mf mfx , record { y = x ; mfy = mfx ; y-p⊂x = mu03 } ⟫ where |
| 1131 | 224 mu03 : (* x ＼ * (& p)) ⊆ * x |
| 225 mu03 {z} ⟪ xz , _ ⟫ = xz | |
| 226 F∋P-p : F ∋ (P ＼ p ) | |
| 1136 | 227 F∋P-p = ⟪ Lnp , record { y = y ; mfy = mxy ; y-p⊂x = mu30 } ⟫ where |
| 228 mxy : odef (filter (MaximumFilter.mf mx)) y | |
| 229 mxy = MaximumFilter.F⊆mf mx mfy | |
| 230 mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p)) | |
| 1132 | 231 mu30 {z} ⟪ yz , ¬pz ⟫ = subst (λ k → odef k z) (sym *iso) ( ⟪ Pz , (λ pz → ¬pz (subst (λ k → odef k z) (sym *iso) pz )) ⟫ ) where |
| 232 Pz : odef P z | |
| 1136 | 233 Pz = LP (f⊆L mf mxy ) _ yz |
| 1133 | 234 FisProper : ¬ (filter FisFilter ∋ od∅) -- if F contains p, p is in mf which contract np |
| 235 FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = | |
| 236 ⊥-elim ( np (filter1 mf Lp (subst (λ k → odef (filter mf) k) (sym &iso) mfz) mu31) ) where | |
| 237 mu31 : * z ⊆ p | |
| 238 mu31 {x} zx with ODC.decp O (odef p x) | |
| 239 ... | yes px = px | |
| 240 ... | no npx = ⊥-elim ( ¬x<0 (subst (λ k → odef k x) *iso (z-p⊂x ⟪ zx , (λ px → npx (subst (λ k → odef k x) *iso px) ) ⟫ ) ) ) | |
| 1132 | 241 mu40 = (MaximumFilter.is-maximum mx) |
| 242 F=mf : F ≡ filter mf | |
| 243 F=mf with osuc-≡< ( ⊆→o≤ FisGreater ) | |
| 244 ... | case1 eq = &≡&→≡ (sym eq) | |
| 245 ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper ⟪ lt , FisGreater ⟫ ) | |
| 478 | 246 |
| 480 | 247 open _==_ |
| 248 | |
| 1124 | 249 ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} |
| 250 → L ∋ p → L ∋ ( P ＼ p)) | |
| 251 → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | |
| 1135 | 252 → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP U |
| 1136 | 253 ultra→max {L} {P} LP NG CAP U u = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where |
| 1124 | 254 is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U ⊂ filter F ) → ⊥ |
| 255 is-maximum F Prop ⟪ U<F , U⊆F ⟫ = Prop f0 where | |
| 480 | 256 GT : HOD |
| 1124 | 257 GT = record { od = record { def = λ x → odef (filter F) x ∧ (¬ odef (filter U) x) } ; odmax = & L ; <odmax = um02 } where |
| 258 um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L | |
| 259 um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) ) | |
| 480 | 260 GT≠∅ : ¬ (GT =h= od∅) |
| 1124 | 261 GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where |
| 262 U≠F : ¬ ( filter U ≡ filter F ) | |
| 263 U≠F eq = o<¬≡ (cong (&) eq) U<F | |
| 264 gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x)) | |
| 480 | 265 gt01 x not = ¬x<0 ( eq→ eq not ) |
| 266 p : HOD | |
| 267 p = ODC.minimal O GT GT≠∅ | |
| 268 ¬U∋p : ¬ ( filter U ∋ p ) | |
| 269 ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅) | |
| 1124 | 270 L∋p : L ∋ p |
| 271 L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅)) | |
| 272 um00 : ¬ odef (filter U) (& p) | |
| 273 um00 = proj2 (ODC.x∋minimal O GT GT≠∅) | |
| 274 L∋-p : L ∋ ( P ＼ p ) | |
| 275 L∋-p = NG L∋p | |
| 480 | 276 U∋-p : filter U ∋ ( P ＼ p ) |
| 1124 | 277 U∋-p with ultra-filter.ultra u {p} L∋p L∋-p |
| 480 | 278 ... | case1 ux = ⊥-elim ( ¬U∋p ux ) |
| 279 ... | case2 u-x = u-x | |
| 280 F∋p : filter F ∋ p | |
| 281 F∋p = proj1 (ODC.x∋minimal O GT GT≠∅) | |
| 282 F∋-p : filter F ∋ ( P ＼ p ) | |
| 1096 | 283 F∋-p = U⊆F U∋-p |
| 480 | 284 f0 : filter F ∋ od∅ |
| 1124 | 285 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 | 286 |
| 1133 | 287 -- if there is a filter , there is a ultra filter under the axiom of choise |
| 288 -- Zorn Lemma | |
| 289 | |
| 516 | 290 import zorn |
| 1126 | 291 |
| 292 open import Relation.Binary | |
| 293 | |
| 294 PO : IsStrictPartialOrder _≡_ _⊂_ | |
| 295 PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | |
| 296 ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c} | |
| 1133 | 297 ; irrefl = λ x=y x<y → o<¬≡ (cong (&) x=y) (proj1 x<y) |
| 298 ; <-resp-≈ = record { fst = ( λ {x} {y} {y1} y=y1 xy1 → subst (λ k → x ⊂ k) y=y1 xy1 ) | |
| 299 ; snd = (λ {x} {x1} {y} x=x1 x1y → subst (λ k → k ⊂ x) x=x1 x1y ) } } | |
| 1126 | 300 |
| 301 open zorn O _⊂_ PO | |
| 574 | 302 |
| 303 open import Relation.Binary.Structures | |
| 481 | 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 |
| 1133 | 312 -- all filter contains F |
| 313 F⊆X : { L P : HOD } (LP : L ⊆ Power P) → Filter {L} {P} LP → HOD | |
| 1138 | 314 F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x) } ; odmax = osuc (& L) |
| 1133 | 315 ; <odmax = λ {x} lt → fx00 lt } where |
| 1138 | 316 fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L) |
| 317 fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt )) ) | |
| 503 | 318 |
| 1134 | 319 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) |
| 1136 | 320 → (F : Filter {L} {P} LP) → o∅ o< & L → {y : Ordinal } → odef (filter F) y → (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F |
| 1138 | 321 F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = ? |
| 322 ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf) ; is-maximum = {!!} } where | |
| 1133 | 323 FX : HOD |
| 324 FX = F⊆X {L} {P} LP F | |
| 1137 | 325 oF = & (filter F) |
| 326 mf11 : { p q : Ordinal } → odef L q → odef (* oF) p → (* p) ⊆ (* q) → odef (* oF) q | |
| 327 mf11 {p} {q} Lq Fp p⊆q = subst₂ (λ j k → odef j k ) (sym *iso) &iso ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) | |
| 328 (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q ) | |
| 329 mf12 : { p q : Ordinal } → odef (* oF) p → odef (* oF) q → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q))) | |
| 330 mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) | |
| 331 ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq) | |
| 1138 | 332 FX∋F : odef FX (& (filter F)) |
| 1137 | 333 FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 |
| 334 ; proper = subst₂ (λ j k → ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop } | |
| 335 , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ | |
| 1133 | 336 SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B |
| 1138 | 337 SUP⊆ B B⊆FX OB with trio< (& B) o∅ |
| 338 ... | tri< a ¬b ¬c = ⊥-elim (¬x<0 a ) | |
| 339 ... | tri≈ ¬a b ¬c = record { sup = filter F ; isSUP = record { ax = FX∋F ; x≤sup = λ {y} zy → ⊥-elim (o<¬≡ (sym b) (∈∅< zy)) } } | |
| 340 ... | tri> ¬a ¬b 0<B = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ? } } where | |
| 341 mf20 : HOD | |
| 342 mf20 = ODC.minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
| 343 mf18 : odef B (& mf20 ) | |
| 344 mf18 = ODC.x∋minimal O B (λ eq → (o<¬≡ (cong (&) (sym (==→o≡ eq))) (subst (λ k → k o< & B) (sym ord-od∅) 0<B ))) | |
| 1137 | 345 mf16 : Union B ⊆ L |
| 1138 | 346 mf16 record { owner = b ; ao = Bb ; ox = bx } = IsFilter.f⊆L ( proj1 ( B⊆FX Bb )) bx |
| 1137 | 347 mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q |
| 348 mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp | |
| 349 ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) | |
| 1138 | 350 record { owner = owner ; ao = ao ; ox = IsFilter.filter1 mf30 Lq ox p⊆q } where |
| 351 mf30 : IsFilter {L} {P} LP owner | |
| 352 mf30 = proj1 ( B⊆FX ao ) | |
| 353 mf31 : {p q : Ordinal} → odef (* (& (Union B))) p → odef (* (& (Union B))) q → odef L (& ((* p) ∩ (* q))) → odef (* (& (Union B))) (& ((* p) ∩ (* q))) | |
| 354 mf31 {p} {q} bp bq Lpq with subst (λ k → odef k p ) *iso bp | subst (λ k → odef k q ) *iso bq | |
| 355 ... | record { owner = bp ; ao = Bbp ; ox = bbp } | record { owner = bq ; ao = Bbq ; ox = bbq } | |
| 356 with OB (subst (λ k → odef B k) (sym &iso) Bbp) (subst (λ k → odef B k) (sym &iso) Bbq) | |
| 357 ... | tri< bp⊂bq ¬b ¬c = ? | |
| 358 ... | tri≈ ¬a bq=bp ¬c = ? | |
| 359 ... | tri> ¬a ¬b bq⊂bp = ? | |
| 360 mf14 : IsFilter LP (& (Union B)) | |
| 361 mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = mf31 ; proper = ? } | |
| 1137 | 362 mf15 : filter F ⊆ Union B |
| 1138 | 363 mf15 {x} Fx = record { owner = & mf20 ; ao = mf18 ; ox = subst (λ k → odef k x) (sym *iso) (mf22 Fx) } where |
| 364 mf22 : odef (filter F) x → odef mf20 x | |
| 365 mf22 Fx = subst (λ k → odef k x) *iso ( proj2 (B⊆FX mf18) Fx ) | |
| 1137 | 366 mf13 : odef FX (& (Union B)) |
| 367 mf13 = ⟪ mf14 , subst (λ k → filter F ⊆ k ) (sym *iso) mf15 ⟫ | |
| 1134 | 368 mx : Maximal FX |
| 369 mx = Zorn-lemma (∈∅< FX∋F) SUP⊆ | |
| 1138 | 370 imf : IsFilter {L} {P} LP (& (Maximal.maximal mx)) |
| 1134 | 371 imf = proj1 (Maximal.as mx) |
| 372 mf00 : (* (& (Maximal.maximal mx))) ⊆ L | |
| 1138 | 373 mf00 = IsFilter.f⊆L imf |
| 1134 | 374 mf01 : { p q : HOD } → L ∋ q → (* (& (Maximal.maximal mx))) ∋ p → p ⊆ q → (* (& (Maximal.maximal mx))) ∋ q |
| 1138 | 375 mf01 {p} {q} Lq Fq p⊆q = IsFilter.filter1 imf Lq Fq |
| 1134 | 376 (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) )) |
| 377 mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx))) ∋ q → L ∋ (p ∩ q) | |
| 378 → (* (& (Maximal.maximal mx))) ∋ (p ∩ q) | |
| 379 mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso ( | |
| 1138 | 380 IsFilter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq )) |
| 1134 | 381 mf : Filter {L} {P} LP |
| 382 mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00 | |
| 383 ; filter1 = mf01 | |
| 384 ; filter2 = mf02 } | |
| 385 | |
| 386 | |
| 387 F→ultra : {L P : HOD} (LP : L ⊆ Power P) → (NEG : {p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q)) | |
| 1136 | 388 → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) → {y : Ordinal} → (0<F : odef (filter F) y) → (proper : ¬ (filter F ∋ od∅)) |
| 1134 | 389 → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper )) |
| 1136 | 390 F→ultra {L} {P} LP NEG CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F 0<F (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ) |
| 481 | 391 |
| 392 |