From 257d39650ec74800548aa1617c9eb57efaa75708 Mon Sep 17 00:00:00 2001 From: valis Date: Fri, 23 Feb 2024 23:24:16 +0300 Subject: [PATCH] Simplify the proof that completion is complete --- src/Topology/CoverSpace/Complete.ard | 118 +++++++++++++++------------ 1 file changed, 66 insertions(+), 52 deletions(-) diff --git a/src/Topology/CoverSpace/Complete.ard b/src/Topology/CoverSpace/Complete.ard index 39d0a6bf..f5f5e895 100644 --- a/src/Topology/CoverSpace/Complete.ard +++ b/src/Topology/CoverSpace/Complete.ard @@ -176,6 +176,29 @@ | inP (U, inP (V,CV,p), FU) => inP (V, CV, rewriteI p FU) } +\lemma CF-map_<= {X Y : CoverSpace} {f : CoverMap X Y} (F G : CauchyFilter X) (p : F ⊆ G) : CF-map f F ⊆ CF-map f G + => p __ + +\func dense-filter-lift {X Y : CoverSpace} (f : CoverMap X Y) (fd : f.IsDenseEmbedding) (F : CauchyFilter Y) : CauchyFilter X \cowith + | F U => ∃ (V' V : Set Y) (f ^-1 V ⊆ U) (V' <=< V) (F V') + | filter-mono U<=U' (inP (V',V,p,V'<= inP (V', V, p <=∘ U<=U', V'<= inP (top, top, \lam _ => (), <=<_top, filter-top) + | filter-meet (inP (U',U,p,U'<= inP (U' ∧ V', U ∧ V, MeetSemilattice.meet-monotone p q, <=<_meet U'<= \case F.isProper FV' \with { + | inP (y,V'y) => \case fd.1 (<=<-right (single_<= V'y) V'<= inP (x, p Vfx) + } + } + | isCauchyFilter Cc => \case F.isCauchyFilter $ isRegular $ fd.2 Cc \with { + | inP (V', inP (V, inP (U, CU, p), V'<= inP (U, CU, inP (V', V, p, V'<= \lam {C} Cc => \case isCauchyFilter {F} (isRegular Cc) \with { + | inP (V', inP (V, CV, V'<= inP (V, CV, (inP (V', V, <=-refl, V'<= Z.filter-point $ CF-map g \new CauchyFilter { | F U => ∃ (V : Set Y) (f ^-1 V ⊆ U) (single y <=< V) @@ -192,60 +215,17 @@ | func-cover Dc => cauchy-extend (isRegular $ fd.2 $ g.func-cover $ isRegular Dc) $ \lam {V'} (inP (V, inP (U, inP (W', inP (W, DW, W'<= inP (_, inP (W, DW, idp), \lam {y} V'y => <=<_<= (Z.filter-point-elem W'<= ∃ (y : Y) (pointCF y ⊆ CF-map f F)) : IsCompleteCoverSpace Y + => \lam F => \case p $ minCF $ dense-filter-lift f fd F \with { + | inP (y,q) => inP (y, MinCauchyFilter.Min_CF~_<= {_} {pointCF y} $ ~-transitive {_} {pointCF y} (CF~_<= {_} {pointCF y} $ q <=∘ CF-map_<= (minCF $ dense-filter-lift f fd F) (dense-filter-lift f fd F) \lam u => u <=-refl) $ dense-filter-lift.map-equiv fd) + } + \instance CompletionCoverSpace (S : CoverSpace) : CompleteCoverSpace (MinCauchyFilter S) - | isCauchy => isCCauchy - | cauchy-cover {D} (inP (C,Cc,p)) F => - \have | (inP (U,CU,FU)) => isCauchyFilter Cc - | (inP (V,DV,q)) => p CU - \in inP (V, DV, q FU) - | cauchy-top => inP (single top, cauchy-top, \lam _ => inP (top, idp, \lam _ => ())) - | cauchy-extend (inP (E,Ec,g)) f => inP (E, Ec, \lam EU => - \have | (inP (V,CV,p)) => g EU - | (inP (W,DW,q)) => f CV - \in inP (W, DW, p <=∘ q)) - | cauchy-trans {C} {D} (inP (C',C'c,f)) Dc => inP (_, S.cauchy-trans {C'} {\lam U' V' => ∃ (U : C) (V : D U) (mkSet U' ⊆ U) (mkSet V' ⊆ V)} C'c \lam {U'} C'U' => - \have | (inP (U,CU,U'<=U)) => f C'U' - | (inP (D',D'c,g)) => Dc CU - \in cauchy-extend D'c \lam {V'} D'V' => \case g D'V' \with { - | inP (V,DV,V'<=V) => inP (V', inP (U, CU, V, DV, U'<=U, V'<=V), <=-refl) - }, \lam {W'} (inP (U', V', C'U', inP (U, CU, V, DV, U'<=U, V'<=V), W'=U'V')) => inP (U ∧ V, inP (U, V, CU, DV, idp), rewrite W'=U'V' \lam {F} FU'V' => (U'<=U $ filter-mono meet-left FU'V', V'<=V $ filter-mono meet-right FU'V'))) - | isRegular {D} (inP (C,Cc,f)) => - \have <=<_mkFilters {U' U : Set S} (p : U' <=< U) : mkSet U' <=< mkSet U - => unfolds $ inP (_, p, \lam {W} g => inP (mkSet W, \lam (inP (F,(FU',FW))) => mkSet_<= $ g (isProper (filter-meet FU' FW)), <=-refl)) - \in inP (_, isRegular Cc, \lam {U'} (inP (U,CU,U'<= \case f CU \with { - | inP (V,DV,U<=V) => inP (mkSet U', inP (V, DV, <=<-left (<=<_mkFilters U'<= coverSpace | isSeparatedCoverSpace p => MinCauchyFilter.equality \lam Cc => \case p (mkCover-cauchy Cc) \with { | inP (_, inP (U,CU,idp), r) => inP (U,CU,r) } - | isCompleteCoverSpace F => inP - (\new MinCauchyFilter { - | F U => F (mkSet U) - | filter-mono p => filter-mono (mkSet_<= p) - | filter-top => rewrite mkSet_top filter-top - | filter-meet x y => rewrite mkSet_meet (filter-meet x y) - | isProper x => \case isProper x \with { - | inP s => isProper {s.1} s.2 - } - | isCauchyFilter Cc => \case isCauchyFilter {F} (mkCover-cauchy Cc) \with { - | inP (V, inP (U,CU,p), FV) => inP (U, CU, rewriteI p FV) - } - | isMinFilter {G} p c => \have (inP (U',GU',q)) => isMinFilter {F} {\new CauchyFilter { - | F V => ∃ (U : Set S) (minCF G U) (mkSet U ⊆ V) - | filter-mono p (inP (U,GU,q)) => inP (U, GU, q <=∘ p) - | filter-top => inP (top, \lam _ => filter-top, top-univ) - | filter-meet (inP (U1,GU1,p1)) (inP (U2,GU2,p2)) => inP (U1 ∧ U2, filter-meet GU1 GU2, rewrite mkSet_meet $ MeetSemilattice.meet-monotone p1 p2) - | isProper {V} (inP (U',GU',q)) => inP (minCF G, q $ later GU') - | isCauchyFilter {D} (inP (C,Cc,f)) => - \have | (inP (U',CU',GU')) => isCauchyFilter {minCF G} Cc - | (inP (V,DV,q)) => f CU' - \in inP (V, DV, inP (U',GU',q)) - }} (\lam {V} (inP (U',GU',q)) => filter-mono q $ p $ GU' <=-refl) c - \in q {minCF G} GU' <=-refl - }, \lam {V} (inP (C,Cc,f)) => - \have | (inP (V', inP (U,CU,p), FV')) => isCauchyFilter {F} (mkCover-cauchy Cc) - | (inP (W,g,q)) => f CU - \in filter-mono (g $ inP (_, (idp, q $ later $ rewriteF p FV'))) $ filter-mono q $ rewriteI p FV') + | isCompleteCoverSpace => dense-complete completionCoverSpace.isDenseEmbedding \lam F => inP (F, completionCoverSpace.dense-aux {_} {F} __) \where { \func mkSet (U : Set S) : Set (MinCauchyFilter S) => \lam F => F U @@ -267,13 +247,47 @@ \lemma mkCover-cauchy {C : Set (Set S)} (Cc : isCauchy C) : isCCauchy (mkCover C) => inP (C, Cc, \lam {U} CU => inP (mkSet U, inP (U,CU,idp), <=-refl)) + + \func coverSpace : CoverSpace (MinCauchyFilter S) \cowith + | isCauchy => isCCauchy + | cauchy-cover {D} (inP (C,Cc,p)) F => + \have | (inP (U,CU,FU)) => isCauchyFilter Cc + | (inP (V,DV,q)) => p CU + \in inP (V, DV, q FU) + | cauchy-top => inP (single top, cauchy-top, \lam _ => inP (top, idp, \lam _ => ())) + | cauchy-extend (inP (E,Ec,g)) f => inP (E, Ec, \lam EU => + \have | (inP (V,CV,p)) => g EU + | (inP (W,DW,q)) => f CV + \in inP (W, DW, p <=∘ q)) + | cauchy-trans {C} {D} (inP (C',C'c,f)) Dc => inP (_, S.cauchy-trans {C'} {\lam U' V' => ∃ (U : C) (V : D U) (mkSet U' ⊆ U) (mkSet V' ⊆ V)} C'c \lam {U'} C'U' => + \have | (inP (U,CU,U'<=U)) => f C'U' + | (inP (D',D'c,g)) => Dc CU + \in cauchy-extend D'c \lam {V'} D'V' => \case g D'V' \with { + | inP (V,DV,V'<=V) => inP (V', inP (U, CU, V, DV, U'<=U, V'<=V), <=-refl) + }, \lam {W'} (inP (U', V', C'U', inP (U, CU, V, DV, U'<=U, V'<=V), W'=U'V')) => inP (U ∧ V, inP (U, V, CU, DV, idp), rewrite W'=U'V' \lam {F} FU'V' => (U'<=U $ filter-mono meet-left FU'V', V'<=V $ filter-mono meet-right FU'V'))) + | isRegular {D} (inP (C,Cc,f)) => + \have <=<_mkFilters {U' U : Set S} (p : U' <=< U) : mkSet U' <=< mkSet U + => unfolds $ inP (_, p, \lam {W} g => inP (mkSet W, \lam (inP (F,(FU',FW))) => mkSet_<= $ g (isProper (filter-meet FU' FW)), <=-refl)) + \in inP (_, isRegular Cc, \lam {U'} (inP (U,CU,U'<= \case f CU \with { + | inP (V,DV,U<=V) => inP (mkSet U', inP (V, DV, <=<-left (<=<_mkFilters U'<= pointCF | func-cover (inP (C,Cc,f)) => cauchy-extend (isRegular Cc) \case \elim __ \with { | inP (U',CU',U<= \case f CU' \with { | inP (V,DV,p) => inP (pointCF ^-1 V, inP (V, DV, idp), \lam Ux => p $ <=<-right (single_<= Ux) U<= V (completionCoverSpace S x) \elim r + | inP (C,Cc,f) => + \have | (inP (U', inP (U, CU, U'<= isCauchyFilter {F} (isRegular Cc) + | (inP (W,g,U<=W)) => f CU + \in filter-mono (\lam U'x => g (inP (F, (idp, U<=W $ filter-mono (<=<_<= U'<= (\lam r => isProper (dense-aux r), \lam {C} Cc => inP (C, Cc, \lam {U} CU => inP (CompletionCoverSpace.mkSet U, inP (U, CU, <=<_<= __ idp), <=-refl))) + } \ No newline at end of file