Skip to content

Commit

Permalink
Simplify the proof that completion is complete
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Feb 23, 2024
1 parent e2cf9b2 commit 257d396
Showing 1 changed file with 66 additions and 52 deletions.
118 changes: 66 additions & 52 deletions src/Topology/CoverSpace/Complete.ard
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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'<=<V,FV')) => inP (V', V, p <=∘ U<=U', V'<=<V, FV')
| filter-top => inP (top, top, \lam _ => (), <=<_top, filter-top)
| filter-meet (inP (U',U,p,U'<=<U,FU')) (inP (V',V,q,V'<=<V,FV')) => inP (U' ∧ V', U ∧ V, MeetSemilattice.meet-monotone p q, <=<_meet U'<=<U V'<=<V, filter-meet FU' FV')
| isProper (inP (V',V,p,V'<=<V,FV')) => \case F.isProper FV' \with {
| inP (y,V'y) => \case fd.1 (<=<-right (single_<= V'y) V'<=<V) \with {
| inP (x,Vfx) => inP (x, p Vfx)
}
}
| isCauchyFilter Cc => \case F.isCauchyFilter $ isRegular $ fd.2 Cc \with {
| inP (V', inP (V, inP (U, CU, p), V'<=<V), FV') => inP (U, CU, inP (V', V, p, V'<=<V, FV'))
}
\where {
\lemma map-equiv (fd : f.IsDenseEmbedding) : CF-map f (dense-filter-lift f fd F) CF~ F
=> \lam {C} Cc => \case isCauchyFilter {F} (isRegular Cc) \with {
| inP (V', inP (V, CV, V'<=<V), FV') => inP (V, CV, (inP (V', V, <=-refl, V'<=<V, FV'), filter-mono (<=<_<= V'<=<V) FV'))
}
}

\func dense-lift {X Y : CoverSpace} {Z : CompleteCoverSpace} (f : CoverMap X Y) (fd : f.IsDenseEmbedding) (g : CoverMap X Z) : CoverMap Y Z \cowith
| func y => Z.filter-point $ CF-map g \new CauchyFilter {
| F U => ∃ (V : Set Y) (f ^-1 V ⊆ U) (single y <=< V)
Expand All @@ -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'<=<W), p), q), V'<=<V)) =>
inP (_, inP (W, DW, idp), \lam {y} V'y => <=<_<= (Z.filter-point-elem W'<=<W $ inP $ later (V, rewriteF p q, <=<-right (single_<= V'y) V'<=<V)) idp)

\lemma dense-complete {X Y : CoverSpace} {f : CoverMap X Y} (fd : f.IsDenseEmbedding) (p : \Pi (F : MinCauchyFilter X) -> ∃ (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'<=<U)) => \case f CU \with {
| inP (V,DV,U<=V) => inP (mkSet U', inP (V, DV, <=<-left (<=<_mkFilters U'<=<U) U<=V), <=-refl)
})
| CoverSpace => 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
Expand All @@ -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'<=<U)) => \case f CU \with {
| inP (V,DV,U<=V) => inP (mkSet U', inP (V, DV, <=<-left (<=<_mkFilters U'<=<U) U<=V), <=-refl)
})
}

\func completionCoverSpace (S : CoverSpace) : CoverMap S (CompletionCoverSpace S) \cowith
\func completionCoverSpace (S : CoverSpace) : CoverMap S CompletionCoverSpace.coverSpace \cowith
| func => pointCF
| func-cover (inP (C,Cc,f)) => cauchy-extend (isRegular Cc)
\case \elim __ \with {
| inP (U',CU',U<=<U') => \case f CU' \with {
| inP (V,DV,p) => inP (pointCF ^-1 V, inP (V, DV, idp), \lam Ux => p $ <=<-right (single_<= Ux) U<=<U')
}
}
}
\where {
\protected \lemma dense-aux {F : MinCauchyFilter S} {V : Set (MinCauchyFilter S)} (r : single F <=< {CompletionCoverSpace.coverSpace} V) : F \lam x => V (completionCoverSpace S x) \elim r
| inP (C,Cc,f) =>
\have | (inP (U', inP (U, CU, U'<=<U), FU')) => 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'<=<U) FU'))) $ U<=W $ <=<-right (single_<= U'x) U'<=<U) FU'

\lemma isDenseEmbedding : CoverMap.IsDenseEmbedding {completionCoverSpace S}
=> (\lam r => isProper (dense-aux r), \lam {C} Cc => inP (C, Cc, \lam {U} CU => inP (CompletionCoverSpace.mkSet U, inP (U, CU, <=<_<= __ idp), <=-refl)))
}

0 comments on commit 257d396

Please sign in to comment.