Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created apartness space.
Nice, but given its coverage, shouldn't point-point apartness space and set-set apartness space redirect to apartness relation and proximity space, respectively?
Maybe; if you think so, feel free to change it.
Done, making sure that these targets have the redirect appropriately in bold somewhere.
I also edited the main part of apartness space (after the discussion of all of the varieties) to reflect that point–set is the default notion on that page.
The distribution of these notions to pages feels a bit odd and haphazard — why are point-point and set-set apartness spaces discussed on pages with other names, but point-set apartness spaces aren’t? — but I can’t think of anything more logical to do.
Classically, point–set apartness spaces are simply topological spaces, so we could discuss them at topological space; similarly, point–point apartness spaces are classically just setoids, so we could discuss them at setoid. However, these are big topics even classically, and their relatively minor twisted constructive versions would get lost. For set–set apartnesses, however, both the classically equivalent notion of proximity space and the constructive aspects of the set–set apartness are rather obscure, so it works fine to put everything at proximity space, at least for now.
Note that both point–point apartness spaces and point–set apartness spaces get their own articles: apartness relation and apartness space, respectively. The way that these words are used is somewhat arbitrary, but it does reflect the difference in emphasis. For a point–point apartness, the emphasis is on the relation, and the topological aspects are secondary; indeed, classically, the topological aspects are trivial. (Note also that setoid redirects to equivalence relation; that is basically the same phenomenon as redirecting point–point apartness space to apartness relation.) But for a point–set apartness, there's a lot more to say about how it behaves as a space; classically, these topological aspects are the whole point. Thus the page titles make sense to me, although they should come with warnings.
Yeah, I agree with the reasoning; it just doesn’t feel “clean” to me. (-:
I added the missing nullary-unions axiom to the definition at apartness space.
I added a discussion of the relationship of point-set apartness spaces to topological spaces: locally (on each set) the apartnesses are a reflective sub-poset of the topologies, but globally not every apartness-continuous map may be topologically continuous.
I finally got a copy of the Bridges-Vita book cited at apartness space, and updated the page with reference to their definitions, which are actually closer to ours than those of the earlier BSV paper.
I do still believe that it is silly to equip a point-set apartness space with a separate point-point inequality/apartness relation rather than just defining to mean , especially since the BV axioms make the ambient inequality coincide with this in any point-set apartness space. The latter may not be symmetric, but if you want it to be, you’re just assuming your space is , which is reasonable (but an extra assumption). Moreover, I believe that the “transitivity” axiom should be stated in terms of the denial inequality; stating it in terms of seems too weak even in classical mathematics (though I haven’t come up with a concrete example yet).
I don't like your nonce use of ‘comparable’, since that also means (said of a pair of elements of a partial order). I have long found it annoying that there seems to be no standard adjective to go with ‘comparison’, but if we're going to invent one, then I'd prefer ‘comparative’ or ‘comparing’. (Where you write ‘comparability’ later on, that should surely be ‘comparison’ I was hoping that ‘comparative’ was spelt ‘comparitive’ to fit that better, but no such luck.)
Are you sure that it's right that means
I would expect that if is a positive apartness relation itself, but if I'm thinking of as defining the only positive apartness (or quasi-apartness) relation between points, then I would expect
instead. That is, the quasi-apartness is (besides being symmetric, which I guess now needs to be stated separately) tight.
I guess that what I'm really saying here is that
makes sense if you already have an inequality and you want to say that the apartness structure is - (or -Fréchet to use more words and fewer symbols). But if you're using the denial inequality, then
sounds too strong. That something (in this case, the equality of and ) is false shouldn't be enough to imply a positive result (in this case, that is apart from ). I mean, we shouldn't need Markov's Principle to prove that the real line is .
So simply should be
or rather, should be symmetry of , should be
and should be .
But if is a tight inequality, then
is a stronger, -relevant statement that entails . (And
is the stronger, -relevant statement that entails .)
I agree entirely with #12-13; I had actually come to the same conclusion independently but hadn’t updated the article. The “stronger, -relevant statement that entails ” I think it would make sense to call -. I would be inclined to call symmetry of something like “strong ”, since while these and are actually equivalent to the standard properties for the corresponding topology, symmetry of is I think appreciably stronger than topological , which is symmetry of , the specialization preorder.
I don’t like the word “comparable” either. At the time I wrote it, I didn’t have a better idea, but now I would suggest something like “weakly locally decomposable” or maybe “pointwise locally decomposable”. For a proximal or syntopogenous apartness space, the general relation that I’m inclined to call “decomposability” is that if then there are a and such that and and . Local decomposability is the restriction to the case , and in the left-perfect case we may as well take . “Weak local decomposability” is then what we get by weakening the assumption to a pointwise statement (or, in the denial case, ), in which case we may as well take . What do you think?
I like the name “quasi-apartness relation”, meaning I assume an irreflexive comparison. I have been playing around with a weaker notion that I’ve been calling an “anti-preorder”: an irreflexive relation satisfying . This is the anti-specialization-preorder that you get from a point-set apartness space that isn’t even weakly locally decomposable, and it’s also the same as a principal anti-uniform space with the new definition (which I haven’t managed to put on that page yet either).
I also just added to apartness space a simple example showing that axiom 4 written with a non-denial inequality is strictly weaker, even classically (unless the inequality is assumed to be tight, which of course classically forces it to coincide with denial). Bridges+Vita call axiom 4 for the denial inequality (well, something equivalent to it) the “reverse Kolmogorov property”.
Ok, I fixed at apartness space.
I’m worried that the whole theory of point-set apartness spaces seems rather example-free. So far the only examples I can think of are:
I can’t even show that any anti-uniform space has an underlying point-set apartness space. So what exactly is the point of this theory?
I don't know, I kind of assumed that it was of interest since it gets listed along with point–point and set–set apartnesses, but maybe it's just thrown in to cover all possibilities.
Bridges et al certainly seem interested in it — there’s a whole chapter in their book about it — but they don’t include any non-topological examples as far as I can see.
Here are three possible transitivity axioms for a point-set apartness space, all classically equivalent:
(1) is the one on the page now, taken from Bridges-Vita. As noted above, I don’t know how to prove it from an anti-uniform space. However, (2) does follow from the transitivity axiom of an anti-uniformity, while (3) follows from the dual of that transitivity axiom (which possibly should also be part of the definition of anti-uniformity). Note that (2) says that if then is apart from the (weak) closure of in the apartness topology. Also, (1) is a specialization of the transitivity axiom for at proximity space to the perfect case, while (3) is a similar specialization of its dual. It’s not clear to me at present whether any of these axioms implies any of the others.
And here’s another even weaker one, implied by (1) and (3):
(4) If , there exists such that and for .
Together with (1) and (3), these result from weakening the disjunction in local decomposability in various ways, from to or or the weakest .
Slightly OT, but I found the discussion here on separation axioms interesting (and curious to know how things go when passing to a constructive setting)
As far as analysis goes, sure, (which this writer calls ‘complete regularity’) is what you need. I have no objection to that cutoff between lower and higher. I think that a lot of the time you hear a lot about Hausdorffness simply because, at least in analysis, all of your spaces are already completely regular (which I guess that this writer would call ‘complete regularity of the quotient’) and is the most well-known concept between and (possibly for historical reasons having to do with Bourbaki's dropping that axiom from Hausdorff's original definition of topological space, so that for a while one had to make a big point about whether one was assuming it or not).
But the writer loses me when they start talking about all of the extra structure that you can only put on a space. I guess that they've never heard of preproximity spaces (which are called simply ‘proximity spaces’ by some authors, as we've discussed here) and quasiproximity spaces, uniform convergence spaces and quasiuniform spaces, and so forth.
Interesting post. I think the fact that complete regularity is the boundary between quasiproximity/quasiuniformity and proximity/uniformity proper suggests that a more evocative name for the “lower/higher” distinction would be “asymmetric/symmetric”. That is, the topology of completely regular spaces is “symmetric topology”, while that of arbitrary spaces is “asymmetric topology”.
It also suggests that constructively, the appropriate version of “complete regularity” would be one that maintains this meaning. For this purpose I quite like the notion of “strongly regular” in this paper, which is essentially by definition the existence of a (finest) proximally-regular (or “decomposable”) proximity compatible with the topology. Though they don’t use that terminology for some reason (maybe they don’t know about proximities? Proximities seem to be under-appreciated in the point-free topology community.)
That is, the topology of completely regular spaces is “symmetric topology”, while that of arbitrary spaces is “asymmetric topology”.
Well, ‘symmetric topology’ is already a term in the literature for an topology, that is a topology whose specialization preorder is symmetric. (But here, ‘topology’ is used in the sense of a structure on a set, not a field of mathematics.) Incidentally, the ‘R’ in ‘’ stands for ‘regular’; that is, this notation is meant to suggest that it should be considered a weak regularity axiom. But we see that such a space is not symmetric in all respects, as the natural quasiuniformity on it, for example, is not symmetric.
I quite like the notion of “strongly regular”
Yes, that looks very nice! This seems to be the notion of complete regularity that I've been wanting, equivalent to being a subspace (in the sense of a sublocale, at least) of a compactum. (I notice that the paper is impredicative because it avoids Dependent Choice; if one accepted DC, then one could be predicative again.)
But if one accepts DC, then there is nothing wrong with the classical notion of complete regularity, is there?
If one accepts DC, then classical regularity is the same as strong regularity; so either way, strong regularity is the property that we want. But how to define it? With DC, a predicative definition is available; without DC, a predicative definition is not known. Of course, life is like that sometimes; you can't have everything.
Well, it's too much to say that one cannot define strong regularity at all, but one cannot define the relation . Instead, you say that a space is strongly regular if there exists an interpolative relation contained in such that …. (I've had some thoughts along that line myself, but I never pursued them, partly because I doubted that it would actually work!) And to judge from the proof on the bottom of page 4, it appears that the author did just that in an earlier paper (although one would have to check the details to see if it's all predicative).
What remains, however, is that one cannot define the relation predicatively; whereas , which can be defined predicatively, is of no interest without DC.
Come to think of, ‘has a uniformity’ should also be expressible predicatively (although, as far as I can see, not ‘has a [regular] compactification’, that is not directly).
Incidentally, I had thought that the usual term for what this paper calls ‘interpolative relation’ was ‘dense relation’, but I can only find references for ‘dense order’ (which means an interpolative quasiorder). (Well, ‘dense relation’ is on the Wikipedia page for dense orders, but marked [citation needed], and Google book search does not find it in the references for that page. Both terms also appear as neologisms with other meanings in other papers.)
ETA: (The subscript ‘’ is too small here, at least as I see it. But that's a font issue; the character here is correct, and it looks fine in Computer Modern.)
Makes sense. Something still seems off, though, because they claim (Proposition, p4) that in particular every uniform locale is strongly regular; but we know that constructively, not every uniform space is regular. Their proof of that direction cites another paper, which I don’t have in front of me to tell how constructive it is; but their use of in defining doesn’t fill me with confidence.
If they're using a constructive theory of uniform locales that we're ignorant of, then it might well incorporate uniform regularity, just as Bridges does for uniform point–set spaces. Do we have any reason to doubt that uniform regularity implies strong regularity?
I suppose that’s true. I think I believe that uniform regularity implies strong regularity for spaces. I’m a little dubious that it would work constructively for locales unless the locale is at least overt. I don’t know how to show that is interpolative otherwise, since the natural interpolating set is defined as an image under projecting away the locale itself, which won’t be open unless the locale is overt. Curi’s paper cited at uniform locale (which defines uniformities in terms of a “gauge of diameters”) requires overtness as part of the definition; but the Banaschewski-Pultr paper doesn’t mention overtness anywhere.
Another reason I’m doubtful of the constructivity of their other paper is that Picado & Pultr’s book on locale theory is relentlessly classical, despite the fact that on the cover they tout constructivity as one of the benefits of locale theory. Also, Curi’s paper, which is 4 years more recent than Banaschewski-Pultr, doesn’t cite any other work on constructive uniform locale theory more recent than Johnstone (Remark 3.3).
By coincidence I find I am writing a review of :ASYMPTOTIC RESEMBLANCE, by SH. KALANTARI AND B. HONARI, ROCKY MOUNTAIN JOURNAL OF MATHEMATICS Volume 46, Number 4, 2016. This looks at an analogue of proximity for coarse structures. I do not know if others have seen this.
Also relevant: Stone-Cech compactification of locales, III.
1 to 35 of 35