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.
Added a bit more to proximity space.
I rearranged this to give about equal emphasis to the three relations . Also more on quasiproximities and on the preorder implicitly involved in the definition of a separated proximity.
Our definition of proximity came from the one at the English Wikipedia, but I don't think that it's right, for two reasons:
So, I want to change this, but first I'll need to verify which assertions currently on the page assume Regularity and which do not. (There are some of each.)
They call it ‘normality’, and I can see why, but that doesn't really work. But it may be that complete regularity is a better analogue. ↩
I think the point is the theorem about proximities corresponding to compactifications. Won’t that fail if you omit regularity?
Yes, that is an example of an assertion that requires regularity; it's about completely regular spaces. So it has to be stated so.
On the other hand, the assertion that proximities correspond to simple symmetric syntopogenous spaces cannot require regularity. Our articles are wrong as they stand.
I guess one might make an argument that compactifications are a more important (and certainly more well-known!) concept than syntopogenous spaces, so it’s better for the terminology to coincide with them.
Yes, but nonregular (quasi)-proximities are good for more than just syntopogenous spaces. For example, given any pseudotopological space, let iff ; then this defines a quasiproximity which is regular if the space is topological. (This is different from the regular proximity defined by a completely regular topological space.)
I am coming around more to the view that Regularity is more fundamental (and so should probably get a different name). Assuming isotony, Reflexivity () and Regularity combine to form the following unbiased axiom:
If , then, for every , for some ,
(Changing If to Iff here (and being careful with the placement of ), we get a statement that precisely combines Reflexivity, Regularity, and Isotony, but this a rather obscure way to put Isotony, so it's probably best not to do this.)
Having Reflexivity without Regularity can be done, but it's like having reflexivity without transitivity (for a binary relation on a set), or having an identity without associativity (in a magma), or indeed having a pseudotopological space that is not a topological space (which is the same as the previous example for the ultrafilter monad, assuming the ultrafilter principle).
Yes, I agree.
It's interesting that Regularity is the one axiom that (when expressed using ) makes no reference to the lattice structure of the algebra of posets whatsoever; it simply states that is a dense order. (Well, that's thinking of as a quasiorder, which it actually is not, since it's not irreflexive, although it's not reflexive either. At least it is transitive, which is proved using Reflexivity and Isotony.)
There should be some analogy in which is like a ring and is like an ideal; is transitive but not reflexive for the same reason that an ideal is closed under binary multiplication but not unary [edit: this word should have been ‘nullary’ for the past 2½ years]. And in fact, can only be reflexive if it reduces to precisely, just an ideal with a unit must be the entire ring.
I've made that analogy precise, but now it seems that Reflexivity is very basic while Regularity is not. The usual notion of ideal in a poset is a generalization of ideal in a meet-semilattice, which is a commutative idempotent monoid, and which generalizes further to a sieve in a category. But the notion that I want here generalizes from monoids to categories and then specializes to posets.
Then an ideal in this sense is, first of all, a property of morphisms, that is of pairs where (writing for the arbitrary preorder). So it's a binary relation satisfying Reflexivity right off the bat. Then being a two-sided ideal means closure under composition with any morphism on either side, which is Isotony. Additivity and Regularity are then extra conditions.
Moving back to an ideal in a monoid (or a monoid in if that's more familiar), the analogue of Regularity is a condition that I've never seen before; it says that if is in the ideal then for some and in the ideal. A sort of mixed-up version of primality.
So I'm coming back to seeing Regularity as more optional. And even though there is a perspective in which Regularity goes with Reflexivity, still there are a lot of times when we use the nullary case of something without the binary case; it's the other way around that we really should avoid.
This all seems very interesting, but unfortunately I don’t have the time to think about it deeply right now. (-: Go ahead and rewrite the article however you like, but of course I would suggest mentioning up front that there are different opinions about which axioms are fundamental.
No wait, I'm not done!
Now instead of an ideal I want to think of it as a module. An ideal is a module equipped with module monomorphism to the unit module, but here in the world of posets every morphism is monic, so we just have a homomorphism to the unit module. This is nullary, and the binary partner is a homomorphism from the module to . So altogether, we have a coalgebra. (We may as well go ahead and call it a coassociative coalgebra; you can't tell in a poset.)
I like this better since a coassociative coalgebra is much more recognizable than an ideal with that weird mixed-up version of primality.
However, while the counit is precisely Reflexivity, the comultiplication is not quite Regularity. Rather than the property that, given , there is some such that , we have an operation that, given , gives us an equivalence class of such that , where is equivalent to if (and whatever follows from that). Classically, we can't tell the difference between that property and the existence of such an operation, but it should affect the morphisms.
ETA: Actually, additivity (on either side) makes these all equivalent. So while the general notion of coalgebra of a poset has this nontrivial structure, a quasiproximity doesn't.
I've written this up at proximity space#profunctors.
Since Regularity doesn't necessarily have any more to do with regularity than with normality, I've changed its name in the page to Normality, which at least appears in the literature. (Possibly Transitivity would be a better name, but more obscure.)
I also rearranged the definition so that we could easily discuss the possible variations in terminology. This meant move Separation back up to the main list. It was also convenient to bring in Todd's notion of topogeny, linking more clearly to syntopogenous spaces. Borrowing from syntopogenous spaces, I threw Perfection in as well, but maybe we don't need it.
Arguing further in favour of Regularity/Normality, I was wrong in #5 to say that the relation between proximities and syntopogenies is wrong if a proximity must satisfy this disputed axiom. I neglected to see that, while this axiom plays no role in the definition of a topogenous relation, it instead corresponds to the extra condition on a filter of topogenous relations to be syntopogeny! So we have been assuming Normality all along.
Ah, excellent. I was surprised if we’d missed something like that.
Now that I understand uniform regularity and local decomposability for uniform spaces and point-set apartness spaces, I’m coming back to think about proximity spaces and set-set apartness spaces.
In their notion of set-set apartness space, Bridges-Schuster-Vita assume Isotony, Additivity, Reflexivity, Symmetry, the weak constructive separation axiom that on the page apartness space I called “comparability”, the last axiom of a point-set apartness space, and another weird axiom that I don’t understand. All three of the latter axioms follow from the axiom that the page proximity space calls “Normality (constructive)” for , arguing further for its importance.
However, I really do object to calling it “Normalty”, since even classically a proximity space may not be a normal space. If the literature does that, then I would say that the literature is wrong. The axiom looks a bit like normality, but it fails to imply normality because (in a non-compact space) disjoint closed sets need not be apart. But it is definitely a kind of regularity, so by analogy with uniform regularity I am tempted to call it “proximal regularity”. The weird thing is that it seems to combine regularity with an analogue of the “ axiom” for uniform spaces, and while regularity is a separation axiom that can be left out of a definition, the latter is not.
Suppose we start from a uniform space (or a uniform apartness space) that is not uniformly regular. What can we prove about its underlying proximity structures?
It's called normality at https://www.encyclopediaofmath.org/index.php?title=Proximity_space. I think that I used that page as a reference for our page (it is cited at Wikipedia). It uses this despite recognizing its problems; here is a quotation: ‘The topology of a Hausdorff proximity is Hausdorff; on the contrary, a normal proximity is merely completely regular’. In light of the next sentence (‘Moreover, all completely-regular topologies are generated by a normal proximity’), maybe it should just be called complete regularity.
Let’s see, here’s the syntopogeny condition:
() For any , there exists a such that if have the property that whenever , either or , then .
I can think of three natural (classically-equivalent) ways to contrapose this to a condition on relations:
(1) For any , there exists a such that whenever , there exist and such that , , and .
(2) For any , there exists a such that whenever , there exist and such that , , and .
(3) For any , there exists a such that whenever , there exist and such that , , and .
The version of (1) in the “simple” case () is that currently appearing under “Normality (constructive)” at proximity space. Of course, (2) and (3) are equivalent if we have symmetry. On the other hand, under (left) perfection, in all three conditions we may as well take . Moreover, under perfection it is natural to also consider the weakened versions where is a singleton:
(1P) For any , there exists a such that whenever , there exists such that and .
(2P) For any , there exists a such that whenever , there exists such that and .
(3P) For any , there exists a such that whenever , there exists such that and .
In (3P) we also may as well take , giving the equivalent:
(3P) For any , there exists a such that whenever we have .
Similarly, I can think of two (classically-equivalent) ways to translate () into a condition on relations:
(1) For any , there exists a such that whenever , there exist and such that , , and .
(2) For any , there exists a such that whenever , there exist and such that .
Of course, in (2) it is equivalent to take :
(2) For any , there exists a such that whenever , there exists such that .
These two (constructively) equivalent versions of (2) are the ones currently appearing under “Normality (constructive)” and “Normality (simplified)” at proximity space. Under (left) perfection, we can take in both conditions, and then it is natural to also consider the restricted versions where is a singleton:
(1P) For any , there exists a such that whenever , there exists such that and .
(2P) For any , there exists a such that whenever , we have .
(continued…)
Now how are all these conditions related to known definitions? Consider first the case of a simple perfect syntopogeny (so or ), giving notions of topological space:
Condition (2P) is exactly the condition on a collection of neighborhood filters (a perfect topogenous order ) for it to define a topology. Moreover, in the perfect case, (2P) is equivalent to (2).
Condition (1P) implies (2P), so it defines an extra condition on a topological space. In fact it is precisely local decomposability.
Condition (1) implies (1P), so it also induces an extra condition on a topological space. But this condition seems too strong to be constructively reasonable: since every open set satisfies , it requires that every open set is complemented.
Condition (3P) is precisely Bridges-Schuster-Vita’s last axiom for a point-set apartness space. (Their phrasing is more complicated since they want to incorporate the possibility of a previously-given point-point apartness, but if the latter is the denial inequality then their condition reduces to (3P).) Moreover, in the perfect case, (3P) is equivalent to (3).
Condition (1P) is again precisely local decomposability for a point-set apartness space.
Condition (2P) also appears in Bridges-Schuster-Vita (Proposition 2.10), but they don’t give it a name. It’s a weaker version of local decomposability.
Condition (1) is unreasonably strong constructively: it implies that the basic opens are all complemented. Condition (2) is also too strong: it asserts that the basic opens are complements.
Now consider instead a biperfect symmetric syntopogeny, giving notions of uniform space.
Condition (1P) is the one that I used to define a uniform apartness space: Given a co-entourage , there is a co-entourage such that whenever , for any we have either or . In particular, it is true for the notion of apartness defined by a uniformly regular uniform space.
Conditions (2P) and (3P) (equivalent under symmetry) give a weaker axiom for uniform apartness spaces, equivalent to the stronger version under uniform regularity, and always satisfied by the complements of entourages of a uniform space (though the union axiom is, I believe, still not satisfied by those).
Conditions (2) and (3) seem stronger than (2P) and (3P), but are still always satisfied by the complements of entourages of a uniform space. For if is an entourage such that for all and , let be an entourage such that . With and we have and . And if is such that and for some , then for any we have since , a contradiction; thus .
I can’t make much sence of the right perfection condition stated for at proximity space, but it seems to me that in the biperfect case, a relation is essentially equivalent to a relation: to say that should be the same as saying for all . Under this translation, condition (2P) is just the usual condition in the definition of a uniformity, and is equivalent to (2).
Condition (1P), I believe, translates exactly to uniform regularity (combined with ).
Conditions (1) and (1) seem unreasonably strong: in addition to , they imply that all subsets of are almost located.
(continued…)
I think this analysis sheds some light on the uniform regularity / local decomposability conditions: the reason it’s unclear whether to include them as part of the definition or as extra properties is that they result from classically-equivalent ways to contrapose a statement. But if we want to keep the standard definition of “topological space” (rather than requiring all spaces to be locally decomposable), it seems that for consistency we should not include such conditions in the definition of point-set apartness space or uniform space.
Finally, this suggests that for set-set apartness spaces and proximal neighborhood spaces, we should not use (1) or (1) as the definition constructively, but rather (3) or (2). The observations above show that any uniform space has an underlying proximal neighborhood space satisfying (2), and if it is uniformly regular then it has an underlying set-set apartness space satisfying (3). (A non-uniformly-regular uniform space doesn’t even give rise to a point-point apartness space, so that requirement here isn’t so bad.)
As for a name for (3) and (2) in the definition, I would lean towards “transitivity”, because it would seem reasonable to call conditions (1) and (1) proximal regularity. Just like uniform regularity, they are classically automatic, but constructively ensure a stronger regularity property. As you say, it looks more like complete regularity, but it’s not exactly complete regularity of the underlying topological space; we still need countable choice to produce a real-valued function, in which case I think we get not just topological complete regularity but “proximal complete regularity”, i.e. a separating function that’s proximally continuous. So I would rather call it just “proximal regularity”; the corresponding “modulated” version that doesn’t require countable choice could then be “proximal complete regularity”.
One somewhat unfortunate fact is that the underlying proximity space of a uniformly regular uniform space apparently need not be proximally regular. I’m not sure exactly what to conclude from that.
A rule of thumb in constructive mathematics is to treat negation with suspicion; thus, (1) and (2) are the most natural. But one should also be suspicious of disjunctions in conclusions, since these may be too strong, and this is what you are claiming about (1). Letting every subset be located, even subsets such as for an arbitrary constant proposition , is way too strong.
Indeed, if the obvious simple structure on an inhabited metric space satisfies (1) , then the forbidden de Morgan law follows (hence LLPO, etc).
As you say, it looks more like complete regularity, but it’s not exactly complete regularity of the underlying topological space; we still need countable choice to produce a real-valued function
Well, I am looking for a deep underlying meaning of complete regularity that doesn't refer to . One would not expect this to match the usual definition without a bit of countable choice.
We should be able to get rid of the countable choice gap by asking for a “modulated” version, no?
Well, maybe, although the last time we tried that, we had some additional gaps. Besides which, if I'm looking for the deep inner meaning of complete regularity, I'm not sure that I want something so fiddly as a modulated property.
Well, I can’t see how to prove that even a metric space satisfies (1) or (1) constructively, so probably those are two strong. Here’s another possibility for “proximal regularity” that I think is implied by uniform regularity and implies ordinary regularity:
To get regularity, take to be open and consider the interiors of and . To get this from uniform regularity, if implies , take such that and such that , and let and and .
We could simplify the axiom by taking or .
Also, I don’t think I like the axiom for labeled “Symmetry (constructive)” at proximity space. It’s actually weaker constructively than the one labeled “Symmetry (simplified)” — its hypotheses ensure that and , so implies by isotony — and I can’t see any problem constructively with asserting the “simplified” version — it’s true in any uniform space, for instance. If anything, the “simplified” symmetry axiom for seems likely to be too weak, but I can’t think of any way to strengthen it that doesn’t amount to regularity.
I renamed “Normality” to “Transitivity” at proximity space, and added a remark about it to the Warnings about terminology.
I don’t like the notation for the complement of ; it’s too light and easy to miss for such a drastic operation. Can we switch to something like or at proximity space?
As for the “Transitivity (constructive)” row, its current entry for is boringly equivalent to the “simplified” version, while its entry for is too strong. My lengthy discussion above suggests removing this row entirely and changing the “simplified” version for (which is currently equivalent to my (2)) to my (3) by switching and .
For , I would also switch and in the “simplified” version (which in this case is stronger than the “constructive” one) to get “if for every either or , then ”. I think this is also true in any quasi-uniform space, where means : given an entourage , let be such that and ; then clearly , so , so we have (so that ) and also such that , hence .
Does that sound ok?
Go ahead and edit, and I'll bring it up if I don't like how it looks.
Okay, I have:
In topological spaces, dropping transitivity gives us pretopological spaces, and since some people do drop that from proximity spaces, we should name their objects of study, and I propose to call them ‘preproximity spaces’. That doesn't seem to be used in the literature except in some literature on fuzzy logic; the only problem is that this literature's abstracts suggests that ‘preproximity’ is used outside of their field (and in a way analogous to ‘preuniformity’, which is not what I want here); but if so, Google can't find it.
Anyway, I introduced that term to the article.
Thanks!
Back on #13-14, proximities as profunctors, I would think that if we are talking about -enriched profunctors then there is no extra structure to be gotten rid of, since composites of -enriched profunctors are just relational composites. Am I missing something?
I added some further remarks on the relationship between the three definitions constructively. It seems to me that contains strictly more information that , since the latter is determined by its restriction to complements, whereas the axioms of are just too strong to be reasonable. I haven’t been able to think of a way to define a in terms of that works for proximities (or more general syntopogenies), although there are point-based ways that work for point-set apartnesses and uniform apartnesses.
Oh! There is a way to define a proximity from a uniform space that satisfies (1) or (1): instead of the obvious definition ( if there is an entourage such that ), say that if there is a uniformly continuous function such that and , and similarly. And conversely, conditions (1) and (1) are likewise sufficient to prove complete regularity, modulo countable choice. So it does make sense to call them (or maybe their modulated versions) a sort of proximal complete regularity.
Of course if the uniform space we started from is not completely regular, then this proximity doesn’t really underlie it itself, but some kind of “completely regular reflection” of it. (In particular, it might not have the same underlying topology.) I’m not sure exactly what it should mean to say that a uniform space is “uniformly completely regular”, but maybe something like “for any entourage and point , there is a uniformly continuous function such that and and (not sure about whether to include that last condition). That’s at least sufficient that the above proximity has the same underlying topology.
I think a (completely regular) uniform space can also be interpreted as a syntopogenous space satisfying (1) or (1), if we define say to mean there is a uniformly continuous function such that and and also . If the uniform space is completely regular as above, then this syntopogeny is sufficient to determine the uniformity, and its simple coreflection is the above completely regular proximity. But this syntopogeny is no longer biperfect or even perfect, and I don’t see any easy way to characterize the syntopogenies arising from uniformities in this way.
Unrelatedly, it occurs to me that in addition to there is a fourth classically-equivalent way to express proximities (and, hence, I guess, also syntopogenies). Actually there are at least three more, but only one of them seems likely to be interesting. In proximity-space theory it’s sometimes written “” (where is the proximity space), defined classically to mean . Its Complete Regularity axiom is probably “if , there exist and such that and and ”; but I don’t immediately see how to formulate any weaker notion of Transitivity for it.
I added Complete Regularity to the list of axioms at proximity space, along with the above remarks, and a proof that assuming Complete Regularity and are inter-definable. I am not sure how to state Complete Regularity for , and seems unreasonable anyway constructively, so I left it blank.
Now I decided to rename Complete Regularity to Decomposability, and replace Regularity with a similar axiom (the “perfect” analogue of Decomposability) that doesn’t imply any symmetry, called Local Decomposability. The latter corresponds quite exactly to local decomposability for point-set structures. And Decomposability only implies complete regularity if we also have Symmetry, while classically Symmetry is the crucial ingredient ensuring complete regularity, so it seems not quite right to call Decomposability “complete regularity” (plus there is the countable choice issue).
I also added the missing nonemptiness condition to the definition of clusters in the Smirnov compactification, and some remarks on how a cluster is kind of like a prime filter.
1 to 43 of 43