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.
At uniform space, we have 6 axioms defining a uniform structure (or 4 to define a covering uniformity); I had added an axiom 0 [ETA: which I probably got from Douglas Bridges] which is classically trivial but useful in constructive mathematics. I now think that it's wrong to insist on this axiom; rather, those uniform spaces that satisfy it should be singled out as particularly nice. A good word for this, which may be used in similar contexts related to generalizations of metric spaces, is ‘located’; and since there are no Google hits for "located uniform space" (except for one which says ‘neatly located’ and so does not technically conflict), I am going to use that.
The result is that there are no more references to axiom (0) at uniform space; instead, we have a definition of a located uniform space.
I thought that were references to this axiom (0) on at least on other page pointing to uniform space, but the search function doesn't find any; if you do, though, then it would be nice to fix them.
I’m curious, what convinced you that this should be an extra adjective rather than part of the definition?
Douglas Bridges has worked quite a bit on the constructive theory of uniform spaces and related topological notions. Two initial remarks:
@Mike: With regards to purely mathematical arguments, mainly the example of arbitrary topological groups. But there is really a more philosophical reason, probably borne from reading more constructive literature, which is that one doesn't want to exclude things from the domain of discussion too early. If you're only interested in the located case, you can always say so; somebody else might want to be more general, and they're also entitled to use the term ‘uniform space’.
@Bas Spitters: The connection to located subspaces is as follows: located subspace of the metric space of rational numbers → located Dedekind cut = located real number → metric valued in located real numbers = located metric space → located uniform space. So yes, definitely the analogy with the three types of metric spaces.
You referred to Dedekind real numbers rather than located real numbers, and of course this is common, but I don't like that terminology. Not for this distinction, at least. Lower and upper real numbers are also described by Dedekind cuts, after all, and you can even make the cuts two-sided if you wish. So I want some term to indicate not only that we use two-sided Dedekind cuts but in particular ones which satisfy the rule
This rule implies that and are located subsets in , and Paul Taylor calls it ‘locatedness’ in his notes on Dedekind cuts. So I adopt that terminology; and then it becomes natural to generalize it as above.
We have to have some word for this, and I've already explained why I don't like ‘Dedekind’. The only other term that I can think of is ‘continuous’ (as in lower real = lower semicontinuous, upper real = upper semicontinuous). I think that that would be excessively weird; that a metric space is valued in located real numbers has little to say about the continuous maps on that space, for example. With ‘located’, however, even if one's mind is drawn to located subspaces, that is a closely related notion; in fact, a metric space (a priori valued in upper reals) is located (= valued only in located reals) iff every point of it is a located subset. (As you know, but I will recall for others, a subset of a metric space is located iff, for each point , the infimum , which again is a priori an upper real even when takes only located values, is a located real number.)
Re 4: Interesting. Arbitrary topological groups also have another defect: they are not necessarily localic groups (even classically). I wonder whether every localic group is a located uniform space, and what happens we also make the uniformity localic.
Re #5,#6, localic groups are always “open’ locales, Paul Taylor uses the word “overt”, which I like. I wrote a paper on the connections between locatedness and overtness. Paul has a number of papers on the topic, in fact, there are a few more. This should be related to the current discussion. Locatedness is not a topological property, but overtness is.
I’ll try to find time to say some more.
Regarding teminology, Paul usually has very sensible, but revolutionary ideas about this. It would be OK with me to refer to these as located reals (aka Dedekind reals). Fred Richman refers to generalized real numbers.
Toby, Bridges has a notion of almost located uniform space in this paper. He has also been working on apartness spaces, a constructive variant of nearness spaces (aka proximity spaces). I see you have been looking at them already. Do you know how they relate to your located uniform spaces?
Here is Wraith’s result on the overtness of localic groups.
I've been thinking lately about various analogies between uniform spaces, proximity spaces (particularly in the guise of neighbourhood spaces rather than apartness spaces), prometric spaces, etc. See generalized uniform structures - table. Also the reference (Clementino, Hofmann, Tholen) at prometric space; but that work is all classical.
I don't see what you mean by Wraith's result on localic groups. If you mean the result that every localic group is overt, that is trivial classically (since every locale is overt classically), and Wraith is working classically. Of course, even a classical mathematician might say something about locales in an arbitrary topos, but I don't see that either.
What I am calling ‘located’ is simply property S from the top of page 3 in that reference by Bridges et al. So Bridges is doing what I was doing until the other day, assuming that all uniform spaces are located. I probably got it from Bridges in the first place, although probably not that reference.
So it's clearly a very important property. Whether ‘located’ is really a good term for it is another question, of course.
While on the subject of Page 3 of Bridges et al, note the definition of an apartness relation on a uniform space:
(where runs over entourages and is my symbol for that I really like). Bridge's Axiom S (my Locatedness) allows one to conclude
This is a sort of approximate law of excluded middle that seems very powerful. (Of course, locatedness itself is an approximate law of excluded middle, but doubly approximate.) It also seems to me that we need locatedness to prove comparison for too.
Thanks for #11,#12. It may be useful to add these remarks. Re #9, yes, this is nice. A constructive comparison would be nice too, but may require a lot of work.
Another constructive definition is in Bishop/Bridges p124. These are located in your sense, but it seems easy to change this definition with pseudometrics in the lower reals.
Re #10, I don’t have the time to check carefully now, but I seem to recall that Lemma 2 can be used for a definition of positivity and that the proofs are basically constructive.
If I recall correctly what's in Bishop & Bridges, they're really considering gauge spaces (with, I think, countable bases). These are a step along the way to prometric spaces, although there I had to use (extended) upper reals to make the definition most beautiful.
#14: OK, I didn't check the details either, but that makes sense. An open subspace (of a localic group) is positive iff the identity belongs to , and this is a bona fide point regardless of whether had any points to begin with.
There happens to be some discussion on this at the categories list currently. Simon Henry also suggests that openness is important.
Yes, I've been reading that with interest.
I added a remark to uniform space about the uniformity of uniform convergence, and that constructively to prove it is located (assuming the codomain is) we seem to need the domain to be compact in some sense (e.g. covert). One could interpret this as an argument for considering locatedness as an additional property rather than part of the constructive definition of “uniform space”.
I do think we ought to find another word than “located” for this property, though. I just re-encountered the notion and spent a while being confused about its relationship to located subspaces before I rediscovered this old conversation. Here it’s not really the space that’s “located”, but rather its points or subsets, i.e. rather than itself being located, it allows us to locate things inside of it. I’d like a word that’s related to “located” in the same sort of way that “overt” is related to “open”, maybe “locatable”?
@Mike #20: Bas and I were discussing that in comments #3, #5, #7 (last paragraph).
I recall some old literature saying that a topological space is of second category if it is a non-meagre (aka of second category) subspace of itself (more careful authors would write ‘second category in itself’). Of course, every uniform space is a located subspace of itself; here we're looking in the other direction and asking if the points are located.
I'm not entirely sure, however, that a uniform space is located iff its points are located subspaces, because I don't remember what the definition of located subspace of a uniform space is supposed to be (and whether such definitions as appear in the literature agree with each other —or indeed are any of them appropriate— without assuming that the uniform space is located in the first place).
Yes, I did read #3, 5, and 7, but the discussion seemed to have stalled without finding a better word, so I was saying that I’d like to reopen it.
Another question: is there an appropriate notion of “located” for quasi-uniform spaces?
I speculate a bit about generalizations of locatedness in Ch10 of my Locatedness and overt sublocales. It seems that one needs a strict < on opens to define a notion of locatedness. However, I did not consider uniform, or quasi-norm spaces explicitly.
Thanks.
Yet another: is it constructively true that (located) uniform spaces are completely regular? Given a point and an open neighborhood , I think I can make the classical construction yield functions or with and , where and are the lower real numbers and upper real numbers. But I can’t see how to make these into a Dedekind or even a MacNeille section; locatedness of the uniform space doesn’t seem to be enough.
As far as I can tell, you need countable choice to get any good results about complete regularity. Even in locale theory, Johnstone (in Stone Spaces) had to use countable choice to prove that a compact regular locale is completely regular. And while I can't recall noticing that he used excluded middle, he didn't keep track of that in that book, so he might have and I missed it.
My suspicion is that real meaning of ‘completely regular’ should be ‹embeddable in a compact regular space›, turning the definition in terms of functions to the real line into an alternative characterization that is provable in classical mathematics but may fail otherwise. On the other hand, I haven't proved constructively that every uniform space (or even every located one) can be so embedded. Considering how badly compactness behaves in point-set topology without the fan theorem, that may not be true either.
My current suspicion is that the Urysohn-type argument for producing real-valued functions can be made to work if the located uniform space is also “locally covert” in the sense that it has a base of entourages such that each is covert.
That would be an interesting result!
One thing we’d almost certainly need, in the absence of countable/dependent choice, is that the axioms of an entourage uniformity are given by functions (e.g. a function assigning to each entourage an entourage such that ) rather than mere existence. I’m not sure what to call a uniform space with this property (or, really, structure): functional? pure? modulized? Is there a word used for analogous dichotomies elsewhere?
By ‘modulized’, do you mean to evoke the notion of a modulus of continuity/convergence/etc? At Cauchy real number, you can see that sequences equipped with a modulus of Cauchy convergence are called ‘modulated’ Cauchy sequences, and this is a fairly standard term. I'm not sure that this is the right word to use here, but I'll use it for now.
The uniformity on a metric space is modulated. To begin with, given , let mean . Then given , the required entourage in the cited axiom is .
What really makes this work is the existence of what I am going to call the base of and denote , given by . (Note that really depends on only through , and with equality in many cases, hence the notation.) The same function may be used to prove that the uniform space is located. (That these two axioms can be combined is mentioned in the reference to constructive mathematics in the section on motivation at uniform space. And of course, all of the other axioms come with a canonical modulus.)
It would be nice if the uniformity on a gauge space would also always be modulated; gauge spaces are, after all, how Bishop wanted to handle uniform spaces (although he restricted to those with a countable subbase). I don't see how to prove that, since a single entourage might be an entourage for a multiplicity of reasons; there is no way to identity which gauging distance to use. Even in the case of a metric space, there is the question of which to use, and I effectively answered to use the maximum; and since constructively this might not exist, I referred to the condition of being than this putative maximum instead. But I see no way, even with excluded middle, to choose a maximum gauging distance, nor to refer to one obliquely. (Gauges are closed under finitary maxima but not under even countably infinitary ones.) That is, I can define but not .
However, I think that instead we should speak of a modulated base of a uniformity, and the base should be parametrized. Given an arbitrary entourage, there exists some basic entourage within it, but we can't expect a function to pick out this base. However, given a basic entourage, we do expect a function to pick out one of its lax square roots, and in fact to pick out a basic one. That said, we don't expect this function to depend only on what relation the entourage is; instead, it acts on parameters for a parametrization of the basic entourages. We should also require this to be a base in a strict way: closed under finitary intersections rather than merely lax-closed. (I just made up the terms ‘lax square root’ and ‘lax-closed’; I hope that you like them.) I don't even know a name for this property, altough I once asked on MathOverflow about it. In principle, this could be replaced with another function choosing from the basic lax intersections, but it would be easier just to have the intersection in there. Similarly, the base should be closed under taking inverses, to avoid needing a function to choose from a basic entourage's basic lax inverses.
So a modulated base (terminology pending) for a uniformity on a set is an index , the structure of an involutory monoid on (written multiplicatively with involution ), a unary operation on , and a ternary relation on , , and , written , such that:
A modulated uniformity is symmetric if the involution is trivial; it is located if
By Excluded Middle, every modulated base is located. (A base can be modulated without being located, because modulation avoids Choice, while locatedness avoids Excluded Middle, and it's just a coincidence that Excluded Middle is a special case of Choice.)
Given a modulated base, an entourage is a binary relation such that, for some index , if , then ; the collection of entourages is a uniformity. Conversely, using Choice, we can turn any base for a uniformity into a modulated base, and we can make it located (in the sense of a modulated base) if the uniformity was located (in the weaker sense of a uniformity) while we do so. (Of course, using Choice, any uniformity is located, but it's a different choice; for example, using only Countable Choice, we can turn any countable base for a uniformity into a modulated base, and we can make it located if the uniformity is located, but Countable Choice alone can't force the uniformity to be located.) To do this, we close the base up under finitary intersections and opposites, then use this collection of basic entourages as the index set, with intersection as the monoid operation and opposites as the involutes. Using Choice, we pick a lax square root for each basic entourage; the approximate transitivity axiom of a uniformity guarantees that each basic entourage has a lax square root among the entourages, which in turn must contain a basic entourage that is therefore also a lax square root. To make this located, we use a lax square root that will satisfy the locatedness axiom, which always exists (see again the discussion of constructive aspects in the Motivation section of the article). Of course, means that .
Given any modulated base, we can find a symmetric modulated base that is equivalent, in the sense of generating the same uniformity. Furthermore, if the modulated base was located, then this symmetric base will also be located. I would like to say that an index of the new modulated base will be an unordered pair of old indexes such that , but I have trouble defining the new operations without Choice, so I'm settling for doubling all of the non-self-involutory indexes. So we keep the same index set with the same structure but redefine (in the symmetrized meaning) to mean that and (in the original meaning). Note that we have no guarantee that , but that doesn't actually matter. (If we need that, then we could impose it from the beginning, but I don't see a need yet.)
It's also kind of arbitrary to require to be an involutory monoid. I said that mostly because it was the easiest to say; but if is nonassociative or if the involution is not compatible with the multiplication, then that's not really important. On the other hand, we could require multiplication to be idempotent, much as we could require . Without choice, I don't see how to replace a modulated base satisfying a weaker definition with one that satisfies a stronger definition, which is somewhat disconcerting.
Anyway, every gauge space has a modulated base; an index consists of a gauging distance together with a positive real number. Alternatively, we could use a base for a gauge instead; we could even start with a subbase, but we'd just have to close it up under finitary maxima to get a base. Similarly, we could use only basic positive real numbers, such as the reciprocals of positive integers; this guarantees that a gauge space with a countable base (or subbase) gives rise to a uniformity with a countable modulated base.
I need to go, so I'll post this now, before checking whether or not this is actually enough to prove the Urysohn Lemma!
Thanks for writing all that up; I had come to essentially the same conclusions myself, except that I figured the entourages themselves should also be parametrized (not just the base). (-:
I didn’t say “modulated” because my main association with that is “modulated bicategories” which is a different meaning, but I suppose there’s unlikely to be any ambguity, and “modulated” sounds better than “modulized”.
This business of putting an algebraic structure on the indexes of the basic whatevers is very reminiscent of formal topology, which starts by putting an algebraic structure on the basic opens of a locale.
Yes. I don’t know whether anyone has seriously tried doing “formal uniformity” in such a way. To my knowledge the limited attempts at uniform locales have been done by starting with a locale and putting a (covering) uniformity structure on it, and didn’t work constructively.
My inclination, though, as I said, would be to put the structure on the entourages themselves rather than on a base. That is, I would define a modulated uniformity to be an index set , a function , and operations:
Now suppose we have a point and an open containing it, which in turn by definition of the uniform topology contains some . Using your notation , and your assumption that these also satisfy the locatedness axiom, define to get a sequence of entourages . Let and , and for each dyadic rational , write and . Then for . For any , define
This should be a Dedekind cut except for locatedness. Locatedness would follow if we had for any , which would follow from , and we know . Put differently, for each we know either or , and we want to know that for any either or . By definition of we can write as , and similarly for . So if each is covert, we can apply the Theorem mentioned under “covert sets” at covert space.
I figured the entourages themselves should also be parametrized (not just the base). (-:
Fortunately, this is not any more restrictive. Given a base indexed by , you can index the entourages by ; the entourage indexed by is , define , and use . So every entourage comes equipped with a basic entourage inside of it.
This construction is not predicative, of course; indeed, if you want to be predicative and have any decent examples, then you'll have to satisfy for indexing a base, because you can't reasonably expect to find an index set large enough to parametrize the set of all entourages. (I suppose that this is why the formal topologists index a base instead of the entire frame of opens; they're trying to be predicative.)
I was attempting a proof along the same lines as what you just wrote. As far as you went, it works the same way for a modulated base for a uniformity as for an entire modulated uniformity. (You never use axiom 6.)
For the record, if you keep axiom 2 separate from the locatedness axiom, then that's equivalent to my single combined axiom, even when being functional, since you can just compose the functions.
to mean for some (or )
If you use only this, then you define an upper-real-valued function with the desired properties, and you don't need locatedness (of the uniformity). This is what I expected should be possible.
the Theorem mentioned under “covert sets” at covert space
Yeah, I often want to apply that theorem, but I don't think that there are many covert sets.
Given a base indexed by , you can index the entourages by
Yes, of course. But it’s harder for me to think predicatively, and I’m not highly motivated to do so since I don’t know of hardly any interesting predicative toposes that aren’t elementary toposes.
If you use only this, then you define an upper-real-valued function with the desired properties
Yes, that’s where I started back in #26.
I don’t think that there are many covert sets.
I agree that there are probably not many sets that can be proven to be covert in pure constructive mathematics. However, the Dubuc-Penon paper cited at covert space shows that in topological, smooth, and algebraic models, the covert sets tend to coincide with the compact spaces. So, for instance, and other “locally compact spaces” (with “space” meaning “set”, as in synthetic topology) are “locally covert” in such models.
I have a proposal for another name for the “locatedness” property of a uniform space: uniform regularity. This is based on two observations:
The classical proof that every uniform space is regular (which is much easier than the proof that it is completely regular) seems — to me, right now — to require this condition, at least if “regular” is meant in the localic/open-set-theoretic sense (Definition 2.2 at regular space). If is a uniform neighborhood of , let be an entourage such that , and an entourage such that . Then is a neighborhood of , and the interior of is an open set , such that and .
If a topological group is regular, then its induced uniformities satisfy this condition. For if is any neighborhood of the identity in a topological group , by regularity we have a neighborhood of and an open set with and , and in particular , whence the entourages defined by and satisfy the desired condition.
I don’t know whether it is possible to prove constructively that a non-located uniform space is regular, or any countermodels containing uniform spaces (such as topological groups) that are not regular. So I can’t fully justify this proposed terminology, but it feels natural to me and I like it better than “located”.
OK, so you've proved that a topological group is regular iff its uniformity is uniformly regular, and you've proved that uniform space is regular if its uniformity is uniformly regular, but we remain ignorant about the existence of regular uniform spaces (necessarily with no compatible group structure) that are not uniformly regular, as well as about the existence of uniform spaces that are not regular.
Let me add that it's obvious that a completely regular uniform space is uniformly regular, so uniform regularity lies between regularity and complete regularity, even if we're not sure yet how strict that inclusion can be. To my mind, this pretty much justifies the terminology. If we eventually find that every completely regular uniform space is uniformly regular or that every uniformly regular uniform space is regular, then we can remove the new phrase from our vocabulary, but until then it remains viable.
Besides that, the condition has always clearly had the flavour of regularity. I like it!
I’m glad you like it! What would you think about splitting off a separate page uniformly regular space?
By the way, regarding the scarcity of covert sets, I have some vague hope that the argument could be made “more pointless” and thereby make use of topological compactness of as a locale rather than its covertness as a set. But I haven’t managed to make that work yet, and at some point it starts bumping up against the question of what a uniform locale is, constructively.
Also, calling it “uniformly regular” makes it clear why it should not be regarded as part of the definiton of a uniform space: it’s actually a separation condition!
Here’s an attempt at a constructive proof that a compact regular space is (uniformly regularly) uniformizable.
Let be compact regular. Since compactness and regularity are properties of the open-set lattice, is still compact regular when regarded as a locale, and hence also Hausdorff as a locale. Moreover, it is locally compact, and hence the locale and spatial products coincide. Furthermore, is also compact regular.
As usual, define the entourages to be all the neighborhoods of the diagonal in ; this obviously satisfies all the axioms of a uniformity except possibly the square-root (and uniform regularity).
Let be a neighborhood of the diagonal in . Since is regular, and using the definition of the product topology, for each there is a square neighborhood and an open set such that and . The open sets cover the compact space , hence finitely many of them suffice. Let , and . Then is a neighborhood of the diagonal, and an open set such that and . In particular, , so this uniformity (if it exists) is uniformly regular.
Now, is the union of rectangular open neighborhoods . Note that since is disjoint from the diagonal, any satisfies . Moreover, since is regular, each and is the union of open sets that are well-inside it; thus is the union of rectangular open neighborhoods such that there are opens with and and . Since and is compact, we can cover it by together with finitely many such rectangles , say .
For each of these rectangles , let be an open set such that and , and let . Then is a neighborhood of the diagonal; let .
We claim . Let , so that there is a with and . Now we have either (which is what we want) or for some , so it suffices to rule out the latter possibility. Since , we have , hence or or . But , which is disjoint from and , so it must be that and hence . Similarly, we conclude that so that . But , a contradiction.
It remains to show that the uniform topology on is the original one. Clearly if is an entourage then each is a neighborhood of . Conversely, if is a neighborhood of , then by regularity we have a neighborhood of and an open with and . Then is a neighborhood of the diagonal, i.e. an entourage, such that .
We can also conclude, as classically, that this is the unique uniformity compatible with a compact regular topology. Suppose is any compact regular uniform space, and any neighborhood of the diagonal; we want to show is an entourage. For any , there is an entourage such that . Let be an entourage such that . Since is compact, it is covered by finitely many of the neighborhoods , say . Let ; we claim . For let ; then we have for some , whence also , and thus .
In particular, a compact regular uniform space is automatically uniformly regular as well.
I just noticed this from #24:
is there an appropriate notion of “located” for quasi-uniform spaces?
Isn't the definition as it stands at uniform space reasonable? Of course, the analogue of ‹completely regular› for quasiuniform spaces is ‹anything whatsoever›, and here the theorems seem to go the other way: every uniformly regular quasiuniform space induces a topology that satisfies this trivial conclusion, but not every topology can be quasiuniformized by a uniformly regular quasiuniformity, as far as I can see. But it certainly can be quasiuniformized, period. (Every open set defines an entourage such that iff , and generate from this subbase.) This quasiuniformity can even be modulated. (On the subbase, and even on the generated base, is the identity function.)
ETA: Of course, any quasigaugeable space is uniformly regular. (Despite not being regular, so maybe that's not such a great term in the nonsymmetric case.)
Moreover, it is locally compact, and hence the locale and spatial products coincide.
Is this a constructive theorem? But I don't think that it matters, since you seem to only use it to say
is also compact regular
and this can be proved directly.
I wrote earlier:
My suspicion is that real meaning of ‘completely regular’ should be ‹embeddable in a compact regular space›
A subspace of a uniformly regular uniform space is uniformly regular, so any uniform space embeddable in a compact regular space is uniformly regular. However, it doesn't seem likely that every uniformly regular uniform space will be constructively embeddable in a compact regular space. Without the real-valued-functional kind of complete regularity, we can't make it into a gauge space and so can't embed it in a product of unit intervals; and so what if we could, since the unit interval need not be compact, and so what if it were, since an infinitary product of compact spaces need not be compact either. Perhaps there is some completely different approach, but I don’t know it. (And keeping in mind that a complete, totally bounded uniform space, even a CTB metric space, need not be compact either, even though one can construct a compact locale from it.)
I wrote:
any quasigaugeable space is uniformly regular. (Despite not being regular, so maybe that’s not such a great term in the nonsymmetric case.)
The obvious term then would be ‘uniformly quasiregular’ (or ‘quasiuniformly’, but that doesn't fix the noted problem). Which is maybe a bit silly, since what does ‘quasiregular’ mean anyway?
But actually this works out great! After all, uniform regularity, while related to regularity, doesn't directly uniformize topological regularity. What it uniformizes is the following classically trivial condition that I hereby dub quasiregularity: is quasiregular if, for each point and neighbourhood of , for some neighbourhood of , . Of course, every regular space is quasiregular. Also, the same condition on entourages makes a quasiuniform space uniformly quasiregular. Just as uniform spaces are classically all regular, so uniformly quasiregular uniform spaces are all regular, and this allows us to use ‘uniformly regular’ as a synonym for ‘uniformly quasiregular’ when discussing symmetric spaces.
Edit: fixed definition of quasiregularity.
Haven’t read 44-46 yet, but here’s another class of uniform spaces that are regular iff uniformly regular: discrete ones (the diagonal is a uniformity). In this case both conditions are equivalent to the underlying set having decidable equality.
In particular, “all uniform spaces are regular”, “all discrete uniform spaces are regular”, “all uniform spaces are uniformly regular”, etc. are all equivalent to LEM.
For reasons that I don’t have time to explain right now, I was hoping for a quasi- analogue of uniform regularity that could be satisfied by any topological space, and in particular by the Sierpinski space.
What makes you suspect that the real definition of “completely regular” should be “embeddable in a compact regular space”?
Would it work to embed in a compact regular locale (since the localic unit interval is compact, and locales satisfy Tychonoff constructively)?
Coincidence of localic and spatial products of locally compact spaces is C4.1.8 in the Elephant, which is specifically remarked to be constructive.
In the paper of Bridges et. al. cited in #8, a subset of a uniform space is said to be almost located if for each entourage there exists an entourage such that . It seems that a uniform space is quasiregular iff all singletons are almost located. Also, I think another way to fix the Urysohn-type argument is if we had “ almost located almost located, for any entourage ”; but I suppose that is too much to hope for? I don’t have much intuition yet for (almost) located subsets.
I was hoping for a quasi- analogue of uniform regularity that could be satisfied by any topological space, and in particular by the Sierpinski space.
Of course, it's true classically that every quasiuniform space is uniformly quasiregular (and that every topological space is quasiregular), as I've defined these, but I presume that this is not what you wanted. Since a uniform space might not be uniformly regular constructively, I doubt that a quasiuniform space must be quasi-(uniformly regular) constructively, for any notion of quasi-(uniformly regular) that would reasonably be considered an analogue. (In particular, a discrete space is quasiregular iff equality is decidable, too.)
What makes you suspect that the real definition of “completely regular” should be “embeddable in a compact regular space”? Would it work to embed in a compact regular locale (since the localic unit interval is compact, and locales satisfy Tychonoff constructively)?
So even speaking of point-set topological spaces, we would call one completely regular iff its soberification, when viewed as a locale, is a sublocale of some complete regular locale? That seems kind of cheating, even restricting to spaces that are already known to be sober. But since there aren't enough compact point-set spaces anyway, it might still be right thing to do.
Coincidence of localic and spatial products of locally compact spaces is C4.1.8 in the Elephant, which is specifically remarked to be constructive.
OK, good.
It seems that a uniform space is quasiregular iff all singletons are almost located.
Making the argument for calling such spaces simply ‘located’ even worse.
The motivation for that terminology, hinted at way back in comment #1, is that a metric valued in (located) real numbers has this property, while a metric valued in more general (upper, lower, etc) numbers might not. That was really too tenuous a connection all along; nothing in the definition of uniform regularity refers to any kind of real numbers. I still might say things like ‘located gauge space’ etc, but ‘located uniform space’ is unjustifiable.
On the other hand, it does look similar to the definitions at located subspace, even though I don't think that I was thinking about those in 2014!
I doubt that a quasiuniform space must be quasi-(uniformly regular) constructively, for any notion of quasi-(uniformly regular) that would reasonably be considered an analogue
Certainly, but my hope was a little different, namely that every topological space would admit some quasiuniformity that was quasi-(uniformly regular). It does seem unlikely, though, now that we see uniform regularity as a separation condition.
So even speaking of point-set topological spaces, we would call one completely regular iff its soberification, when viewed as a locale, is a sublocale of some [compact] regular locale? That seems kind of cheating, even restricting to spaces that are already known to be sober.
Well, there are plenty of topological properties of spaces that are really properties of their open-set lattice and hence of their soberification viewed as a locale, such as compactness and regularity, even if (especially classically) those conditions are equivalent to others that use points.
I guess to know the right constructive definition of “completely regular” I would like to know more about what classical theorems about completely regular spaces we want to preserve. The main theorem I know of right now is the equivalence of three conditions: uniformizability, separation of points and closed subsets by real-valued functions, and embeddability in compact Hausdorff spaces. Given that that theorem seems unlikely to remain true constructively, it doesn’t give me much intuition for which of the three no-longer-equivalent conditions should be called “complete regularity”. What else are completely regular spaces for?
At Tychonoff space it is claimed that the real-valued-functions definition is “suitable in any case if lands in the locale of real numbers and by “complement” we mean the set of real numbers apart from ”. What does “suitable” mean? (Also, as long as is a space rather than a locale, any function from it to the locale of real numbers will factor through the space of real numbers, since the spatial part of a locale is a coreflection.)
I presume that the localic definition referred to is the one in Stone spaces using a “scale” (a mesh of interpolating opens indexed by rational numbers)? I can try to add that to the page.
If a located subspace is one that doesn’t exist only for pathological logical reasons, as you suggested in its idea section, then it doesn’t seem too farfetched to hope that at least for a well-behaved uniform space, there would be at least a base of entourages such that if is located then so is . Are there any uniform spaces that can be shown to satisfy that condition? Even ?
I created uniformly regular space.
Good. I edited one place where you improperly let the word ‘located’ stand.
I just noticed that the notion of quasi-regular space appears in the Bridges-Schuster-Vita paper on apartness, under the name “locally decomposable” (Proposition 2.2).
1 to 57 of 57