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.
    • CommentAuthorMike Shulman
    • CommentTimeAug 16th 2012

    Added a bit more to proximity space.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJun 29th 2014

    I rearranged this to give about equal emphasis to the three relations δ,,\delta, \bowtie, \ll. Also more on quasiproximities and on the preorder implicitly involved in the definition of a separated proximity.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeJul 4th 2014
    • (edited Jul 4th 2014)

    Our definition of proximity came from the one at the English Wikipedia, but I don't think that it's right, for two reasons:

    • A quasiproximity should be the same thing as a topogenous relation at syntopogenous space (and we state as much on both pages), but we have an extra requirement of Regularity.
    • The Springer Encyclopedia of Math treats Regularity1 as an optional separation axiom, like Separatedness, and this makes a lot of sense to me. In fact, I can even distingish two ways of stating Separatedness so that one corresponds to T 1T_1, one corresponds to T 2T_2, the first is weaker than the second, and they are equivalent given Regularity. That is perfect.

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


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

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJul 5th 2014

    I think the point is the theorem about proximities corresponding to compactifications. Won’t that fail if you omit regularity?

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJul 5th 2014
    • (edited Jul 5th 2014)

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJul 6th 2014

    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.

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJul 9th 2014

    Yes, but nonregular (quasi)-proximities are good for more than just syntopogenous spaces. For example, given any pseudotopological space, let ABA \ll B iff AInt(B)A \subseteq Int(B); 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.)

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeJul 10th 2014

    I am coming around more to the view that Regularity is more fundamental (and so should probably get a different name). Assuming isotony, Reflexivity (ABABA \ll B \;\Rightarrow\; A \subseteq B) and Regularity combine to form the following unbiased axiom:

    If ABA \ll B, then, for every n=0,1,2,n = 0, 1, 2, \ldots, for some C 0,C 1,,C nC_0, C_1, \ldots, C_n,

    AC 0C 1C nB. A \subseteq C_0 \ll C_1 \ll \cdots \ll C_n \subseteq B .

    (Changing If to Iff here (and being careful with the placement of nn), 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).

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJul 10th 2014

    Yes, I agree.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeJul 10th 2014
    • (edited Jan 1st 2017)

    It's interesting that Regularity is the one axiom that (when expressed using \ll) makes no reference to the lattice structure of the algebra of posets whatsoever; it simply states that \ll is a dense order. (Well, that's thinking of \ll 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 \subseteq is like a ring and \ll is like an ideal; \ll 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, \ll can only be reflexive if it reduces to \subseteq precisely, just an ideal with a unit must be the entire ring.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJul 12th 2014

    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 (A,B)(A,B) where ABA \subseteq B (writing \subseteq 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 AbAb if that's more familiar), the analogue of Regularity is a condition that I've never seen before; it says that if xx is in the ideal then x=yzx = y z for some yy and zz 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.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJul 13th 2014

    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.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJul 13th 2014
    • (edited Jul 13th 2014)

    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 MM to MMM \otimes M. 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 xzx \ll z, there is some yy such that xyzx \ll y \ll z, we have an operation that, given xzx \ll z, gives us an equivalence class of yy such that xyzx \ll y \ll z, where yy is equivalent to yy' if yyy \subseteq y' (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.

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeJul 14th 2014

    I've written this up at proximity space#profunctors.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeJul 18th 2014

    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.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeJul 18th 2014

    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.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJul 19th 2014

    Ah, excellent. I was surprised if we’d missed something like that.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeDec 17th 2016

    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 \bowtie, 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 “ε2\frac{\varepsilon}{2} 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?

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeDec 18th 2016

    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.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeDec 18th 2016

    Let’s see, here’s the syntopogeny condition:

    (δ\delta) For any δ\delta, there exists a δ\delta' such that if A,BXA,B\subseteq X have the property that whenever CD=XC\cup D = X, either AδCA\;\delta'\; C or DδBD\;\delta'\; B, then AδBA\;\delta\; B.

    I can think of three natural (classically-equivalent) ways to contrapose this to a condition on \bowtie relations:

    (\bowtie1) For any \bowtie, there exists a \bowtie' such that whenever ABA\bowtie B, there exist CC and DD such that ACA \bowtie' C, DBD\bowtie' B, and CD=XC\cup D = X.

    (\bowtie2) For any \bowtie, there exists a \bowtie' such that whenever ABA\bowtie B, there exist CC and DD such that ACA \bowtie' C, DBD\bowtie' B, and (XC)D(X\setminus C)\subseteq D.

    (\bowtie3) For any \bowtie, there exists a \bowtie' such that whenever ABA\bowtie B, there exist CC and DD such that ACA \bowtie' C, DBD\bowtie' B, and (XD)C(X\setminus D) \subseteq C.

    The version of (\bowtie1) in the “simple” case (=\bowtie=\bowtie') is that currently appearing under “Normality (constructive)” at proximity space. Of course, (\bowtie2) and (\bowtie3) are equivalent if we have symmetry. On the other hand, under (left) perfection, in all three conditions we may as well take D={xxB}D = \{ x \mid x\bowtie' B \}. Moreover, under perfection it is natural to also consider the weakened versions where AA is a singleton:

    (\bowtie1P) For any \bowtie, there exists a \bowtie' such that whenever xBx\bowtie B, there exists CC such that xCx \bowtie' C and y,(yCyB)\forall y, (y\in C \vee y\bowtie' B).

    (\bowtie2P) For any \bowtie, there exists a \bowtie' such that whenever xBx\bowtie B, there exists CC such that xCx \bowtie' C and y,(yCyB)\forall y, (y\notin C \to y\bowtie' B).

    (\bowtie3P) For any \bowtie, there exists a \bowtie' such that whenever xBx\bowtie B, there exists CC such that xCx \bowtie' C and y,(¬(yB)yC)\forall y, (\neg(y\bowtie' B) \to y\in C).

    In (\bowtie3P) we also may as well take C={y¬(yB)}C = \{ y \mid \neg(y\bowtie' B) \}, giving the equivalent:

    (\bowtie3P) For any \bowtie, there exists a \bowtie' such that whenever xBx\bowtie B we have x{y¬(yB)}x \bowtie' \{ y \mid \neg(y\bowtie' B) \}.

    Similarly, I can think of two (classically-equivalent) ways to translate (δ\delta) into a condition on \ll relations:

    (\ll1) For any \ll, there exists a \ll' such that whenever ABA\ll B, there exist CC and DD such that ACA\ll' C, DBD\ll' B, and (XC)D=X(X\setminus C) \cup D = X.

    (\ll2) For any \ll, there exists a \ll' such that whenever ABA\ll B, there exist CC and DD such that ACDBA\ll' C\subseteq D\ll' B.

    Of course, in (\ll2) it is equivalent to take C=DC=D:

    (\ll2) For any \ll, there exists a \ll' such that whenever ABA\ll B, there exists DD such that ADBA\ll' D\ll' B.

    These two (constructively) equivalent versions of (\ll2) are the ones currently appearing under “Normality (constructive)” and “Normality (simplified)” at proximity space. Under (left) perfection, we can take D={yyB}D = \{ y \mid y \ll' B \} in both conditions, and then it is natural to also consider the restricted versions where AA is a singleton:

    (\ll1P) For any \ll, there exists a \ll' such that whenever xBx\ll B, there exists CC such that xCx\ll' C and y,(yCyB)\forall y, (y\notin C \vee y \ll' B).

    (\ll2P) For any \ll, there exists a \ll' such that whenever xBx\ll B, we have x{yyB}x\ll' \{ y \mid y \ll' B\}.

    (continued…)

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeDec 18th 2016

    Now how are all these conditions related to known definitions? Consider first the case of a simple perfect syntopogeny (so =\bowtie =\bowtie' or =\ll=\ll'), giving notions of topological space:

    1. Condition (\ll2P) is exactly the condition on a collection of neighborhood filters (a perfect topogenous order \ll) for it to define a topology. Moreover, in the perfect case, (\ll2P) is equivalent to (\ll2).

    2. Condition (\ll1P) implies (\ll2P), so it defines an extra condition on a topological space. In fact it is precisely local decomposability.

    3. Condition (\ll1) implies (\ll1P), 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 UUU\ll U, it requires that every open set is complemented.

    4. Condition (\bowtie3P) 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 (\bowtie3P).) Moreover, in the perfect case, (\bowtie3P) is equivalent to (\bowtie3).

    5. Condition (\bowtie1P) is again precisely local decomposability for a point-set apartness space.

    6. Condition (\bowtie2P) 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.

    7. Condition (\bowtie1) is unreasonably strong constructively: it implies that the basic opens {xxB}\{ x\mid x\bowtie B\} are all complemented. Condition (\bowtie2) is also too strong: it asserts that the basic opens are complements.

    Now consider instead a biperfect symmetric syntopogeny, giving notions of uniform space.

    1. Condition (\bowtie1P) is the one that I used to define a uniform apartness space: Given a co-entourage EE, there is a co-entourage FF such that whenever (x,z)E(x,z)\in E, for any yy we have either (x,y)F(x,y)\in F or (y,z)F(y,z)\in F. In particular, it is true for the notion of apartness defined by a uniformly regular uniform space.

    2. Conditions (\bowtie2P) and (\bowtie3P) (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).

    3. Conditions (\bowtie2) and (\bowtie3) seem stronger than (\bowtie2P) and (\bowtie3P), but are still always satisfied by the complements of entourages of a uniform space. For if UU is an entourage such that (x,y)U(x,y)\notin U for all xAx\in A and yBy\in B, let VV be an entourage such that VVUV\circ V \subseteq U. With C={yxA,(x,y)V}C = \{ y \mid \forall x\in A, (x,y)\notin V \} and D={yzB,(y,z)V}D = \{ y \mid \forall z\in B, (y,z)\notin V \} we have A VCA\bowtie_V C and D VBD\bowtie_V B. And if yy is such that ¬zB,(y,z)V\neg\forall z\in B, (y,z)\notin V and (x,y)V(x,y)\in V for some xAx\in A, then for any zBz\in B we have (y,z)V(y,z)\notin V since (x,z)U(x,z)\notin U, a contradiction; thus (XD)C(X\setminus D)\subseteq C.

    4. I can’t make much sence of the right perfection condition stated for \ll at proximity space, but it seems to me that in the biperfect case, a \ll relation is essentially equivalent to a δ\delta relation: to say that xBx\ll B should be the same as saying xδyyBx \;\delta\; y \to y\in B for all yy. Under this translation, condition (\ll2P) is just the usual ε2\frac{\varepsilon}{2} condition in the definition of a uniformity, and is equivalent to (\ll2).

    5. Condition (\ll1P), I believe, translates exactly to uniform regularity (combined with ε2\frac{\varepsilon}{2}).

    6. Conditions (\bowtie1) and (\ll1) seem unreasonably strong: in addition to ε2\frac{\varepsilon}{2}, they imply that all subsets of XX are almost located.

    (continued…)

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeDec 18th 2016

    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 (\bowtie1) or (\ll1) as the definition constructively, but rather (\bowtie3) or (\ll2). The observations above show that any uniform space has an underlying proximal neighborhood space satisfying (\ll2), and if it is uniformly regular then it has an underlying set-set apartness space satisfying (\bowtie3). (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 (\bowtie3) and (\ll2) in the definition, I would lean towards “transitivity”, because it would seem reasonable to call conditions (\bowtie1) and (\ll1) 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.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeDec 19th 2016

    A rule of thumb in constructive mathematics is to treat negation with suspicion; thus, (\bowtie1) and (\ll2) 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 (\bowtie1). Letting every subset be located, even subsets such as {x|P}\{ x \;|\; P \} for an arbitrary constant proposition PP, is way too strong.

    Indeed, if the obvious simple \bowtie structure on an inhabited metric space satisfies (\bowtie1) , then the forbidden de Morgan law follows (hence LLPO, etc).

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeDec 19th 2016
    • (edited Dec 19th 2016)

    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 \mathbb{R}. One would not expect this to match the usual definition without a bit of countable choice.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeDec 19th 2016

    We should be able to get rid of the countable choice gap by asking for a “modulated” version, no?

    • CommentRowNumber26.
    • CommentAuthorTobyBartels
    • CommentTimeDec 20th 2016

    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.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeDec 26th 2016

    Well, I can’t see how to prove that even a metric space satisfies (\bowtie1) or (\ll1) 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:

    • Whenever {x}A\{x\}\ll A, there exist BB, CC and DD such that CDC\ll D and AC=XA\cup C = X and {x}B\{x\} \ll B and BD=B\cap D = \emptyset.

    To get regularity, take AA to be open and consider the interiors of BB and DD. To get this from uniform regularity, if (x,y)U(x,y)\in U implies yAy\in A, take VV such that U¬V=X×XU\cup \neg V = X\times X and WW such that WWVW\circ W \subseteq V, and let C={y(x,y)V}C = \{ y \mid (x,y)\notin V\} and D={y(x,y)W}D = \{ y \mid (x,y)\notin W\} and B={y(x,y)W}B = \{ y \mid (x,y)\in W\}.

    We could simplify the axiom by taking B=¬DB = \neg D or D=¬BD = \neg B.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeDec 26th 2016

    Also, I don’t think I like the axiom for \ll labeled “Symmetry (constructive)” at proximity space. It’s actually weaker constructively than the one labeled “Symmetry (simplified)” — its hypotheses ensure that D¬BD\subseteq \neg B and ¬AC\neg A \subseteq C, so ¬B¬A\neg B \ll \neg A implies DCD\ll C 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 \ll seems likely to be too weak, but I can’t think of any way to strengthen it that doesn’t amount to regularity.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeDec 26th 2016

    I renamed “Normality” to “Transitivity” at proximity space, and added a remark about it to the Warnings about terminology.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeDec 26th 2016

    I don’t like the notation BB' for the complement of BB; it’s too light and easy to miss for such a drastic operation. Can we switch to something like ¬B\neg B or B\sim B at proximity space?

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeDec 26th 2016

    As for the “Transitivity (constructive)” row, its current entry for \ll is boringly equivalent to the “simplified” version, while its entry for \bowtie is too strong. My lengthy discussion above suggests removing this row entirely and changing the “simplified” version for \bowtie (which is currently equivalent to my (\bowtie2)) to my (\bowtie3) by switching DD and DD'.

    For δ\delta, I would also switch DD and DD' in the “simplified” version (which in this case is stronger than the “constructive” one) to get “if for every DD either AδDA\;\delta\; D' or DδBD\;\delta\; B, then AδBA\;\delta\; B”. I think this is also true in any quasi-uniform space, where AδBA\;\delta\; B means UxA,yB,(x,y)U\forall U '\exists x\in A, \exists y\in B, (x,y)\in U: given an entourage UU, let VV be such that VVUV\circ V \subseteq U and D={yxA,(x,y)V}D = \{ y \mid \exists x\in A, (x,y)\in V\}; then clearly ¬(AδD)\neg (A\;\delta\; D'), so DδBD\;\delta\; B, so we have yDy\in D (so that xA,(x,y)V\exists x\in A, (x,y)\in V) and also zBz\in B such that (y,z)V(y,z)\in V, hence (x,z)U(x,z)\in U.

    Does that sound ok?

    • CommentRowNumber32.
    • CommentAuthorTobyBartels
    • CommentTimeDec 28th 2016

    Go ahead and edit, and I'll bring it up if I don't like how it looks.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeDec 28th 2016

    Okay, I have:

    1. Switched to B cB^{\mathsf{c}} for the complement of BB – I couldn’t figure out how to make \sim behave like a unary operator in iTeX
    2. Divided Symmetry up differently into a weak “if-then” version and a strong “iff” version, the latter being too strong for constructive neighborhoods (in #28 I didn’t notice that the simplified version was stated as an iff).
    3. Modified Transitivity as suggested in #31
    4. Added the Regularity axiom suggested in #27 for \ll, and some classically-equivalent versions for δ\delta and \bowtie
    5. Changed the Right Perfection axiom for \ll to one that I think is equivalent (given Isotony) but is much easier for me to parse
    6. Edited the remarks afterwards to conform to these changes.
    7. Added some more details about the relation between proximities and topologies and uniformities in constructive mathematics.
    • CommentRowNumber34.
    • CommentAuthorTobyBartels
    • CommentTimeDec 30th 2016

    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.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2016

    Thanks!

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2016

    Back on #13-14, proximities as profunctors, I would think that if we are talking about Ω\Omega-enriched profunctors then there is no extra structure to be gotten rid of, since composites of Ω\Omega-enriched profunctors are just relational composites. Am I missing something?

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeJan 1st 2017

    I added some further remarks on the relationship between the three definitions constructively. It seems to me that \ll contains strictly more information that \bowtie, since the latter is determined by its restriction to complements, whereas the axioms of δ\delta are just too strong to be reasonable. I haven’t been able to think of a way to define a \ll in terms of \bowtie that works for proximities (or more general syntopogenies), although there are point-based ways that work for point-set apartnesses and uniform apartnesses.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2017

    Oh! There is a way to define a proximity from a uniform space that satisfies (\bowtie1) or (\ll1): instead of the obvious definition (ABA\ll B if there is an entourage UU such that U[A]BU[A]\subseteq B), say that ABA\ll B if there is a uniformly continuous function f:Xf:X\to \mathbb{R} such that f 1(0,)A=f^{-1}(0,\infty)\cap A=\emptyset and f 1(,1)Bf^{-1}(-\infty,1)\subseteq B, and similarly. And conversely, conditions (\bowtie1) and (\ll1) 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 UU and point xx, there is a uniformly continuous function f:Xf:X\to \mathbb{R} such that f(x)=0f(x)=0 and f 1(,1)U[x]f^{-1}(-\infty,1) \subseteq U[x] and yz,(y,z)U|f(y)f(z)|<1\forall y\forall z, (y,z)\in U \Rightarrow |f(y)-f(z)|\lt 1 (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 (\bowtie1) or (\ll1), if we define say A UBA\ll_U B to mean there is a uniformly continuous function f:Xf:X\to \mathbb{R} such that f 1(0,)A=f^{-1}(0,\infty)\cap A=\emptyset and f 1(,1)Bf^{-1}(-\infty,1)\subseteq B and also yz,(y,z)U|f(y)f(z)|<1\forall y\forall z, (y,z)\in U \Rightarrow |f(y)-f(z)|\lt 1. 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.

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2017

    Unrelatedly, it occurs to me that in addition to δ,,\delta,\bowtie,\ll 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 “AB=XA\Cup B = X” (where XX is the proximity space), defined classically to mean A cB cA^{\mathsf{c}} \bowtie B^{\mathsf{c}}. Its Complete Regularity axiom is probably “if AB=XA\Cup B = X, there exist CC and DD such that AD=XA\Cup D = X and CB=XC\Cup B = X and CD=C\cap D = \emptyset”; but I don’t immediately see how to formulate any weaker notion of Transitivity for it.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJan 5th 2017

    I added Complete Regularity to the list of axioms at proximity space, along with the above remarks, and a proof that assuming Complete Regularity \bowtie and \ll are inter-definable. I am not sure how to state Complete Regularity for δ\delta, and δ\delta seems unreasonable anyway constructively, so I left it blank.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeJan 5th 2017

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

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeJan 5th 2017

    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.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeJul 7th 2018

    Add example from Bridges-Vita that a non-Decomposable proximity space need not be induced by a uniform space in the usual way.

    diff, v34, current