Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1198:6e0cc71097e0
fip <-> compact done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 01 Mar 2023 09:00:11 +0900 |
| parents | 0a88fcd5d1c9 |
| children | 1338b6c6a9b6 |
| files | src/Topology.agda |
| diffstat | 1 files changed, 58 insertions(+), 51 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Wed Mar 01 00:37:34 2023 +0900 +++ b/src/Topology.agda Wed Mar 01 09:00:11 2023 +0900 @@ -283,6 +283,7 @@ fin-e : Finite-∪ S o∅ fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x )) fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) + -- Finite-∪ S y → Union y ⊆ S record Compact {L : HOD} (top : Topology L) : Set n where field @@ -420,10 +421,25 @@ Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top Compact→FIP {L} top compact with trio< (& L) o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) -... | tri≈ ¬a b ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX xx) } where - fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ¬ odef (* X) x - fip000 {X} {x} CX xx = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) b)) o∅≡od∅ ) (sym &iso) - ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) ? )) +... | tri≈ ¬a L=0 ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX fip xx) } where + -- empty L case + -- if 0 < X then 0 < x ∧ L ∋ xfrom fip + -- if 0 ≡ X then ¬ odef X x + fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ({y : Ordinal} → Subbase (* X) y → o∅ o< y) → ¬ odef (* X) x + fip000 {X} {x} CX fip xx with trio< o∅ X + ... | tri< 0<X ¬b ¬c = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) L=0)) o∅≡od∅ ) (sym &iso) + ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) Xe )) where + 0<x : o∅ o< x + 0<x = fip (gi xx ) + e : HOD -- we have an element of x + e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) + Xe : odef (* x) (& e) + Xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) + ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin + * X ≡⟨ cong (*) (sym 0=X) ⟩ + * o∅ ≡⟨ o∅≡od∅ ⟩ + od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning + ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) )) ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where -- set of coset of X @@ -440,34 +456,37 @@ has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where - fp07 : HOD -- we have an element of X - fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) - fp08 : odef (* X) (& fp07) - fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) + e : HOD -- we have an element of X + e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) + Xe : odef (* X) (& e) + Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) no-cover : ¬ ( (* (OX CX)) covers L ) - no-cover cov = ⊥-elim (f20 (Compact.isCover compact (OOX CX) cov)) where + no-cover cov = ⊥-elim (no-finite-cover (Compact.isCover compact (OOX CX) cov)) where + -- construct Subase from Finite-∪ fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov record SB (t : Ordinal) : Set n where field i : Ordinal sb : Subbase (* X) (& (L ＼ * i)) - not-t : (L ＼ * i) ⊆ (L ＼ Union ( * t ) ) + t⊆i : (L ＼ * i) ⊆ (L ＼ Union ( * t ) ) fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t - fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = fp23 } where - fp22 : fp07 ⊆ L - fp22 {x} lt = cs⊆L top (CX fp08) lt - fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07))) + fp02 t fin-e = record { i = & ( L ＼ e) ; sb = gi (subst (λ k → odef (* X) k) fp21 Xe) ; t⊆i = fp23 } where + -- t ≡ o∅, no cover. Any subst of L is ok and we have e ⊆ L + fp22 : e ⊆ L + fp22 {x} lt = cs⊆L top (CX Xe) lt + fp21 : & e ≡ & (L ＼ * (& (L ＼ e))) fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso))) - fp23 : (L ＼ * (& (L ＼ fp07))) ⊆ (L ＼ Union (* o∅)) + fp23 : (L ＼ * (& (L ＼ e))) ⊆ (L ＼ Union (* o∅)) fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫ - fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = fp24 } where + fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; t⊆i = fp24 } where + -- we have a single cover x, L ＼ * x is single finite intersection fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x)))) fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25 ⟫ where fp25 : ¬ odef (Union (* x , * x)) y fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox ) - fp03 : odef (* X) (& (L ＼ * x)) + fp03 : odef (* X) (& (L ＼ * x)) -- becase x is an element of Replace (* X) (λ z → L ＼ z ) fp03 with subst (λ k → odef k x ) *iso tx ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where fip34 : * z1 ⊆ L @@ -479,8 +498,8 @@ & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ & (L ＼ * x ) ∎ where open ≡-Reasoning - fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = fp35 } where - fp35 : (L ＼ * (& (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty)))) + fp02 t (fin-∪ {tx} {ty} ux uy ) = record { i = & (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ; sb = fp11 ; t⊆i = fp35 } where + fp35 : (L ＼ * (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty)))) fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36 where fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) ao )) @@ -493,21 +512,21 @@ fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } - fp36 : (L ＼ (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* tx ∪ * ty)) + fp36 : (L ＼ (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* tx ∪ * ty)) fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where fp37 : ¬ odef (Union (* tx ∪ * ty)) z fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where - fp38 : (L ＼ (* (SB.i (fp02 tx x)))) ⊆ (L ＼ Union (* tx)) - fp38 = SB.not-t (fp02 tx x) - fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx x))) - fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx x))} (fp40 x txw) + fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx)) + fp38 = SB.t⊆i (fp02 tx ux) + fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux))) + fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx ux))} (fp40 ux txw) ... | case1 sb = sb ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where - fp38 : (L ＼ (* (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* ty)) - fp38 = SB.not-t (fp02 ty y) - fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty y))) - fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty y))} (fp40 y tyw) + fp38 : (L ＼ (* (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* ty)) + fp38 = SB.t⊆i (fp02 ty uy) + fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty uy))) + fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw) ... | case1 sb = sb ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) @@ -522,33 +541,21 @@ fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ - fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))))) - fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx x)) (SB.sb (fp02 ty y )) ) - fp12 : (L ＼ * (SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)))) ⊆ Union (* fp01) - fp12 {x} ⟪ Lx , not ⟫ = fp17 fp19 where - fcov = Compact.isCover compact (OOX CX) cov - fp13 : Ordinal - fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)) - fp16 : {y : Ordinal} → odef (L ＼ * fp13) y → odef L y - fp16 {y} ⟪ Ly , _ ⟫ = Ly - fp15 : ¬ ( odef (* fp13) x) - fp15 = not - fp19 : odef (L ＼ * fp13) x - fp19 with ∨L＼X {L} {* fp13} Lx - fp19 | case1 lt = ⊥-elim (not lt) - fp19 | case2 lt = lt - fp17 : (L ＼ * fp13 ) ⊆ Union (* fp01 ) - fp17 {y} lt = record { owner = cover fcov (fp16 lt) ; ao = P∋cover fcov (fp16 lt) ; ox = isCover fcov (fp16 lt) } + fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))))) + fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx ux)) (SB.sb (fp02 ty uy )) ) + -- + -- becase of fip, finite cover cannot be a cover + -- fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov) fcov = Compact.isFinite compact (OOX CX) cov 0<sb : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → o∅ o< & (L ＼ * i) 0<sb {i} sb = fip sb sb : SB (Compact.finCover compact (OOX CX) cov) sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov) - f20 : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) - f20 fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where + no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) + no-finite-cover fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) - f23 = SB.not-t sb + f23 = SB.t⊆i sb f22 : (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅ f22 = record { eq→ = λ lt → ⊥-elim ( f24 lt) ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where f24 : {x : Ordinal } → ¬ ( odef (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) x ) @@ -558,7 +565,7 @@ & (L ＼ * (SB.i sb)) ≤⟨ ⊆→o≤ f23 ⟩ & (L ＼ Union (* (Compact.finCover compact (OOX CX) cov))) ∎ ) where open o≤-Reasoning O - record NC : Set n where -- x is not covered + record NC : Set n where -- find an element xi, which is not covered (which is a limit point) field x : Ordinal yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x @@ -594,8 +601,8 @@ fp06 : NC.x not-covered o≤ & (* X) fp06 = begin NC.x not-covered ≡⟨ sym &iso ⟩ - & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ - & fp07 <⟨ c<→o< fp08 ⟩ + & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered Xe)) ⟩ + & e <⟨ c<→o< Xe ⟩ & (* X) ∎ where open o≤-Reasoning O limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal