Showing changes from revision #16 to #17:
Added | Removed | Changed
This entry is about a generalized notion of topology. For the notion of formal space in the sense of rational homotopy theory, see formal dg-algebra.
Context
Topology
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Introduction
Basic concepts
-
open subset, closed subset, neighbourhood
-
topological space, locale
-
base for the topology, neighbourhood base
-
finer/coarser topology
-
closure, interior, boundary
-
separation, sobriety
-
continuous function, homeomorphism
-
uniformly continuous function
-
embedding
-
open map, closed map
-
sequence, net, sub-net, filter
-
convergence
-
category Top
Universal constructions
Extra stuff, structure, properties
-
nice topological space
-
metric space, metric topology, metrisable space
-
Kolmogorov space, Hausdorff space, regular space, normal space
-
sober space
-
compact space, proper map
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
-
compactly generated space
-
second-countable space, first-countable space
-
contractible space, locally contractible space
-
connected space, locally connected space
-
simply-connected space, locally simply-connected space
-
cell complex, CW-complex
-
pointed space
-
topological vector space, Banach space, Hilbert space
-
topological group
-
topological vector bundle, topological K-theory
-
topological manifold
Examples
-
empty space, point space
-
discrete space, codiscrete space
-
Sierpinski space
-
order topology, specialization topology, Scott topology
-
Euclidean space
-
cylinder, cone
-
sphere, ball
-
circle, torus, annulus, Moebius strip
-
polytope, polyhedron
-
projective space (real, complex)
-
classifying space
-
configuration space
-
path, loop
-
mapping spaces: compact-open topology, topology of uniform convergence
-
Zariski topology
-
Cantor space, Mandelbrot space
-
Peano curve
-
line with two origins, long line, Sorgenfrey line
-
K-topology, Dowker space
-
Warsaw circle, Hawaiian earring space
Basic statements
Theorems
Analysis Theorems
topological homotopy theory
Idea
Formal topology is a programme for doing topology in a finite, predicative, and constructive fashion.
It is a kind of pointless topology; in the context of classical mathematics, it reproduces the theory of locales rather than topological spaces (although of course one can recover topological spaces from locales).
The basic definitions can be motivated by an attempt to study locales entirely through the posites that generate them. However, in order to recover all basic topological notions (particularly those associated with closed rather than open features) predicatively, we need to add a ‘positivity’ relation to the ‘coverage’ relation of sites.
Definitions
A formal topology or formal space is a set together with
such that
- whenever and ,
- whenever ,
- whenever and for all ,
- whenever or ,
- whenever and ,
- ,
- for some whenever and , and
- whenever if ,
for all , , , and .
We interpret the elements of as basic opens in the formal space. We call the entire space and the intersection of and . We say that is covered by or that is a cover of if . We say that is positive or inhabited if . (For a topological space equipped with a strict topological base , taking these intepretations literally does in fact define a formal space; see the Examples.)
Some immediate points to notice:
- If we drop (1), then the hypothesis of (1) defines an equivalence relation on which is a congruence for , , , and , so that we may simply pass to the quotient set. In appropriate foundations, we can even allow to be a preset originally, then use (1) as a definition of equality.
- We can prove that is a bounded semilattice; if (as the notation suggests) we interpret this as a meet-semilattice, then if and only if . Conversely, we could require that be a semilattice originally, then let (1) say that whenever .
- We can prove that holds iff every cover of is inhabited and that fails iff . Accordingly, this predicate is uniquely definable (in two equivalent ways, one impredicative and one nonconstructive) in a classical treatment; only in a treatment that is both predicative and constructive do we need to include it in the axioms. See positivity predicate.
Examples
Let be a topological space, and let be the collection of open subsets of . Let be itself, and let be the literal intersection of and for . Let if and only is literally an open cover of , and let if and only if is literally inhabited. Then is a formal topology.
The above example is impredicative (since the collection of open subsets is generally large), but now let be a base for the topology of which is strict in the sense that it is closed under finitary intersection. Let the other definitions be as before. Then is a formal topology.
More generally, let be a subbase for the topology of , and let be the free monoid on , that is the set of finite lists of elements of (so this example is not strictly finitist), modulo the equivalence relation by which two lists are identified if their intersections are equal. Let be the empty list, let be the concatenation of and , let if the intersection of is contained in the union of the intersections of the elements of , and let if the intersection of is inhabited. Then is a formal topology.
Let be an accessible locale generated by a posite whose underlying poset is a (meet)-semilattice. Let and be as in the semilattice structure on , and let if contains a basic cover (in the posite structure on ) of . Then we get a formal topology, defining in the unique way.
The last example is not predicative, and this is in part why one studies formal topologies instead of sites, if one wishes to be strictly predicative. (It still needs to be motivated that we want at all.)
In dependent type theory
In dependent type theory , if let one doesn’t have a be the type of all propositions , then and one let usually the cannot define a relation between a type and for the type of all subtypes of , which and is necessary for defining the coverage . Instead, as one has to use aTarski universe to define the type of all locally -small subtypes of , and use that to define a locally -small formal topology on .
Let be a Tarski universe, and let be the type of all propositions in
The singleton subtype function is a function , such that for all elements , , and for all functions such that for all elements , , the type of functions is contractible for all and .
which A comes with anembeddingformal topology orformal space . In is addition, a we define the relationtype for and together with as
The singleton subtype function is a function , such that for all elements , , and for all functions such that for all elements , , the type of functions is contractible for all and .
Given a Tarski universe , a locally -small formal topology or locally -small formal space is a type together with
such that
- For all elements and , the canonical function
is an equivalence of types.
- For all elements and subsets , if , then
- For all elements and subsets and , if and for all elements , and , then
- For all elements and and subsets , if or , then .
- For all elements and subsets and , if and , then
- For all elements , ,
- For all elements and subsets , if and , there exists an element such that and .
- For all elements and subsets , if implies , then .
References
-
Mike Fourman and Grayson (1982); Formal Spaces. This is the original development, intended as an application of locale theory to logic.
-
Giovanni Sambin (1987); Intuitionistic formal spaces; pdf.
- This is the probably the main reference on the subject.
- Warning: you can ignore the material about foundations and type theory, but if you do read any of it, the term ‘category’ means (roughly) proper class; this was common in type theory in the 1980s.
-
Giovanni Sambin (2001); Some points in formal topology; pdf. This has newer results, alternative formulations, etc.
-
Erik Palmgren, From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory, Logicism, Intuitionism, and Formalism Volume 341 of the series Synthese Library pp 237-253, 2005 (pdf)