formal topology

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.



topology (point-set topology, point-free topology)

see also differential topology, algebraic topology, functional analysis and topological homotopy theory


Basic concepts

Universal constructions

Extra stuff, structure, properties


Basic statements


Analysis Theorems

topological homotopy theory

Formal topology


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.


A formal topology or formal space is a set SS together with

such that

  1. a=ba = b whenever a{b}a \lhd \{b\} and b{a}b \lhd \{a\},
  2. aUa \lhd U whenever aUa \in U,
  3. aVa \lhd V whenever aUa \lhd U and xVx \lhd V for all xUx \in U,
  4. abUa \cap b \lhd U whenever aUa \lhd U or bUb \lhd U,
  5. a{xy|xU,yV}a \lhd \{ x \cap y \;|\; x \in U,\; y \in V \} whenever aUa \lhd U and aVa \lhd V,
  6. a{}a \lhd \{\top\},
  7. x\Diamond x for some xUx \in U whenever a\Diamond a and aUa \lhd U, and
  8. aUa \lhd U whenever aUa \lhd U if a\Diamond a,

for all aa, bb, UU, and VV.

We interpret the elements of SS as basic opens in the formal space. We call \top the entire space and aba \cap b the intersection of aa and bb. We say that aa is covered by UU or that UU is a cover of aa if aUa \lhd U. We say that aa is positive or inhabited if a\Diamond a. (For a topological space equipped with a strict topological base SS, taking these intepretations literally does in fact define a formal space; see the Examples.)

Some immediate points to notice:


Let XX be a topological space, and let SS be the collection of open subsets of XX. Let \top be XX itself, and let aba \cap b be the literal intersection of aa and bb for a,bSa, b \in S. Let aUa \lhd U if and only UU is literally an open cover of aa, and let a\Diamond a if and only if aa is literally inhabited. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

The above example is impredicative (since the collection of open subsets is generally large), but now let SS be a base for the topology of XX which is strict in the sense that it is closed under finitary intersection. Let the other definitions be as before. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

More generally, let BB be a subbase for the topology of XX, and let SS be the free monoid on BB, that is the set of finite lists of elements of BB (so this example is not strictly finitist), modulo the equivalence relation by which two lists are identified if their intersections are equal. Let \top be the empty list, let aba \cap b be the concatenation of aa and bb, let aUa \lhd U if the intersection of aa is contained in the union of the intersections of the elements of UU, and let a\Diamond a if the intersection of aa is inhabited. Then (S,,,,)(S,\top,\cap,\lhd,\Diamond) is a formal topology.

Let XX be an accessible locale generated by a posite whose underlying poset SS is a (meet)-semilattice. Let \top and \cap be as in the semilattice structure on SS, and let aUa \lhd U if UU contains a basic cover (in the posite structure on SS) of aa. Then we get a formal topology, defining \Diamond 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 \Diamond at all.)