\import Function.Meta ($) \import Logic \import Logic.Meta \import Meta \import Order.Directed \import Order.Lattice \import Order.PartialOrder \import Paths \import Paths.Meta \import Set \import Set.Category \import Set.Filter \import Set.Subset \open Bounded(top) \class TopSpace \extends BaseSet { | isOpen : Set E -> \Prop | open-top : isOpen Bounded.top | open-inter {U V : Set E} : isOpen U -> isOpen V -> isOpen (U ∧ V) | open-Union {S : Set (Set E)} : ∀ {U : S} (isOpen U) -> isOpen (Set.Union S) \lemma cover-open {U : Set E} (c : ∀ {x : U} ∃ (V : isOpen) (V x) (V ⊆ U)) : isOpen U => \have uo => open-Union {_} {\lam V => \Sigma (isOpen V) (V ⊆ U)} __.1 \in transport isOpen (ext \lam x => ext (\lam (inP (V,(_,V<=U),Vx)) => V<=U Vx, \lam Ux => TruncP.map (c Ux) \lam (V,Vo,Vx,V<=U) => (V, (Vo, V<=U), Vx))) uo \lemma open-IUnion {J : \hType} (g : J -> Given isOpen) : isOpen \lam x => ∃ (j : J) ((g j).1 x) => \have uo => open-Union {_} {\lam U => ∃ (j : J) ((g j).1 = U)} \lam (inP (j,p)) => transport isOpen p (g j).2 \in transport isOpen (ext \lam x => ext (\lam (inP (U, inP (j,p), Ux)) => inP (j, rewrite p Ux), \lam (inP (j,c)) => inP ((g j).1, inP (j, idp), c))) uo \type \infix 4 <=<T (V U : Set E) : \Prop => \Pi (y : E) -> ∃ (W : isOpen) (W y) (Given (V ∧ W) -> W ⊆ U) \func IsRegular => ∀ {U : isOpen} {x : U} ∃ (V : isOpen) (V x) (V <=<T U) \func IsLimit {I : DirectedSet} (f : I -> E) (l : E) : \Prop => ∀ {U : isOpen} (U l) ∃ (N : I) ∀ {n} (N <= n -> U (f n)) \func IsClosed (U : Set E) : \Prop => \Pi {x : E} -> (\Pi {V : Set E} -> isOpen V -> V x -> ∃ (U ∧ V)) -> U x } \func NFilter {X : TopSpace} (x : X) : ProperFilter X \cowith | F U => ∃ (V : isOpen) (V x) (V ⊆ U) | filter-mono p (inP (W,Wo,Wx,q)) => inP (W, Wo, Wx, q <=∘ p) | filter-top => inP (top, open-top, (), <=-refl) | filter-meet (inP (U,Uo,Ux,p)) (inP (V,Vo,Vx,q)) => inP (U ∧ V, open-inter Uo Vo, (Ux,Vx), MeetSemilattice.meet-monotone p q) | isProper (inP (V,Vo,Vx,p)) => inP (x, p Vx) \func IsDenseSet {X : TopSpace} (S : Set X) : \Prop => \Pi {x : X} {U : Set X} -> isOpen U -> U x -> ∃ (y : S) (U y) \record ContMap \extends SetHom { \override Dom : TopSpace \override Cod : TopSpace | func-cont {U : Cod -> \Prop} : isOpen U -> isOpen \lam x => U (func x) \func IsDense : \Prop => IsDenseSet (\lam y => ∃ (x : Dom) (func x = y)) \func IsEmbedding : \Prop => ∀ {U : isOpen} ∃ (V : isOpen) (U = func ^-1 V) \lemma embedding-char : IsEmbedding <-> ∀ {U : isOpen} {x : U} ∃ (V : isOpen) (V (func x)) (func ^-1 V ⊆ U) => (\lam e Uo Ux => \case e Uo \with { | inP (V,Vo,p) => inP (V, Vo, rewrite p in Ux, rewrite p <=-refl) }, \lam e {U} Uo => inP (_, open-Union {_} {\lam V => \Sigma (isOpen V) (func ^-1 V ⊆ U)} __.1, ext \lam x => ext (\lam Ux => \case e Uo Ux \with { | inP (V,Vo,Vfx,p) => inP (V, (Vo, p), Vfx) }, \lam (inP (V,(Vo,p),Vfx)) => p Vfx))) \func IsDenseEmbedding : \Prop => \Sigma IsDense IsEmbedding } \where { \func id {X : TopSpace} : ContMap X X \cowith | func x => x | func-cont Uo => Uo \func compose \alias \infixl 8 ∘ {X Y Z : TopSpace} (g : ContMap Y Z) (f : ContMap X Y) : ContMap X Z \cowith | func x => g (f x) | func-cont Uo => f.func-cont (g.func-cont Uo) \func const {Y X : TopSpace} (x : X) : ContMap Y X \cowith | func _ => x | func-cont _ => Y.cover-open \lam Ux => inP (top, open-top, (), \lam _ => Ux) } \lemma const-limit {I : DirectedSet} {X : TopSpace} {x : X} : X.IsLimit (\lam (_ : I) => x) x => \lam _ Ux => \case I.isInhabitted \with { | inP N => inP (N, \lam _ => Ux) } \lemma cont-limit {I : DirectedSet} {X Y : TopSpace} {f : I -> X} {l : X} (p : X.IsLimit f l) (g : ContMap X Y) : Y.IsLimit (\lam n => g (f n)) (g l) => \lam Uo Ugl => p (g.func-cont Uo) Ugl \class HausdorffTopSpace \extends TopSpace | isHausdorff {x y : E} : ∀ {U V : isOpen} (U x) (V y) ∃ (U ∧ V) -> x = y \lemma denseSet-lift-unique {X : TopSpace} {Y : HausdorffTopSpace} {S : Set X} (Sd : IsDenseSet S) (f g : ContMap X Y) (p : \Pi {x : X} -> S x -> f x = g x) (x : X) : f x = g x => isHausdorff \lam {U} Uo Vo Ufx Vgx => \case Sd {x} (open-inter (f.func-cont Uo) (g.func-cont Vo)) (Ufx,Vgx) \with { | inP (y,Sy,(Ufy,Vgy)) => inP (g y, (transport U (p Sy) Ufy, Vgy)) } \lemma dense-lift-unique {X Y : TopSpace} {Z : HausdorffTopSpace} (f : ContMap X Y) (fd : f.IsDense) (g h : ContMap Y Z) (p : \Pi (x : X) -> g (f x) = h (f x)) (y : Y) : g y = h y => denseSet-lift-unique fd g h (\lam (inP (x,q)) => rewriteI q (p x)) y \func TopTransfer {X : \Set} {Y : TopSpace} (f : X -> Y) : TopSpace X \cowith | isOpen U => ∃ (V : isOpen) (U = f ^-1 V) | open-top => inP (top, open-top, idp) | open-inter (inP (V,Vo,p)) (inP (V',V'o,p')) => inP (V ∧ V', open-inter Vo V'o, pmap2 (∧) p p') | open-Union {S} h => inP (Set.Union \lam V => \Sigma (isOpen V) (f ^-1 V ⊆ Set.Union S), open-Union __.1, <=-antisymmetric (\lam (inP (U,SU,Ux)) => \case h SU \with { | inP (V,Vo,p) => inP (V, (Vo, rewriteI p$ Set.Union-cond SU), rewrite p in Ux)
}) (\lam (inP (V,(Vo,p),Vfx)) => p Vfx))