# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674094420 -32400
# Node ID c4fd0bfdfbae5c2f348f7c622093cb9291c298b2
# Parent  0612874b815c7c5d2472331aeb90eb4b38c7031f
FIP to Filter done

diff -r 0612874b815c -r c4fd0bfdfbae src/Topology.agda
--- a/src/Topology.agda	Wed Jan 18 20:53:01 2023 +0900
+++ b/src/Topology.agda	Thu Jan 19 11:13:40 2023 +0900
@@ -88,6 +88,10 @@
 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫
 is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso  xy))
 
+sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x
+sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px)
+sb⊆ {P} {Q} P⊆Q (g∩ px qx) = g∩ (sb⊆ P⊆Q px) (sb⊆ P⊆Q qx)
+
 --  An open set generate from a base
 --
 --  OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →  x ∈ b ⊂ U }
@@ -408,7 +412,7 @@
 -- Ultra Filter has limit point
 
 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP )
-       (FL : filter F ∋ P) (ultra : ultra-filter F ) : Set (suc (suc n)) where
+       (ultra : ultra-filter F ) : Set (suc (suc n)) where
    field
        limit : Ordinal
        P∋limit : odef P limit
@@ -419,36 +423,62 @@
 record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where
    field
        b x : Ordinal 
+       b⊆X : * b ⊆ * X
+       sb  : Subbase (* b) x 
        0<x : o∅ o< x
-       b⊆X : * b ⊆ * X
-       u⊆X : * u ⊆ * X
+       X∋u : odef (* X) u
        x⊆u : * x ⊆ * u
-       sb : Subbase (* b) x 
+
+open import maximum-filter O
 
 UFLP→FIP : {P : HOD} (TP : Topology P) → 
-   ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP
+   ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
-     N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = ? ; <odmax = ? }
+     N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = X 
+        ; <odmax = λ {x} lt → subst₂ (λ j k → j o< k) refl &iso (odef< (NFIP.X∋u lt))  }
      N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X
-     N⊆PX {X} CSX fp {z} nz = ?
-     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (λ lt → CS⊆PL TP (CSX lt))
-     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = ? ; filter2 = ? } where
+     N⊆PX {X} CSX fp {z} nz = NFIP.X∋u nz
+     X⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → * X ⊆ Power P
+     X⊆PP CSX lt = CS⊆PL TP (CSX lt)
+     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (X⊆PP CSX)
+     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = f1 ; filter2 = f2 } where
          f1 :  {p q : HOD} → * X ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
-         f1 {p} {q} Lq Np p⊆q = ?
+         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; 0<x = 0<x ; X∋u = Xp ; x⊆u = x⊆p } p⊆q = 
+                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; 0<x = 0<x ; X∋u = Xq ; x⊆u = λ {z} xp → 
+                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } 
+         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → * X ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
+         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; 0<x = f21 ; X∋u = Xpq ; x⊆u = f22 } where
+              Np+Nq = * (NFIP.b Np) ∪ * (NFIP.b Nq)
+              xp∧xq = * (NFIP.x Np) ∩ * (NFIP.x Nq)
+              sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
+              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (NFIP.sb Np)) (sb⊆ case2 (NFIP.sb Nq)))
+              f20 : * (& Np+Nq) ⊆ * X
+              f20 {x} npq with subst (λ k → odef k x) *iso npq
+              ... | case1 np = NFIP.b⊆X Np np
+              ... | case2 nq = NFIP.b⊆X Nq nq
+              f21 : o∅ o< & xp∧xq
+              f21 = fp f20 sbpq 
+              f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
+              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq 
+                 → ⟪ subst (λ k → odef k w) *iso ( NFIP.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( NFIP.x⊆u Nq (proj2 xpq)) ⟫ )
+     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
+     proper = ?
+     CAP : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → {p q : HOD } → * X ∋ p → * X ∋ q → * X ∋ (p ∩ q)
+     CAP = ?
+     maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (X⊆PP CSX) (F CSX fp)
+     maxf {X} CSX fp = F→Maximum (X⊆PP CSX) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)
      uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     uf00 {X} CSX fip = ?
-     -- UFLP.limit ( uflp
-     --    ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? ))
-     --    ?
-     --    (F→ultra LP ? ? (F CSX fip)  ? ? ? ) )
+     uf00 {X} CSX fp = UFLP.limit ( uflp (X⊆PP CSX)
+         ( MaximumFilter.mf (maxf CSX fp) )
+         (F→ultra (X⊆PP CSX) (CAP CSX fp) (F CSX fp)  ? ? (proper CSX fp)))
 
 -- some day
 FIP→UFLP : Set (suc (suc n))
 FIP→UFLP = {P : HOD} (TP : Topology P) →  FIP TP
-   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
 
 -- product topology of compact topology is compact
 
@@ -457,9 +487,9 @@
     L = pbase TP TQ
     LPQ = pbase⊆PL TP TQ
     -- Product of UFL has limit point
-    uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F)
-             → UFLP (ProductTopology TP TQ) LP F LF UF
-    uflp {L} LP F LF UF = record { limit = & < ? , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} }
+    uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP)  (UF : ultra-filter F)
+             → UFLP (ProductTopology TP TQ) LP F UF
+    uflp {L} LP F UF = record { limit = & < ? , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} }
 
 
 
diff -r 0612874b815c -r c4fd0bfdfbae src/maximum-filter.agda
--- a/src/maximum-filter.agda	Wed Jan 18 20:53:01 2023 +0900
+++ b/src/maximum-filter.agda	Thu Jan 19 11:13:40 2023 +0900
@@ -55,9 +55,9 @@
 import zorn 
 open zorn O _⊂_ PO
 
-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))
+F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → o∅ o< & L →  {y : Ordinal } → odef (filter F) y →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
-F→Maximum {L} {P} LP NEG CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = subst (λ k → filter F ⊆ k ) (sym *iso) mf52  
+F→Maximum {L} {P} LP CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = subst (λ k → filter F ⊆ k ) (sym *iso) mf52  
          ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( IsFilter.proper imf)  ; is-maximum = mf50 }  where
       FX : HOD
       FX = F⊆X {L} {P} LP F
@@ -156,9 +156,9 @@
          mf51 : filter F ⊆ * (& (filter f))
          mf51 = subst (λ k → filter F ⊆ k ) (sym *iso) F⊆f 
 
-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))
+F→ultra : {L P : HOD} (LP : L ⊆ Power P) → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) →  {y : Ordinal} →  (0<F : odef (filter F) y) →  (proper : ¬ (filter F ∋ od∅)) 
-      → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ))
-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 ) 
+      → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP CAP F 0<L 0<F proper ))
+F→ultra {L} {P} LP CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F 0<F (F→Maximum {L} {P} LP CAP F 0<L 0<F proper )