.Open Topology

.History
Originally topologogy was developed to clarify the ideas of `space`, 
`limit`, `nearness`, `continuous`, ... Nowadays topology is used in 
software theory to model how finite approximations can imply infinite 
properties - in particular ideas like `infiniely close` and `infinitely 
large`. The key idea is that some conditons that are carried over as the 
finite becomes infinite.  Thus topology is concerned with the how an 
infinite sequence can "look as if it was going to a particular value" and the
way a function's values change as its arguments change in a `smooth` way.
It is based on a study of sets of `points` in a `space`. For example in a 
certain kind of sets if a series stays in the set then if series tends to a
limit, the limit is forced to remain in the set as well.  Other sets can 
allow a limit of an internal sequence to escape.  It took people about 100
to 200 years to abstract the essence of these ideas - they are very 
abstract, and so very powerful, and so worthy of study.

.See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html
Use open and closed families plus filters and refinement.

. Spaces
A space has a set of points with a defined topology:
Spaces::=$TOPOLOGY.

The next section collects many major ideas together. Later sections give more information on specific topics.

.  Definition of a Topology
TOPOLOGY::=Net{

There are many approaches to defining a topology of a space, differing only in theire appeal to different people. This one starts with the 'closure' operation. Others follow.

To 'close' a set is to add points to it - those points that we decide are `infinitely close to` or `on the edge of` the set.  The result of 'close' is a 'closed' set.
	X::=Space::Sets -- the set of points in the space. 
	0::@X={x:X||false} - the null subset of the space.
CLOSURE::=Net{ The close operator adds points on the edge of a set to that set.
A more precisely, the boundary of a set and the idea of closeness is defined by the closure function.
	close::(monoid)(@X,|,0)->(@X,|,0),
	|- close;close=close,
	F|- or all A:@X(A==>close(A)),
	close::X->@X=close({(_)}).

 For x:X, Y:@X, x in close(Y)=`x is close to or inside Y`.

dense::={A:@X||close(A)=X},
closed,open::@@X.

|-closed={A:@X || close(X)=X },
()|- closed in closed_family(X),

|- close(A)=min{C:closed||A==>C}.

If we removes a closed set from a space then we remove its "edge" as well an leave behind a set that is said to be open.
|-open={A:@X|| X~A in closed},
()|- open in open_family(X).

discrete::@= (open=@X).
indiscrete::@= (open={0,X}).

Note well: there are sets that are both open and closed, and there can be sets that are neither open or closed.

interior::@X->@X,
exterior::@X->@X,
boundary::@X->@X,

 |-For all A:@X, X>=={interior(A), boundary(A), exterior(A)}.

|- For all A:@X,
	interior(A)=(|(open & @A)),
	exterior(A)=(interior(X~A)),
	boundary(A)=(X~interior(A)~exterior(A)).

()|- dense={A:@X||exterior(A)={}}.


 |- For all A:@S, boundary(A)=boundary(S~A).

open_neighbourhoods::X->@@X.
neighbourhoods::X->@@X.
fundamental_neighbourhoods::X->@@X.

 |-For x:X,
	open_neighbourhoods(x)={G:open||x in G},
	neighbourhoods(x)={N:@X||for some G:open( p in G ==> N)},
	fundamental_neighbourhoods(x)={F:@@X ||for all V:open_neighbourhoods(x), some W:F (W==>V)}.

 For A:@X, neighbourhoods(A)={N:@X||for some G:open(A==>G==>N)}.
separated::=$Hausdorf.
Hausdorff::@=`Any two points can be separated or Housed-off.`.
|- Housdorff iff for x,y:X, if x<>y then for some N1:n(x), N2:n(y) ( N1&N2 ).
|- if Housdorff then for x:X, {x} in closed.

basis::@@X.
 |- For all x:X ({V:basis||x in V}in fundamental_neighbourhoods(x)).

 For p:X, W:@^S, for x:near[p](W(x)) ::=for some N:neighbourhoods(p), all x:N (W(x)).
inside::@(@X,@X)= (1st)==>interior((2nd)).
()|- if A inside B then some C:open(A==>C==>B).
()|- neighbourhoods=[x:X]{A:@X||{x}inside A}.
()|- open={A||A inside X}.

. Isolated points of a Space.

 For A:@X, isolated(A) ::={x:X||some N:neighbourhood(x)( A&N={x})}.

. Subspaces of X.

 For Y:@Y, Y subspace X ::= Y in subspaces.
subspaces::={Y:@X||Y.open={G&Y:@Y||G:X.open}.
()|- for Y:subspaces(Y.open in open_family(Y)).

compact::@.
compact::=Hausdorff and for all oc:open & covers(X), some foc:FiniteSubsets(oc)(foc in covers(X)),
()|- for all oc:open & covers(X), some foc:FiniteSubsets(oc)(foc in covers(X)) iff for all cc:closed & covers(X), some fcc:FiniteSubsets(fc)(fcc in covers(X)).
compact_sets::={A:@X||A subspace X and compact.A}.

. Limits in X.

 For Y:Sets, \beta:filter_bases(Y), f:Y->X,
	f ->[\beta] l::=for all V:(X.neighbourhoods)(l), some b:\beta. (f(B)==>V),
	f ->[\beta] l::= `f tends to l along \beta in space X`.
Cf. LIMITS later.
connected:@.
?? connected::=no(open & covers(X)).?.
}=::CLOSURE.

. Text Book Definitions.
There are other ways to define a topology. The text book starting point is from either a closed or an open family of subsets of the space `S`.

CLOSED::=Net{
S::Sets, 
closed::closed_family(S).
|- TOPOLOGY and Net{close:=[A]min{B:closed||A==>B} }.
}=::CLOSED.

OPEN::=Net{ .
S::Sets, 
open::open_family(S),
Duality: |-CLOSED and Net{ closed:={S~G:@X||G in Open} }.

Once you have got a set of points and the set of all open sets than you 
have determined the `shape` of the space. Knowing the closed sets 
determines the shape as well. As an example suppose that the whole space 
S>=={A,B} and both A,B in open, then clearly its possible for a sequence to
be in A and for its limit to `jump` to B and vice versa - the space is not
connected.
}=::OPEN.

INSIDE::=Net{
An alternative approach is to take the idea of one set lying completely inside another - with some kind of skin separating them - however thin it gets.
	X::Sets, 
	inside::@(@X,@X),
	|-0 inside 0 and X inside X,
	|-(==>;inside;==>) ==>inside,
	|-inside ==> ( ==>),
	|-For all A,B,C,D:@X(if A inside B and C inside D then A&C inside B&D),
	|-For all A,B:array I of @X (if for all i:I(A(i) inside B(i)) then |A inside |B).
()|- CLOSED and Net{ closed:={B||(X~B) inside (X~B)} }.
}=::INSIDE.

INTERIOR::=Net{
X::Sets, 
interior::(monoid)(@X,&,0)->(@X,&,0).
 |-interior;interior=interior.
 |-For all A:@X(interior(A)==>A).
 |-interior(X)=X.
()|- OPEN(open=>{G:@X||int(G)=G}).
}=::INTERIOR.

NEIGHBOURHOODS::=Net{
X::Sets, 
n::=neighbourhoods::X->(@@X).
 |-For all x:X( (n(x),&) in semigroup).
 |-For all p:X, N:n(p)( p in N).
 |-For all p,N, some G:n(p)&@N, all g:G(N in n(g)).
()|-OPEN(open=>{G:@S||for all x:G(G in n(x)}).
}=::NEIGHBOURHOODS.

FINENESS::=Net{
	X1,X2::Spaces. 
	|-X1 finer X2 iff for G:open.X1(G in open.X2)
.Hole
}.

LIMITS::=Net{
Use TOPOLOGY.
|- {n..||n:Nat} in filter_bases(Nat),
 base for limits of sequences.
|- For X:Spaces, x:X, neighbourhoods(x) in filter_bases(X).
   Used for limits of functions at a point.
|- For X:Space, Y:@X, x0:close(Y), {Y&V||V in neighbourhoods(x0)}in filters(Y).

 For Y:Sets, \beta:filter_bases(Y), X:Spaces, f:Y->X,
	f ->[\beta,X] l::=for all V:(X.neighbourhoods)(l), some b:\beta.
		(f(B)==>V),
	f ->[\beta,X] l ::= `f tends to l along \beta in space X`.
Note. When there is no ambiguity the space (,X) is omitted).

 For X:Spaces, a:Nat->X,
 lim[n->oo]a[n] ::= the [l](a->[{n..||n:Nat}]l),
  l=lim[n->oo]a[n] iff for all V:neighbourhoods(l), abf n (a[n] in V).
(note. 'oo' is an arbitrary symbol, not necesarily a value in Nat, and 'abf' is 'short for 'all but a finite number of'.).

 For X,Y:Spaces, f:X->Y,
 lim[x->x0]f(x) ::= the [l](f->[X.neighbourhoods(x0)]l),

|- l=[x->x0]f(x) iff for all V:Y.neighbourhoods(l), some W:X.neighbouhoods(x0), (if x in W then f(x) in V).

Similarly:
 {[x0..x0+\epsilon)||\epsilon>0} is a filter_base for lim[x->x0,x>=0]f(x).

Notice that {x0..x0+\epsilon)||\epsilon>=0} is not because [x0..x0) =0).
 {[a..)||a:Real} is a filter_base for lim[x->oo]f(x).

 For x0:close(Y), {Y&V||V in nieghbourhoods(x0)} is a base for lim[x->x0,x:Y].

 For X,Y:Spaces, x0:X, y0:Y, f:X->Y,
   W:X.fundamental_neighbourhoods(x0), V:Y.fundamental_neighbourhoods(y0),
    y0=lim[x->x0]f(x) iff for all v:V, some w:W(f(w)==>V).

Hausdorff spaces have unique limits (if any).
()|- For Y:Sets, \beta:filter_bases(Y), X:Spaces and Hausdorff, f:Y->X,
          0..1 l (f ->[\beta] l).
The limit of a function does not depend on what it does initially (where the filter is widest) but what happens later (inside the narrower confines of the filter):
()|- For Y:Sets, \beta:filter_bases(Y), X:Spaces, f:Y->X, B:\beta,
      \gamma={B&A||A in \beta},
          f ->[\beta] l iff f ->[\gamma] l.

. Adherence/Accumulation points.
Even though a function may not have a unique limit (at a point, as x->oo,...) it may still get close to one or more points while avoiding coming to a unique limit. For example fun[n]((-1)^n(1+1/n)) in Seq(Real) tends to `accumulate at` or `adhere to` both -1 and +1.

 For X,Z:Spaces, f:X->Z, Y:@X, x0:close(Y), \beta={Y&V||V in neighbourhoods(x0)}, z0:Z, adherence_value[\beta](f):={z:Z ||for all V:neighbourhood(z), W:neighbourhoods(x0), (f(W&Y) & Y)},

|- For X:sets, Y:Spaces and Hausdorff, \beta:filter_bases(X), f:X->Y,
    f ->[\beta] l iff l= the adherence_value[\beta](f).

|- For X:sets, Y:Spaces and Hausdorff, \beta:filter_bases(X), f:X->Y,
    adherence_value[\beta](f)=&{close(f(B))||B in \beta}.

}=::LIMITS.

. Continuity
CONTINUITY::=Net{
Continuous maps are not a topological morphism because continuity alone 
gives no guarantee that a structure is preserved when the mapping is 
applied - in fact the reverse is true - continuity implies that properties
in the  domain of the map are implied by properties in the codomain. 
Continous maps form a category but without uniqely defined products and 
coproducts.
(C) ::=(Continuous)::=(Cont).
arrow::{->,>->,...},
X,Y::Spaces, 
p::X.
(Cont)X arrow Y::={f:(X arrow Y || for all A:@X( f(close(A))==>close(f(A) )},
This is not the text book definition  but is equivalent to it.
\swashC(X,Y) ::=(Cont)(X->Y) - This notation is often used in text books.

A easily understood definition of continuity at a point  is that the limit of the function at that point is the value of the function at that point:

 For all f:(Continuous(x0))X arrow Y iff f:X arrow Y and f ->[x0] f(x0).

In the vernacular: `If it looks like its going there, then it gets there.`.
(C(p)) ::=(Continuous(p))::=(Continuous(p))::=`Continuous at p`,

(Continuous(p))X arrow Y={f:X arrow Y||for all A:@X( if p in X.close(A) then f(p) in f(A))},

()|- for all p:X (Cont)==>(Cont(p)).

()|- for all f:X->Y, (f in Continuous iff for all A,B:@Y(if A inside B then /f(A) inside /f(B)).

()|- for f:X->Y, f in continuous iff for all x, some F:fundamental_neighbourhoods(f(x)), all V:F(/f(V)in open_neighbourhoods(x)).

()|- For f:(Cont)X->Y,
 For all G:open(Y) (/f(G) in open(X))
 and for all G:closed(Y) (/f(G) in closed(X))
 and for all A:@X (f(close(A))==>close(f(A)))
 and for all B:@Y (close(/f(B))==>/f(close(f(B)))
 and for all B:@Y (/f(interior(B))==>interior(/f(B)))
 and for all A,B:@Y (if A inside B then /f(A) inside /f(B))
 and ? for all A:connected(Y) (f(A) is connected)
 and for all A:compact(X) (f(A) in compact(Y) )
 and for all x:X,  N:neighbourhoods(f(x)) (/f(N) in neighbourhoods(x)).

()|- For f:>X->Y, g:Y->Z, if f,g in Cont then f;g in Cont.

()|- Id(X) is (Cont)X->X.

()|- CATEGORY(Spaces,Continuous).

 |-For f:>X->Y, g:Y->Z, if f in Cont(x0), g in Cont(f(x0)) then f;g in Cont(x0).

}=::CONTINUITY.

. Morphisms
TOPOLOGICAL_MORPHISMS::=Net{

 For X,Y::Spaces, 
arrow::Arrows, 
F::@@X|@@Y,   (F is typically open, closed,...),

(F)X arrow Y ::={f:X arrow Y|| for all A:@X(if A in F then f(A) in F)}.

(topological) ::=(Closed)&(Continuous).

Hom(X,Y) ::=homeomorphisms(X,Y)::={f:(Cont)X---Y || /f in (Cont)Y---X}.

()|- homeomorphism<>Continuous && (1)-(1).

()|- For F:X---Y, f in Hom(X,Y)
    iff f,/f in Cont
    iff (for all A:@X(X in open iff f(X) in open)
    iff (for all A:@X(X in close iff f(X) in close).

()|- homeomorphisms(X,Y)=(topological)X---Y.

()|- if compact then homeomorphisms=continuous & (1)-(1).

Example - stereographic projection of a sphere onto a plane.
()   |- for p:sphere[n], (topological) (sphere[n]~{p})---R^(n).

}=::TOPOLOGICAL_MORPHISMS.

. Subspaces and relative topologies

SUBSPACE::=Net{
	|-TOPOLOGY(X), 
	Subset::@X.
	Y:=Subset.
	|-TOPOLOGY(Y,close=>[B:@Y](Y & X.close(B))
	()|- Y.open={G&Y||G:X.open}.
}=::SUBSPACE.

 For X:Space, subspaces(X) ::=$SUBSPACE.$Subset.

|- for X:Spaces, Y:subspaces(X)(Y.open in open_family(Y) and Y ==> X).

 For X,Y:Spaces, (topology)X==>Y::=X in  subspaces(Y).

Many properties are propagated from space to subspace:

|- For X,Y, (topology)X==>Y,
	X.closed={C&X||C:Y.closed},
	X.neighbourhoods=[x]{N&X||N:Y.neighbourhoods(x)},
	if Y.Hausdorff then then X.Hausdorff,
	For I:Sets, \beta:fbase(I), f:I->X, l:X(f ->[\beta,X]l iff f->[\beta,Y]l).
	For T:Spaces, f:T->X(f in Continous(X) iff continuous(Y),
	Id(X) in (continuous.Y)X->Y.

|- For X:Spaces, Y:@X, Y.discrete iff for all y:Y(y in isolated.Y).

|- subspace in Transitive(Spaces).

. Embedding.
??|- (topology)X-->Y iff for some Z((topology)X---Z and Z subspace Y).

. Quotient Topology.

QUOTIENT_TOPOLOGY::=Net{
|-TOPOLOGY(X).
R::equivalence_relations(X).  `Glueing things together`
\phi::=[x]x/R.
quotient_topology is the finest topology with \phi in (continous)X>==X/R.
|-TOPOLOGY(X=>X/R,open=>{A||A./\phi in open(X)},...).
}=::QUOTIENT_TOPOLOGY.

. Basies.
TOPOLOGICAL_BASIS::=Net{
S::Sets, 
basis::covers(S), 0 in basis.
 For all A:finite(basis)(&A in basis).
generate_open::=[B:@@S]{|(A)   ||  A:@B}.
|-OPEN and Net{open=generate_open(basis)}.
}=::TOPOLOGICAL_BASIS.
.
ORDERED_TOPOLOGY::=Net{
|-Toset(X,<=).
|-TOPOLOGICAL_BASIS, 
|- basis={u..v ~{u,v}||u,v:S}.
()|- for all u,v(u..v=close(u..v not {u,v})).
}=::ORDERED_TOPOLOGY.

ADIC::=Net{ 
p::Integer, 
S::=Integer, 
|-neighbourhoods=[n]{n+s*p^r||r:Nat0, s:Integer

.Hole
}=::ADIC.

INITIAL::=Net{
I::Sets, 
Y::I->$TOPOLOGY, 
X::Set, 
Z::$TOPOLOGY.

 For i:I, f[i]::X->Y(i), \alpha:`coarsest topology on X such that` for all i(f[i] in continuous).

|- for all g:(continuous???.

.Hole
}=::INITIAL.

FINAL::=Net{
I::Sets, 
Y::I->$TOPOLOGY, 
X::Set, 
Z::$TOPOLOGY.

 For i:I, f[i]::Y(i)->X, \beta:`finest topology on X such that` for all i(f[i] in continuous).

|- \beta={U||for all i (/(f[i])in open)}.
}=::FINAL.

. Product of Spaces
PRODUCT_SPACE::=Net{

 For Family:{open,closed,...}, elementary(Family) ::={(U><V):@(X><Y)|| U in Family(X) and V in Family(Y)}).
|-TOPOLOGY(X).
|-TOPOLOGY(Y).

()|- TOPOLOGY(X><Y, open=>{U:@(X><Y)||some eo:elementary(open)|U=|(eo)}).
}=::PRODUCT_SPACE.

. Sums of Spaces

SUM_SPACE::=Net{
|-TOPOLOGY(X).
|-TOPOLOGY(Y).
|-{X,Y} in open & partitions(X|Y).
}=::SUM_SPACE.

.Close Topology