Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeAug 9th 2014
    • (edited Aug 22nd 2014)

    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.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2014

    I’m curious, what convinced you that this should be an extra adjective rather than part of the definition?

    • CommentRowNumber3.
    • CommentAuthorspitters
    • CommentTimeAug 9th 2014
    • (edited Aug 9th 2014)

    Douglas Bridges has worked quite a bit on the constructive theory of uniform spaces and related topological notions. Two initial remarks:

    • Locatedness is usually considered as a property of a subspace, not of a space per se.
    • The ananology you have in mind is probably with three kinds of metric spaces, i.e. ones where the metric has values in the Dedekind reals, the lower reals or the upper reals. Now take any such metric space and consider the derived uniform spaces. Which ones would be “located” in your sense?
    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeAug 11th 2014

    @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’.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeAug 11th 2014

    @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 (L,U)(L,U) but in particular ones which satisfy the rule

    a<baLbU. a \lt b \;\Rightarrow\; a \in L \;\vee\; b \in U .

    This rule implies that LL and UU are located subsets in \mathbb{Q}, 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 SS of a metric space is located iff, for each point xx, the infimum inf ySd(x,y)\inf_{y \in S} d(x,y), which again is a priori an upper real even when dd takes only located values, is a located real number.)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2014

    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.

    • CommentRowNumber7.
    • CommentAuthorspitters
    • CommentTimeAug 12th 2014
    • (edited Aug 12th 2014)

    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.

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeAug 14th 2014

    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.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeAug 14th 2014

    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.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2014

    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.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2014

    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.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2014
    • (edited Aug 15th 2014)

    While on the subject of Page 3 of Bridges et al, note the definition of an apartness relation on a uniform space:

    xyU,¬x Uy x \ne y \;\Leftrightarrow\; \exists U,\; \neg\; x \approx_U y

    (where UU runs over entourages and U\approx_U is my symbol for (x,y)U(x,y) \in U that I really like). Bridge's Axiom S (my Locatedness) allows one to conclude

    U,x,y,x Uyxy. \forall U,\; \forall x, y,\; x \approx_U y \;\vee\; x \ne y .

    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 \ne too.

    • CommentRowNumber13.
    • CommentAuthorspitters
    • CommentTimeAug 15th 2014

    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.

    • CommentRowNumber14.
    • CommentAuthorspitters
    • CommentTimeAug 15th 2014

    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.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2014

    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.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeAug 16th 2014
    • (edited Aug 16th 2014)

    #14: OK, I didn't check the details either, but that makes sense. An open subspace SS (of a localic group) is positive iff the identity belongs to S 1SS^{-1} S, and this is a bona fide point regardless of whether SS had any points to begin with.

    • CommentRowNumber17.
    • CommentAuthorspitters
    • CommentTimeAug 22nd 2014

    There happens to be some discussion on this at the categories list currently. Simon Henry also suggests that openness is important.

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeAug 22nd 2014

    Yes, I've been reading that with interest.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2016

    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”.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2016

    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”?

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeNov 21st 2016

    @Mike #20: Bas and I were discussing that in comments #3, #5, #7 (last paragraph).

    • CommentRowNumber22.
    • CommentAuthorTobyBartels
    • CommentTimeNov 21st 2016

    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).

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2016

    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.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2016

    Another question: is there an appropriate notion of “located” for quasi-uniform spaces?

    • CommentRowNumber25.
    • CommentAuthorspitters
    • CommentTimeNov 22nd 2016

    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.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2016

    Thanks.

    Yet another: is it constructively true that (located) uniform spaces are completely regular? Given a point xXx\in X and an open neighborhood UxU\ni x, I think I can make the classical construction yield functions f:XR lf:X\to R_l or f:XR uf:X\to R_u with f(x)=1f(x)=1 and f(y)>0yUf(y)\gt 0 \to y\in U, where R lR_l and R uR_u 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.

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeDec 2nd 2016

    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.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeDec 2nd 2016

    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 UU such that each U[x]U[x] is covert.

    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeDec 4th 2016

    That would be an interesting result!

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2016

    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 UU an entourage VV such that VVUV\circ V \subseteq U) 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?

    • CommentRowNumber31.
    • CommentAuthorTobyBartels
    • CommentTimeDec 5th 2016

    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 ε>0\varepsilon \gt 0, let U εU_\varepsilon mean {x,y|d(x,y)ε}\{x, y \;|\; d(x,y) \leq \varepsilon\}. Then given UU, the required entourage VV in the cited axiom is U{x,y|ε>0,(x,y)U ε,U 2εU}\sqrt{\lfloor{U}\rfloor} \coloneqq \{x, y \;|\; \exists \varepsilon \gt 0,\; (x, y) \in U_\varepsilon,\; U_{2\varepsilon} \subseteq U\}.

    What really makes this work is the existence of what I am going to call the base of UU and denote U\lfloor{U}\rfloor, given by U{x,y|ε>0,(x,y)U εU}\lfloor{U}\rfloor \coloneqq \{x, y \;|\; \exists \varepsilon \gt 0,\; (x, y) \in U_\varepsilon \subseteq U\}. (Note that U\sqrt{\lfloor{U}\rfloor} really depends on UU only through U\lfloor{U}\rfloor, and UUU\sqrt{\lfloor{U}\rfloor} \circ \sqrt{\lfloor{U}\rfloor} \subseteq {\lfloor{U}\rfloor} 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 ε\varepsilon to use, and I effectively answered to use the maximum; and since constructively this might not exist, I referred to the condition of being \leq 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 \sqrt{} but not \lfloor{}\rfloor.

    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 \lfloor{}\rfloor 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.

    • CommentRowNumber32.
    • CommentAuthorTobyBartels
    • CommentTimeDec 5th 2016

    So a modulated base (terminology pending) for a uniformity on a set XX is an index II, the structure of an involutory monoid on II (written multiplicatively with involution **), a unary operation on II, and a ternary relation on XX, II, and XX, written x iyx \approx_i y, such that:

    1. x ixx \approx_i x always;
    2. if x iy izx \approx_{\sqrt{i}} y \approx_{\sqrt{i}} z, then x izx \approx_i z;
    3. x i *yx \approx_{i^*} y iff y ixy \approx_i x;
    4. x ijyx \approx_{i j} y iff x iyx \approx_i y and x jyx \approx_j y;
    5. x 1yx \approx_{1} y always.

    A modulated uniformity is symmetric if the involution is trivial; it is located if

    • x iyx \approx_i y or not x iyx \approx_{\sqrt{i}} y always.

    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 UU such that, for some index ii, if x iyx \approx_i y, then (x,y)U(x,y) \in U; 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, x Uyx \approx_U y means that (x,y)U(x,y) \in U.

    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 {i,j}\{i,j\} of old indexes such that j=i *j = i^*, 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 x iyx \approx_i y (in the symmetrized meaning) to mean that x iyx \approx_i y and y ixy \approx_i x (in the original meaning). Note that we have no guarantee that i *=(i) *\sqrt{i^*} = (\sqrt{i})^*, 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 II to be an involutory monoid. I said that mostly because it was the easiest to say; but if II 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 i *=(i) *\sqrt{i^*} = (\sqrt{i})^*. 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!

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2016

    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”.

    • CommentRowNumber34.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2016

    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.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2016

    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 II, a function U:IP(X×X)U:I \to P(X\times X), and operations:

    • iΔU i\forall_{i} \Delta \subseteq U_i
    • i j(U jU jU i)\prod_i \sum_j (U_j \circ U_j \subseteq U_i)
    • i j(U j) opU i\prod_i \sum_j (U_j)^{op} \subseteq U_i
    • i(U i=X×X)\sum_i (U_{i} = X\times X)
    • i,j k(U k=U jU j)\prod_{i,j} \sum_k (U_k = U_j\cap U_j)
    • i VX×X(U iV) j(V=U j)\prod_i \prod_{V\subseteq X\times X} (U_i \subseteq V) \to \sum_j (V = U_j)
    • i j(¬U jU i=X×X)\prod_i \sum_j (\neg U_j \cup U_i = X\times X)

    Now suppose we have a point xx and an open containing it, which in turn by definition of the uniform topology contains some U i 0[x]U_{i_0}[x]. Using your notation \sqrt{}, and your assumption that these also satisfy the locatedness axiom, define i n+1=i ni_{n+1} = \sqrt{i_n} to get a sequence of entourages U n=U i nU_n = U_{i_n}. Let V n,1=U nV_{n,1} = U_n and V n,0=ΔV_{n,0} = \Delta, and for each dyadic rational q[0,1]q\in [0,1], write q=q 0.q 1q 2q nq = q_0.q_1 q_2 \dots q_n and V q=V n,q nV 1,q 1V_q = V_{n,q_n} \circ \cdots \circ V_{1,q_1}. Then U qU rU_q \subseteq U_r for q<rq\lt r. For any yXy\in X, define

    • (q<f(y))(q\lt f(y)) to mean yU ry\notin U_r for some r>qr\gt q (or q<0q\lt 0)
    • (f(y)<q)(f(y)\lt q) to mean yU ry\in U_r for some r<qr\lt q (or q>1q\gt 1)

    This should be a Dedekind cut except for locatedness. Locatedness would follow if we had ¬V q[x](U nV q)[x]=X\neg V_q[x] \cup (U_{n} \circ V_q)[x] = X for any q,nq,n, which would follow from ¬(U n+1V q)[x](U nV q)[x]=X\neg (U_{n+1}\circ V_q)[x] \cup (U_{n} \circ V_q)[x] = X, and we know ¬U n+1U n=X×X\neg U_{n+1}\cup U_n = X\times X. Put differently, for each y,zy,z we know either ¬((y,z)U n+1)\neg((y,z)\in U_{n+1}) or (y,z)U n(y,z)\in U_n, and we want to know that for any yy either zV q[x],¬((y,z)U n+1)\forall z\in V_q[x], \neg((y,z)\in U_{n+1}) or zV q[x],((y,z)U n)\exists z\in V_q[x], ((y,z)\in U_{n}). By definition of V q[x]V_q[x] we can write zV q[x]\exists z\in V_q[x] as z 1V 1,q 1[x],z 2V 2,q 2[z 1],z nV n,q n[z n1]\exists z_1 \in V_{1,q_1}[x], \exists z_2 \in V_{2,q_2}[z_1], \dots \exists z_n \in V_{n,q_n}[z_{n-1}], and similarly for \forall. So if each U n[z]U_n[z] is covert, we can apply the Theorem mentioned under “covert sets” at covert space.

    • CommentRowNumber36.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2016

    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 II, you can index the entourages by I×𝒫(X×X)I \times \mathcal{P}(X \times X); the entourage indexed by (i,A)(i, A) is U iAU_i \cup A, define i,A=(i,U i)\lfloor{i, A}\rfloor = (i, U_i), and use i,A\sqrt{\lfloor{i, A}\rfloor}. 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.

    (f(y)<q)(f(y)\lt q) to mean yU ry\in U_r for some r<qr\lt q (or q>1q\gt 1)

    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.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2016
    • (edited Dec 6th 2016)

    Given a base indexed by II, 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, \mathbb{R} and other “locally compact spaces” (with “space” meaning “set”, as in synthetic topology) are “locally covert” in such models.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2016

    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 U[a]U[a] is a uniform neighborhood of aa, let VV be an entourage such that ¬VU=X×X\neg V\cup U = X\times X, and WW an entourage such that WWVW\circ W \subseteq V. Then W[a]W[a] is a neighborhood of aa, and the interior of W[¬V[a]]W[\neg V[a]] is an open set GG, such that GW[a]=G\cap W[a] = \emptyset and GU[a]=XG\cup U[a] = X.

    • If a topological group is regular, then its induced uniformities satisfy this condition. For if UU is any neighborhood of the identity ee in a topological group XX, by regularity we have a neighborhood VV of ee and an open set GG with VG=V\cap G = \emptyset and GU=XG\cup U = X, and in particular ¬VU=X\neg V\cup U = X, whence the entourages defined by UU and VV 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”.

    • CommentRowNumber39.
    • CommentAuthorTobyBartels
    • CommentTimeDec 6th 2016

    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!

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2016

    I’m glad you like it! What would you think about splitting off a separate page uniformly regular space?

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2016

    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 U[x]U[x] 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.

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2016

    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!

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2016

    Here’s an attempt at a constructive proof that a compact regular space is (uniformly regularly) uniformizable.

    Let XX be compact regular. Since compactness and regularity are properties of the open-set lattice, XX 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 X×XX\times X coincide. Furthermore, X×XX\times X is also compact regular.

    As usual, define the entourages to be all the neighborhoods of the diagonal in X×XX\times X; this obviously satisfies all the axioms of a uniformity except possibly the square-root (and uniform regularity).

    Let UU be a neighborhood of the diagonal in X×XX\times X. Since X×XX\times X is regular, and using the definition of the product topology, for each xXx\in X there is a square neighborhood V x×V xV_x\times V_x and an open set G xX×XG_x\subseteq X\times X such that (V x×V x)G x=(V_x\times V_x)\cap G_x = \emptyset and G xU=X×XG_x \cup U = X\times X. The open sets V xV_x cover the compact space XX, hence finitely many of them suffice. Let V=(V x 1×V x 1)(V x n×V x n)V = (V_{x_1}\times V_{x_1}) \cup \cdots \cup (V_{x_n}\times V_{x_n}), and G=G x 1G x nG = G_{x_1} \cap \cdots \cap G_{x_n}. Then VV is a neighborhood of the diagonal, and GG an open set such that GU=X×XG\cup U = X\times X and VG=V \cap G = \emptyset. In particular, ¬VUGG=X×X\neg V \cup U \subseteq G\cup G = X\times X, so this uniformity (if it exists) is uniformly regular.

    Now, GG is the union of rectangular open neighborhoods A×BA\times B. Note that since GG is disjoint from the diagonal, any A×BGA\times B \subseteq G satisfies AB=A\cap B = \emptyset. Moreover, since XX is regular, each AA and BB is the union of open sets that are well-inside it; thus GG is the union of rectangular open neighborhoods C×DC\times D such that there are opens A,BA,B with CAC\triangleleft A and DBD\triangleleft B and AB=A\cap B = \emptyset. Since GU=X×XG\cup U = X\times X and X×XX\times X is compact, we can cover it by UU together with finitely many such rectangles C×DC\times D, say X×X=U(C 1×D 1)(C m×D m)X\times X = U \cup (C_1\times D_1) \cup\cdots \cup (C_m \times D_m).

    For each of these rectangles C i×D iC_i\times D_i, let E iE_i be an open set such that E iA iB i=XE_i \cup A_i \cup B_i = X and E i(C iD i)=E_i \cap (C_i \cup D_i) = \emptyset, and let W i=(A i×A i)(B i×B i)(E i×E I)W_i = (A_i\times A_i) \cup (B_i \times B_i) \cup (E_i \times E_I). Then W iW_i is a neighborhood of the diagonal; let W=W 1W mW = W_1 \cap \cdots \cap W_m.

    We claim WWUW\circ W \subseteq U. Let (x,z)WW(x,z) \in W\circ W, so that there is a yy with (x,y)W(x,y)\in W and (y,z)W(y,z) \in W. Now we have either (x,z)U(x,z)\in U (which is what we want) or (x,z)C i×D i(x,z) \in C_i\times D_i for some ii, so it suffices to rule out the latter possibility. Since (x,y)W(x,y)\in W, we have (x,y)W i(x,y) \in W_i, hence (x,y)A i×A i(x,y)\in A_i\times A_i or (x,y)B i×B i(x,y)\in B_i\times B_i or (x,y)E i×E i(x,y)\in E_i\times E_i. But xC ix\in C_i, which is disjoint from B iB_i and E iE_i, so it must be that (x,y)A i×A i(x,y)\in A_i\times A_i and hence yA iy\in A_i. Similarly, we conclude that (y,z)B i×B i(y,z)\in B_i\times B_i so that yB iy\in B_i. But A iB i=A_i\cap B_i = \emptyset, a contradiction.

    It remains to show that the uniform topology on XX is the original one. Clearly if UU is an entourage then each U[x]U[x] is a neighborhood of xx. Conversely, if VV is a neighborhood of xx, then by regularity we have a neighborhood WW of xx and an open GG with WG=W\cap G = \emptyset and GV=XG\cup V = X. Then Z=(V×V)(G×G)Z = (V\times V) \cup (G\times G) is a neighborhood of the diagonal, i.e. an entourage, such that Z[x]=VZ[x] =V.

    We can also conclude, as classically, that this is the unique uniformity compatible with a compact regular topology. Suppose XX is any compact regular uniform space, and UU any neighborhood of the diagonal; we want to show UU is an entourage. For any xXx\in X, there is an entourage VV such that V x[x]×V x[x]UV_x[x] \times V_x[x] \subseteq U. Let W xW_x be an entourage such that W xW xV xW_x \circ W_x \subseteq V_x. Since XX is compact, it is covered by finitely many of the neighborhoods W x[x]W_x[x], say X=W x 1[x 1]W x k[x k]X = W_{x_1}[x_1] \cup \cdots\cup W_{x_k}[x_k]. Let W=W 1W kW = W_1 \cap \cdots \cap W_k; we claim WUW\subseteq U. For let (y,z)W(y,z)\in W; then we have yW x k[x k]y\in W_{x_k}[x_k] for some kk, whence also zV x k[x k]z\in V_{x_k}[x_k], and thus (y,z)V x k[x k]×V x k[x k]U(y,z) \in V_{x_k}[x_k]\times V_{x_k}[x_k] \subseteq U.

    In particular, a compact regular uniform space is automatically uniformly regular as well.

    • CommentRowNumber44.
    • CommentAuthorTobyBartels
    • CommentTimeDec 7th 2016
    • (edited Dec 7th 2016)

    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 GG defines an entourage U GU_G such that (x,y)U G(x, y) \in U_G iff xGyGx \in G \;\Rightarrow\; y \in G, and generate from this subbase.) This quasiuniformity can even be modulated. (On the subbase, and even on the generated base, \sqrt{} 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.)

    • CommentRowNumber45.
    • CommentAuthorTobyBartels
    • CommentTimeDec 7th 2016

    Moreover, it is locally compact, and hence the locale and spatial products X×XX\times X coincide.

    Is this a constructive theorem? But I don't think that it matters, since you seem to only use it to say

    X×XX\times X 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.)

    • CommentRowNumber46.
    • CommentAuthorTobyBartels
    • CommentTimeDec 7th 2016
    • (edited Dec 7th 2016)

    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: XX is quasiregular if, for each point xx and neighbourhood UU of xx, for some neighbourhood VV of xx, UV=XU \cup \setminus V = X. 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.

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2016

    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.

    • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2016

    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.

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2016

    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.

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeDec 8th 2016

    In the paper of Bridges et. al. cited in #8, a subset SS of a uniform space is said to be almost located if for each entourage UU there exists an entourage VV such that U[S]¬V[S]=XU[S] \cup \neg V[S] = X. 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 “SS almost located \Rightarrow U[S]U[S] almost located, for any entourage UU”; but I suppose that is too much to hope for? I don’t have much intuition yet for (almost) located subsets.

    • CommentRowNumber51.
    • CommentAuthorTobyBartels
    • CommentTimeDec 9th 2016

    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!

    • CommentRowNumber52.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2016

    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.

    • CommentRowNumber53.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2016

    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 ff lands in the locale of real numbers and by “complement” we mean the set of real numbers apart from cc”. What does “suitable” mean? (Also, as long as XX 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.

    • CommentRowNumber54.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2016

    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 UU such that if SS is located then so is U[S]U[S]. Are there any uniform spaces that can be shown to satisfy that condition? Even \mathbb{R}?

    • CommentRowNumber55.
    • CommentAuthorMike Shulman
    • CommentTimeDec 13th 2016
    • CommentRowNumber56.
    • CommentAuthorTobyBartels
    • CommentTimeDec 14th 2016

    Good. I edited one place where you improperly let the word ‘located’ stand.

    • CommentRowNumber57.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2016
    • (edited Dec 16th 2016)

    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).