An apartness space is a set equipped with an “apartness relation” that distinguishes between pairs of points or sets. They are particularly interesting in constructive mathematics; in classical mathematics they tend to be equivalent to better-known definitions expressed in terms of “closeness” rather than “apartness”.
There are actually several different notions of “apartness space” depending on whether the objects being compared on each side are points or sets.
A point–point apartness space is a set equipped with an apartness relation, usually written on elements . Sometimes it is required to be tight, or to be only an inequality relation.
A point–set apartness space is a set equipped with a relation between points and subsets , satisfying appropriate axioms. In classical mathematics, these axioms are obtained by contraposition from the definition of a topological space in terms of a right exact Moore closure operator, so that point–set apartness spaces are equivalent to topological spaces. In constructive mathematics … well, keep reading.
A set–set apartness space is a set equipped with a relation between subsets , satisfying appropriate axioms. A set–set apartness space is one of the ways to describe the classical notion of a proximity space. In constructive mathematics, the definition of a proximity space in terms of can be taken as a definition of a set–set apartness space.
A uniform apartness space is a set equipped with a collection of “co-entourages”, each giving a different notion of when two points are apart, satisfying appropriate axioms. In classical mathematics, the co-entourages are exactly the complements of the entourages of a uniform space, and the same is true constructively if the space is uniformly regular.
Since point–point apartness spaces are described at apartness relation, set–set apartness spaces at proximity space, and uniform apartness spaces at uniformly regular space, the rest of this page will be about point–set apartness spaces.
An apartness space is a set equipped with a relation between points and subsets such that
The relation should be regarded as a “positive” way of saying that does not belong to the closure of , i.e. . Under this interpretation, the above axioms contrapose to become
which are precisely the axioms of a topology expressed in terms of a closure operator. In constructive mathematics, of course, the law of contraposition does not hold.
The axiom is almost unnecessary, since the last axiom ensures that if for any set then . In particular, this is the case if is (see below) and for any there is a with .
The above definition is almost exactly that of a “pre-apartness” from BV11. The differences are (1) they require to be inhabited (which category-theoretically is wrong-headed, since it excludes the initial object), and (2) they assume that is given with an ambient inequality relation that is referred to by the symbol in axioms 2 and 4. (If is the denial inequality, then these axioms can be written more simply as “if then ” and “if then ”.) Note that if the space is (see below) then this ambient inequality is definable in terms of as . For an “apartness”, BV11 also require comparability (see below).
Axiom 4 is phrased in BV11 as “if , then . This is equivalent to our version, since is the largest set satisfying .
The earlier paper BSV02 omits the axiom , and phrases axiom 2 with the denial inequality but axiom 4 with an ambient inequality — although these are probably oversights — and requires as part of the definition too (see below). An earlier, more predicative presentation of “apartness spaces” can be found in Waaldijk.
Any apartness space comes with an irreflexive relation defined by iff . This is a positive version of the negation of the specialization order. A topological space is called (see separation axioms) if its specialization order is discrete, i.e. ; thus an apartness space is called if .
We could contrapose this to obtain , but it is usually too strong constructively to have a denial statement imply a positive one. However, if we replace with a given apartness relation or inequality relation other than the denial inequality, then we obtain an axiom that is a purely positive version of . Note that if is tight, then this statement implies the negative version of , while conversely if is symmetric (see below) then the negative version of says precisely that is tight.
Note that axiom 2 implies the converse , so that if the axioms and the property are stated with reference to some ambient inequality , then can be defined in terms of . If we define in this way, then axiom 2 should be stated in terms of the denial inequality (thereby asserting that this relation is irreflexive).
If one wants the relation to be symmetric and thus an “inequality relation” one needs to assert this separately. An apartness space with this property is naturally called , or perhaps strongly , since it implies (and classically is equivalent to) the topological property called that the specialization order is symmetric (see separation axioms).
However, stating axiom 4 in terms of the -derived inequality is weaker, even in classical mathematics, than stating it in terms of the denial inequality. For instance, if with the only nonempty apartness relations and , then axiom 4 for the denial inequality fails for , since which is not apart from ; but stated in terms of the -derived inequality it holds, since . This is a pretopological space that is not a topological space; thus only axiom 4 with the denial inequality (or at least a tight inequality, which classically becomes equivalent to denial) gives a notion of point-set apartness space that reduces classically to ordinary toplogical spaces. In BV11, axiom 4 for the denial inequality is called the reverse Kolmogorov property.
An apartness space may be called comparable (nonce definition on this page) if implies for any , where might also be a given apartness on . This condition is classically trivial, and generalizes the comparison axiom on a point–point apartness relation. In particular, if denotes the relation defined above, then this property implies that is a comparison, and hence (if the space is also , so it is symmetric) an apartness relation. It is also related topologically to Penon’s definition of intrinsic open subset in synthetic topology and to the natural topology on a point-point apartness space, and can be viewed as a very weak version of regularity.
An apartness space is locally decomposable if whenever , there exists a set such that and every satisfies either or . This condition is also classically trivial: take . It implies comparability (for the denial inequality).
If is a topological space, we define if there is a neighborhood of disjoint from , or equivalently if the complement of is a neighborhood of . This makes an apartness space. Only the last axiom is somewhat nontrivial: if with open and , and , then since we have too, so .
Conversely, if is an apartness space, define to be a neighborhood of if there is a set such that and . This makes a topological space. Again the nontrivial part is the “transitivity” of neighborhoods, i.e. that if is a neighborhood of then so is is a neighborhood of . To see this, if and , then is a neighborhood of any point with , so it suffices to show that is a neighborhood of ; but this is obvious.
If we order the topologies on by if (i.e. is finer than ), and the apartnesses by if , then these constructions define monotone functions and respectively. Moreover, we have:
The above functions exhibit the poset of apartnesses on as a reflective sub-poset of the poset of topologies on : we have and .
For the former inequality, if is open in , then for every there is a set such that and . Since , there is an open set with and . But then every satisfies , hence ; so . Thus is open.
For the latter equation, if , then to show we must construct an open set with and ; but it suffices to take . Conversely, if , then there is an open set with and . By definition, and mean there is a set with and . And by the last axiom of an apartness space, to show it suffices to show ; but this follows since and .
In other words, an apartness space can be regarded as a well-behaved kind of topological space: one in which for every open neighborhood of a point there is a set and an open neighborhood of such that and contains the interior of the complement of . Note that is then in the interior of the complement of , and if is in the interior of the complement of then the latter is such a . Thus, the condition can equivalently be phrased as: for every open neighborhood of , there is a set such that . In other words, the interiors of complements form a base for the topology. In Bridges et. al. this condition is called being topologically consistent.
A sufficient condition for topological consistency is local decomposability. This was defined above for apartness spaces; more generally, a topological space is said to be locally decomposable if for every open neighborhood of there is an open neighborhood of such that , i.e. every satisfies . This implies that , giving topological consistency. (Of course, in classical mathematics every space is locally decomposable.)
In contrast to the above theorem, it is not quite justified to say that the category of apartness spaces is a subcategory of the category of topological ones. It is most natural to say that a function between apartness spaces is continuous if for all and , if then . It is true that if and are topological spaces and is topologically continuous, then it is apartness-continuous in this sense for the induced apartnesses. For if , then for some open set disjoint from ; topological continuity of then gives that is an open set containing and disjoint from , so that . Thus we do have a functor .
However, a continuous map between apartness spaces in the above sense apparently need not be continuous for the induced topologies; but this is true if is locally decomposable. For if is open and , we have a set such that and implies , and by local decomposability gives a such that and every satisfies either or . Let ; if , we have and hence , so and thus and . Moreover, since we have by apartness-continuity. Thus, is open.
Thus, the category of locally decomposable apartness spaces is equivalent to the category of locally decomposable topological spaces.
Notions of “apartness space” based on a presentation in terms of basic opens, somewhat akin to formal topology, were developed in:
The above definition in terms of an apartness relation between points and subsets is slightly adapted from the version given in:
Last revised on January 20, 2017 at 18:15:06. See the history of this page for a list of all contributions to it.