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

comparison src/Tychonoff.agda @ 1279:7e7d8d825632

P x Q ⇆ Q x P done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Thu, 06 Apr 2023 09:16:52 +0900
parents	b15dd4438d50
children	f4dac8be0a01

comparison

equal deleted inserted replaced

-:2cbe0db250da
+:7e7d8d825632
 open ODC O
 open import filter O
 open import ZProduct O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 open Filter
 open Topology
 --
 field
 limit : Ordinal
 P∋limit : odef P limit
 is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)
+--
+-- If Any ultra filter has a limit that is  all neighbor of the limit is in the filter,
+-- it has finite intersection property.
+--
+-- Finite intersection defines a filter, so we have a ultra filter becaause Zorn lemma maximizing it.
+-- If the limit of filter is not contained by a closed set p in FIP, it is in P \ p. It is open and
+-- contains the limit, so it is in the ultra filter. This means p and P \ p is in the filter, which
+-- contradicts proper of the ultra filter.
+--
 UFLP→FIP : {P : HOD} (TP : Topology P) →
 ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp with trio< (& P) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where
 -- then we have maximum ultra filter ( Zorn lemma )
 --    to debug this file, commet out the maximum filter and open import
 --    otherwise the check requires a minute
 --
 maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-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)
+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)
 mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
 mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
 ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-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)
+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)
 --
--- so it has a limit as a limit of UIP
+-- so it has a limit as a limit of FIP
 --
 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
 limit {X} CSX fp with trio< o∅ X
 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))
 ... | tri≈ ¬a 0=X ¬c = o∅
 x⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → x ⊆ Cl TP x
 x⊆Clx {P} TP {x}  x<p {y} xy  = ⟪ x<p xy , (λ c csc x<c → x<c xy )  ⟫
 P⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → Cl TP x ⊆ P
 P⊆Clx {P} TP {x}  x<p {y} xy  = proj1 xy
+--
+-- Finite intersection property implies that any ultra filter have a limit, that is, neighbors of the limit is in the filter.
+--
+-- An ultra filter F is given. Take a closure of a filter. It is closed and it has finite intersection property, because F is porper.
+-- So it has a limit as a FIP. If a neighbor p which contains the limit, p or P \ p is in the ultra filter.
+-- If it is in P \ p, it cannot contains the limit, contradiction.
+--
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
 →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
 ; P∋limit = ufl10 ; is-limit = ufl00 } where
 F∋P : odef (filter F) (& P)
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))
+--    FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))
-→ Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x)
+--         → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x)
-FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
+--    FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
+--
-projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))
+--    projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))
-→ Filter {Power P} {P} (λ x → x)
+--         → Filter {Power P} {P} (λ x → x)
-projection-of-filter = ?
+--    projection-of-filter = ?
+--
-projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
+--    projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
-→ ultra-filter (projection-of-filter F)
+--         → ultra-filter (projection-of-filter F)
-projection-of-ultra-filter = ?
+--    projection-of-ultra-filter = ?
+--
+-- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter
+-- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q,
+-- which is either inverse projection x of P or Q. The x in in projection of F, because of UFLP. So it is in F, because of the
+-- property of the filter.
+--
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
 uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
 → UFLP TP F UF
 uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF

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

comparison src/Tychonoff.agda @ 1279:7e7d8d825632