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
    • CommentTimeDec 13th 2016

    Created apartness space.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeDec 14th 2016

    Nice, but given its coverage, shouldn't point-point apartness space and set-set apartness space redirect to apartness relation and proximity space, respectively?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2016

    Maybe; if you think so, feel free to change it.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeDec 14th 2016

    Done, making sure that these targets have the redirect appropriately in bold somewhere.

    I also edited the main part of apartness space (after the discussion of all of the varieties) to reflect that point–set is the default notion on that page.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeDec 15th 2016

    The distribution of these notions to pages feels a bit odd and haphazard — why are point-point and set-set apartness spaces discussed on pages with other names, but point-set apartness spaces aren’t? — but I can’t think of anything more logical to do.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeDec 16th 2016

    Classically, point–set apartness spaces are simply topological spaces, so we could discuss them at topological space; similarly, point–point apartness spaces are classically just setoids, so we could discuss them at setoid. However, these are big topics even classically, and their relatively minor twisted constructive versions would get lost. For set–set apartnesses, however, both the classically equivalent notion of proximity space and the constructive aspects of the set–set apartness are rather obscure, so it works fine to put everything at proximity space, at least for now.

    Note that both point–point apartness spaces and point–set apartness spaces get their own articles: apartness relation and apartness space, respectively. The way that these words are used is somewhat arbitrary, but it does reflect the difference in emphasis. For a point–point apartness, the emphasis is on the relation, and the topological aspects are secondary; indeed, classically, the topological aspects are trivial. (Note also that setoid redirects to equivalence relation; that is basically the same phenomenon as redirecting point–point apartness space to apartness relation.) But for a point–set apartness, there's a lot more to say about how it behaves as a space; classically, these topological aspects are the whole point. Thus the page titles make sense to me, although they should come with warnings.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2016

    Yeah, I agree with the reasoning; it just doesn’t feel “clean” to me. (-:

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeDec 16th 2016

    I added the missing nullary-unions axiom to the definition at apartness space.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 17th 2016

    I added a discussion of the relationship of point-set apartness spaces to topological spaces: locally (on each set) the apartnesses are a reflective sub-poset of the topologies, but globally not every apartness-continuous map may be topologically continuous.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    I finally got a copy of the Bridges-Vita book cited at apartness space, and updated the page with reference to their definitions, which are actually closer to ours than those of the earlier BSV paper.

    I do still believe that it is silly to equip a point-set apartness space with a separate point-point inequality/apartness relation rather than just defining x#yx#y to mean x{y}x\bowtie \{y\}, especially since the BV axioms make the ambient inequality coincide with this in any T 1T_1 point-set apartness space. The latter may not be symmetric, but if you want it to be, you’re just assuming your space is R 0R_0, which is reasonable (but an extra assumption). Moreover, I believe that the “transitivity” axiom should be stated in terms of the denial inequality; stating it in terms of x{y}x\bowtie \{y\} seems too weak even in classical mathematics (though I haven’t come up with a concrete example yet).

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 20th 2017

    I don't like your nonce use of ‘comparable’, since that also means xyyxx \leq y \;\vee\; y \leq x (said of a pair of elements of a partial order). I have long found it annoying that there seems to be no standard adjective to go with ‘comparison’, but if we're going to invent one, then I'd prefer ‘comparative’ or ‘comparing’. (Where you write ‘comparability’ later on, that should surely be ‘comparison’ I was hoping that ‘comparative’ was spelt ‘comparitive’ to fit that better, but no such luck.)

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeJan 20th 2017

    Are you sure that it's right that T 1\mathrm{T}_1 means

    xyxy? x \ne y \;\Rightarrow\; x \nleq y ?

    I would expect that if \ne is a positive apartness relation itself, but if I'm thinking of \nleq as defining the only positive apartness (or quasi-apartness) relation between points, then I would expect

    ¬(xy)x=y \neg(x \nleq y) \;\Rightarrow\; x = y

    instead. That is, the quasi-apartness is (besides being symmetric, which I guess now needs to be stated separately) tight.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJan 20th 2017

    I guess that what I'm really saying here is that

    xyxy x \ne y \;\Rightarrow\; x \nleq y

    makes sense if you already have an inequality \ne and you want to say that the apartness structure is \ne-T 1\mathrm{T}_1 (or \ne-Fréchet to use more words and fewer symbols). But if you're using the denial inequality, then

    ¬(x=y)xy \neg(x = y) \;\Rightarrow\; x \nleq y

    sounds too strong. That something (in this case, the equality of xx and yy) is false shouldn't be enough to imply a positive result (in this case, that xx is apart from {y}\{y\}). I mean, we shouldn't need Markov's Principle to prove that the real line is T 1\mathrm{T}_1.

    So simply T 1\mathrm{T}_1 should be

    ¬(xy)x=y; \neg(x \nleq y) \;\Rightarrow\; x = y ;

    or rather, R 0\mathrm{R}_0 should be symmetry of \nleq, T 0\mathrm{T}_0 should be

    ¬(xy)¬(yx)x=y, \neg(x \nleq y) \;\wedge\; \neg(y \nleq x) \;\Rightarrow\; x = y ,

    and T 1\mathrm{T}_1 should be R 0T 0\mathrm{R}_0 \wedge \mathrm{T}_0.

    But if \ne is a tight inequality, then

    xyxy x \ne y \;\Rightarrow\; x \nleq y

    is a stronger, \ne-relevant statement that entails T 1\mathrm{T}_1. (And

    xyxyyx x \ne y \;\Rightarrow\; x \nleq y \;\vee\; y \nleq x

    is the stronger, \ne-relevant statement that entails T 0\mathrm{T}_0.)

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017
    • (edited Jan 20th 2017)

    I agree entirely with #12-13; I had actually come to the same conclusion independently but hadn’t updated the article. The “stronger, \neq-relevant statement that entails T 1T_1” I think it would make sense to call \neq-T 1T_1. I would be inclined to call symmetry of \nleq something like “strong R 0R_0”, since while these T 0T_0 and T 1T_1 are actually equivalent to the standard properties for the corresponding topology, symmetry of \nleq is I think appreciably stronger than topological R 0R_0, which is symmetry of ¬(xy)\neg(x\nleq y), the specialization preorder.

    I don’t like the word “comparable” either. At the time I wrote it, I didn’t have a better idea, but now I would suggest something like “weakly locally decomposable” or maybe “pointwise locally decomposable”. For a proximal or syntopogenous apartness space, the general relation that I’m inclined to call “decomposability” is that if ABA\bowtie B then there are a CC and DD such that ADA\bowtie D and CBC\bowtie B and CD=XC\cup D = X. Local decomposability is the restriction to the case A={x}A=\{x\}, and in the left-perfect case we may as well take C={yyB}C = \{ y \mid y \bowtie B \}. “Weak local decomposability” is then what we get by weakening the assumption A={x}DA = \{x\} \bowtie D to a pointwise statement yD,xy\forall y\in D, x\neq y (or, in the denial case, xDx\notin D), in which case we may as well take D={yxy}D = \{ y \mid x\neq y\}. What do you think?

    I like the name “quasi-apartness relation”, meaning I assume an irreflexive comparison. I have been playing around with a weaker notion that I’ve been calling an “anti-preorder”: an irreflexive relation \nleq satisfying (xz)¬(yz)(xy)(x\nleq z) \wedge \neg(y\nleq z) \Rightarrow (x\nleq y). This is the anti-specialization-preorder that you get from a point-set apartness space that isn’t even weakly locally decomposable, and it’s also the same as a principal anti-uniform space with the new definition (which I haven’t managed to put on that page yet either).

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    I also just added to apartness space a simple example showing that axiom 4 written with a non-denial inequality is strictly weaker, even classically (unless the inequality is assumed to be tight, which of course classically forces it to coincide with denial). Bridges+Vita call axiom 4 for the denial inequality (well, something equivalent to it) the “reverse Kolmogorov property”.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    Ok, I fixed T 1T_1 at apartness space.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 23rd 2017

    I’m worried that the whole theory of point-set apartness spaces seems rather example-free. So far the only examples I can think of are:

    • apartness spaces constructed from topological spaces
    • the “discrete” point-set apartness space arising from an apartness relation (or more generally the “Alexandrov apartness” arising from any anti-preorder) in which xAx\bowtie A means yA,x#y\forall y\in A, x#y (which satisfies transitivity relative to ##, not denial \neq)
    • the silly counterexample on the page showing that ##-transitivity is weaker than \neq-transitivity.

    I can’t even show that any anti-uniform space has an underlying point-set apartness space. So what exactly is the point of this theory?

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeJan 23rd 2017

    I don't know, I kind of assumed that it was of interest since it gets listed along with point–point and set–set apartnesses, but maybe it's just thrown in to cover all possibilities.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 24th 2017

    Bridges et al certainly seem interested in it — there’s a whole chapter in their book about it — but they don’t include any non-topological examples as far as I can see.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 27th 2017

    Here are three possible transitivity axioms for a point-set apartness space, all classically equivalent:

    1. If xAx\bowtie A, then x{y¬(yA)}x\bowtie \{ y \mid \neg(y\bowtie A) \}.
    2. If xAx\bowtie A, then x{yB,(yBzA,(zB)))}x\bowtie \{ y \mid \forall B, (y\bowtie B \Rightarrow \exists z\in A, (z\bowtie B))) \}
    3. If xAx\bowtie A, there exists BB such that xBx\bowtie B and y,(yByA)\forall y,(y\notin B \Rightarrow y\bowtie A).

    (1) is the one on the page now, taken from Bridges-Vita. As noted above, I don’t know how to prove it from an anti-uniform space. However, (2) does follow from the transitivity axiom of an anti-uniformity, while (3) follows from the dual of that transitivity axiom (which possibly should also be part of the definition of anti-uniformity). Note that (2) says that if xAx\bowtie A then xx is apart from the (weak) closure of AA in the apartness topology. Also, (1) is a specialization of the transitivity axiom for \bowtie at proximity space to the perfect case, while (3) is a similar specialization of its dual. It’s not clear to me at present whether any of these axioms implies any of the others.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 27th 2017

    And here’s another even weaker one, implied by (1) and (3):

    (4) If xAx\bowtie A, there exists BB such that xBx\bowtie B and for y,¬(yB¬(yA))\forall y, \neg(y\notin B \wedge \neg(y\bowtie A)).

    Together with (1) and (3), these result from weakening the disjunction yByAy\in B \vee y\bowtie A in local decomposability in various ways, from PQP\vee Q to ¬PQ\neg P \Rightarrow Q or ¬QP\neg Q \Rightarrow P or the weakest ¬(¬P¬Q)\neg (\neg P \wedge \neg Q).

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 29th 2017

    Slightly OT, but I found the discussion here on separation axioms interesting (and curious to know how things go when passing to a constructive setting)

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeJan 29th 2017

    As far as analysis goes, sure, T 3½T_{3½} (which this writer calls ‘complete regularity’) is what you need. I have no objection to that cutoff between lower and higher. I think that a lot of the time you hear a lot about Hausdorffness simply because, at least in analysis, all of your spaces are already completely regular (which I guess that this writer would call ‘complete regularity of the T 0T_0 quotient’) and T 2T_2 is the most well-known concept between T 0T_0 and T 3½T_{3½} (possibly for historical reasons having to do with Bourbaki's dropping that axiom from Hausdorff's original definition of topological space, so that for a while one had to make a big point about whether one was assuming it or not).

    But the writer loses me when they start talking about all of the extra structure that you can only put on a T 3½T_{3½} space. I guess that they've never heard of preproximity spaces (which are called simply ‘proximity spaces’ by some authors, as we've discussed here) and quasiproximity spaces, uniform convergence spaces and quasiuniform spaces, and so forth.

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeJan 29th 2017

    Interesting post. I think the fact that complete regularity is the boundary between quasiproximity/quasiuniformity and proximity/uniformity proper suggests that a more evocative name for the “lower/higher” distinction would be “asymmetric/symmetric”. That is, the topology of completely regular spaces is “symmetric topology”, while that of arbitrary spaces is “asymmetric topology”.

    It also suggests that constructively, the appropriate version of “complete regularity” would be one that maintains this meaning. For this purpose I quite like the notion of “strongly regular” in this paper, which is essentially by definition the existence of a (finest) proximally-regular (or “decomposable”) proximity compatible with the topology. Though they don’t use that terminology for some reason (maybe they don’t know about proximities? Proximities seem to be under-appreciated in the point-free topology community.)

    • CommentRowNumber25.
    • CommentAuthorTobyBartels
    • CommentTimeJan 29th 2017

    That is, the topology of completely regular spaces is “symmetric topology”, while that of arbitrary spaces is “asymmetric topology”.

    Well, ‘symmetric topology’ is already a term in the literature for an R 0R_0 topology, that is a topology whose specialization preorder is symmetric. (But here, ‘topology’ is used in the sense of a structure on a set, not a field of mathematics.) Incidentally, the ‘R’ in ‘R 0R_0’ stands for ‘regular’; that is, this notation is meant to suggest that it should be considered a weak regularity axiom. But we see that such a space is not symmetric in all respects, as the natural quasiuniformity on it, for example, is not symmetric.

    I quite like the notion of “strongly regular”

    Yes, that looks very nice! This seems to be the notion of complete regularity that I've been wanting, equivalent to being a subspace (in the sense of a sublocale, at least) of a compactum. (I notice that the paper is impredicative because it avoids Dependent Choice; if one accepted DC, then one could be predicative again.)

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeJan 29th 2017

    But if one accepts DC, then there is nothing wrong with the classical notion of complete regularity, is there?

    • CommentRowNumber27.
    • CommentAuthorTobyBartels
    • CommentTimeJan 29th 2017

    If one accepts DC, then classical regularity is the same as strong regularity; so either way, strong regularity is the property that we want. But how to define it? With DC, a predicative definition is available; without DC, a predicative definition is not known. Of course, life is like that sometimes; you can't have everything.

    • CommentRowNumber28.
    • CommentAuthorTobyBartels
    • CommentTimeJan 29th 2017
    • (edited Jan 29th 2017)

    Well, it's too much to say that one cannot define strong regularity at all, but one cannot define the relation () (≺)_\circ. Instead, you say that a space is strongly regular if there exists an interpolative relation contained in \prec such that …. (I've had some thoughts along that line myself, but I never pursued them, partly because I doubted that it would actually work!) And to judge from the proof on the bottom of page 4, it appears that the author did just that in an earlier paper (although one would have to check the details to see if it's all predicative).

    What remains, however, is that one cannot define the relation () (≺)_\circ predicatively; whereas () *(≺)_*, which can be defined predicatively, is of no interest without DC.

    Come to think of, ‘has a uniformity’ should also be expressible predicatively (although, as far as I can see, not ‘has a [regular] compactification’, that is not directly).

    Incidentally, I had thought that the usual term for what this paper calls ‘interpolative relation’ was ‘dense relation’, but I can only find references for ‘dense order’ (which means an interpolative quasiorder). (Well, ‘dense relation’ is on the Wikipedia page for dense orders, but marked [citation needed], and Google book search does not find it in the references for that page. Both terms also appear as neologisms with other meanings in other papers.)

    ETA: (The subscript ‘\circ’ is too small here, at least as I see it. But that's a font issue; the character here is correct, and it looks fine in Computer Modern.)

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeJan 29th 2017

    Makes sense. Something still seems off, though, because they claim (Proposition, p4) that in particular every uniform locale is strongly regular; but we know that constructively, not every uniform space is regular. Their proof of that direction cites another paper, which I don’t have in front of me to tell how constructive it is; but their use of sa0s\wedge a \neq 0 in defining 𝔘\lhd_{\mathfrak{U}} doesn’t fill me with confidence.

    • CommentRowNumber30.
    • CommentAuthorTobyBartels
    • CommentTimeJan 30th 2017
    • (edited Jan 30th 2017)

    If they're using a constructive theory of uniform locales that we're ignorant of, then it might well incorporate uniform regularity, just as Bridges does for uniform point–set spaces. Do we have any reason to doubt that uniform regularity implies strong regularity?

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJan 30th 2017

    I suppose that’s true. I think I believe that uniform regularity implies strong regularity for spaces. I’m a little dubious that it would work constructively for locales unless the locale is at least overt. I don’t know how to show that 𝔘\lhd_{\mathfrak{U}} is interpolative otherwise, since the natural interpolating set is defined as an image under projecting away the locale itself, which won’t be open unless the locale is overt. Curi’s paper cited at uniform locale (which defines uniformities in terms of a “gauge of diameters”) requires overtness as part of the definition; but the Banaschewski-Pultr paper doesn’t mention overtness anywhere.

    Another reason I’m doubtful of the constructivity of their other paper is that Picado & Pultr’s book on locale theory is relentlessly classical, despite the fact that on the cover they tout constructivity as one of the benefits of locale theory. Also, Curi’s paper, which is 4 years more recent than Banaschewski-Pultr, doesn’t cite any other work on constructive uniform locale theory more recent than Johnstone (Remark 3.3).

    • CommentRowNumber32.
    • CommentAuthorTim_Porter
    • CommentTimeJan 31st 2017

    By coincidence I find I am writing a review of :ASYMPTOTIC RESEMBLANCE, by SH. KALANTARI AND B. HONARI, ROCKY MOUNTAIN JOURNAL OF MATHEMATICS Volume 46, Number 4, 2016. This looks at an analogue of proximity for coarse structures. I do not know if others have seen this.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 1st 2017