Members/kono/Proof/ZF-in-agda: src/Topology.agda comparison

comparison src/Topology.agda @ 1191:d969fc17d049

fix FIP again

author	kono
date	Mon, 27 Feb 2023 08:26:35 +0800
parents	e110b56d8cbe
children	2c35ccd5aadd

comparison

equal deleted inserted replaced

-:e110b56d8cbe
+:d969fc17d049
 open _covers_
 -- Finite Intersection Property
+data Finite-∩ (S : HOD) : Ordinal → Set n where
+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))
 record FIP {L : HOD} (top : Topology L) : Set n where
 field
 limit : {X : Ordinal } → * X ⊆ CS top
-→       ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) →  Ordinal
+→       ( { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) →  Ordinal
 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top )
-→ ( fip :  { x : Ordinal } → Subbase (* X) x → o∅ o< x )
+→ ( fip :  { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x )
 →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip)
 L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top )
-→ ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x )
+→ ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x )
 →  {x : Ordinal } → odef (* X) x
 →  odef L (limit CX fip)
 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
 -- Compact
 --
 --   X covres L means Intersection of (CX X) contains nothing
 --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
 --     it means there is a finite cover
 --
-finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L →  Subbase (Replace (* X) (λ z → L ＼ z)) o∅
+finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L →  Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅
-finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z)) o∅)
+finCoverBase {X} ox oc with ODC.p∨¬p O (Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅)
 ... | case1 sb = sb
 ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where
 fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
 fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
 -- CX is finite intersection
-fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x
+fip02 : {x : Ordinal} → Finite-∩ (* (CX ox)) x → o∅ o< x
 fip02 {x} sc with trio< x o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri> ¬a ¬b c = c
-... | tri≈ ¬a b ¬c  = ⊥-elim (¬sb (subst₂ (λ j k → Subbase j k ) *iso b sc ))
+... | tri≈ ¬a b ¬c  = ⊥-elim (¬sb (subst₂ (λ j k → Finite-∩ j k ) *iso b sc ))
 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice)
 fip26 : odef (* (CX ox))    (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )))
 fip26 = subst (λ k → odef k (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso)
 record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L))  ; x=ψz = refl }
 fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
 fip20 {y} Xy yl = proj2 fip21 yl where
 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
-finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD
+finCoverSet : {X : Ordinal } → (x : Ordinal) →  Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD
-finCoverSet {X} x (gi rx) =  ( L ＼ * x ) , ( L ＼ * x  )
+finCoverSet {X} x fin-e  =  ?
-finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy
+finCoverSet {X} x (fin-i rx) =  ( L ＼ * x ) , ( L ＼ * x  )
+finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy
 --
 -- this defines finite cover
 finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc))
 -- create Finite-∪ from cex
 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where
-fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
+fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
-fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where
+fip60 x fin-e = ?
+fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) where
 fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x))
 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso
 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))
 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
 fip34 : * z1 ⊆ L
 z1 ≡⟨ sym &iso ⟩
 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
 & (L ＼ * x ) ∎ where open ≡-Reasoning
-fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx)  (fip60 y sy)  ) where
+fip60 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx)  (fip60 y sy)  ) where
 fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy)
 fip62 = cong (&) ( begin
 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩
 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning
 -- is also a cover
 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
 (fip70 o∅ (finCoverBase xo xcp)) where
-fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
+fip70 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
-fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt }
+fip70 x fin-e  = ?
-fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers
+fip70 x (fin-i rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt }
-(L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where
+fip70 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) ? covers
+(L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where
 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ )  ⟫
 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx  ⟫
+fip71 : {a b c : HOD} → a covers c →  (a ∪ b) covers c
+fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt)
+; isCover = isCover cov }
+fip72 : {a b c : HOD} → a covers c →  (b ∪ a) covers c
+fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt)
+; isCover = isCover cov }
 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where
 fip44 :  {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal
 fip44 {x} Lab with fip45 {L} {a} {b} Lab
 ... | case1 La = cover ca La
 comp01 = subst (λ k → odef (* X) k) (sym &iso) az
 --   if all finite intersection of X contains something,
 --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
 --     it means there is a limit
-has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
+has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* 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) )
 no-cover : ¬ ( (* (OX CX)) covers L )
 no-cover cov = ⊥-elim ( ? ) where
 fp01 : Ordinal
 fp01 = Compact.finCover compact (OOX CX) cov
-fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) )
+fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Finite-∩ (* X) (& ( L ＼ * t ) )
-fp02 t fin-e = gi ?
+fp02 t fin-e = ?
-fp02 t (fin-i tx ) = gi fp03 where
+fp02 t (fin-i tx ) = ? where
 fp03 :  odef (* X) (& (L ＼ * t))
 fp03 = ?
-fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x)  (fp02 ty y ) ) where
+fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Finite-∩ (* X) k ) fp04 ( fin-∩ (fp02 tx x)  (fp02 ty y ) ) where
 fp04 :  & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫  where
 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 ⟩
 & (* X) ∎ where open o≤-Reasoning O
-limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
+limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x)
 → Ordinal
 limit {X} CX fip with trio< X o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = o∅
 ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c))
 fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
-(fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
+(fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x)
 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
 fip00 {X} CX fip {x} Xx with trio< X o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = ⊥-elim (  o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) )
 ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c )

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/Topology.agda @ 1191:d969fc17d049