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

Discussion Tag Cloud

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
    • CommentTimeJan 24th 2011

    I added the definition of uniform space in terms of covering families. But I don’t know the covering version of the constructive “axiom (0)”.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2011

    Good question. We should go through the proof that the two definitions are equivalent and see how that corresponds.

    I moved some stuff out of the entourage definition to follow the covering definition, but maybe we could move it back and then supplement the covering definition with corresponding material.

    Along the way, I’ve written uniform cover as a separate page (to go along with entourage).

    I’ll come back to the constructive axiom.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeJan 25th 2011

    Well, for now I’ve written in Axiom 0 by secretly translating it into the entourage language. There may be a slicker way to say it.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2011

    Looks great, thank you!

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeNov 16th 2016

    I added a remark that every uniform space comes with an inequality relation.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 16th 2016

    Interesting; that had not occurred to me before.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2016

    Now I see that Toby actually mentioned it here, but it didn’t make it onto the lab at that point.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2016

    Moreover, if the uniform space is “located” as discussed in that thread, then the inequality is an apartness. I added a proof to uniform space, and a remark about this example to apartness relation.

    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 21st 2016
    • (edited Nov 21st 2016)

    On looking up the constructivenews list, Google pointed me also at Bridges’ webpages (I didn’t know he was in New Zealand!), where I found his 2011 book Apartness and Uniformity, which might be of interest.

    Publisher summary:

    The theory presented in this book is developed constructively, is based on a few axioms encapsulating the notion of objects (points and sets) being apart, and encompasses both point-set topology and the theory of uniform spaces. While the classical-logic-based theory of proximity spaces provides some guidance for the theory of apartness, the notion of nearness/proximity does not embody enough algorithmic information for a deep constructive development. The use of constructive (intuitionistic) logic in this book requires much more technical ingenuity than one finds in classical proximity theory – algorithmic information does not come cheaply – but it often reveals distinctions that are rendered invisible by classical logic.

    In the first chapter the authors outline informal constructive logic and set theory, and, briefly, the basic notions and notations for metric and topological spaces. In the second they introduce axioms for a point-set apartness and then explore some of the consequences of those axioms. In particular, they examine a natural topology associated with an apartness space, and relations between various types of continuity of mappings. In the third chapter the authors extend the notion of point-set (pre-)apartness axiomatically to one of (pre-)apartness between subsets of an inhabited set. They then provide axioms for a quasiuniform space, perhaps the most important type of set-set apartness space. Quasiuniform spaces play a major role in the remainder of the chapter, which covers such topics as the connection between uniform and strong continuity (arguably the most technically difficult part of the book), apartness and convergence in function spaces, types of completeness, and neat compactness. Each chapter has a Notes section, in which are found comments on the definitions, results, and proofs, as well as occasional pointers to future work. The book ends with a Postlude that refers to other constructive approaches to topology, with emphasis on the relation between apartness spaces and formal topology.

    Largely an exposition of the authors’ own research, this is the first book dealing with the apartness approach to constructive topology, and is a valuable addition to the literature on constructive mathematics and on topology in computer science. It is aimed at graduate students and advanced researchers in theoretical computer science, mathematics, and logic who are interested in constructive/algorithmic aspects of topology.

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 21st 2016

    This led me to the older paper

    Bridges, D., Schuster, P. and Vîţă, L. (2002), Apartness, Topology, and Uniformity: a Constructive View. Mathematical Logic Quarterly, 48: 16–28.

    which has the ugliest and worst DOI I’ve ever seen. Link for cut/paste: http://dx.doi.org/10.1002/1521-3870(200210)48:1+<16::AID-MALQ16>3.0.CO;2-7 (I’m too lazy to look up the HTML codes for ) or >, both of which appear in that url and would be used in either of the markdown link syntaxes. The raw text also breaks xml as the forum processes it >:-( [end rant] )

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeNov 21st 2016

    http://dx.doi.org/10.1002/1521-3870%28200210%2948:1%2B%3C16::AID-MALQ16%3E3.0.CO;2-7

    But while Mike #8 is about point–point apartness relations, Bridges is talking about point–set apartness and set–set apartness. I would say to see apartness space, but nobody has written that yet, so see proximity space and look for the apartness symbol ‘⋈’.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2016

    It’s very unfortunate that an “apartness space” is not the same as a set equipped with an “apartness relation”!

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 23rd 2016

    Has anyone studied a constructive notion of an “antiuniform space”, i.e. a set equipped with a collection of “anti-entourages” that behave like the complements of the entourages in a classical uniform space?

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeNov 25th 2016

    @Mike #12:

    Well, it is if you use enough adjectives. A point–point apartness space is a set equipped with a point–point apartness relation, a point–set apartness space is a set equipped with a point–set apartness relation; a set–set apartness space is a set equipped with a set–set apartness relation. Only the defaults are different (and even those defaults might vary with the author).

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeDec 13th 2016

    uniform space says “The definition described above is based on entourages… There is an equivalent (but less directly generalisable) definition based on uniform covers.” In what way is the uniform cover definition less directly generalizable? Is it quasi-uniformities you had in mind? (There is a way to do those with covers, isn’t there, even if it’s more awkward?)

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeDec 14th 2016

    I was probably thinking of quasiuniformities, and I don't know how to do those with covers.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2016

    Hmm… I thought I remembered there was a way to do quasiuniformities with covers, but I can’t find the book I thought it was in, and I can’t think right now of how you would do it. I edited the page to clarify.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2017

    I found a reference that describes how to do quasiuniformities with covers: you have to use covers by pairs of sets. For instance, this paper contains a version of the definition for locales. I’ve added to uniform space a citation to what is apparently the original paper that does this, although I haven’t read it.

    • CommentRowNumber19.
    • CommentAuthormaxsnew
    • CommentTimeJun 22nd 2017

    Why is the title of this page “uniform space draft” and not “uniform space”?

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 22nd 2017

    On the assumption that this was a mistake (or left over from an initial attempt), I renamed it.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    Mention two closed monoidal structures on UnifUnif, one symmetric and one not.

    diff, v55, current

  1. I have added a remark that ” The original definition in Bourbaki can be seen as describing a contravariant functor from the category of finite sets to a category of filters of subsets. ” and a reference to a paper describing the construction. ” * {#naive_tame_topology} M. Gavrilovich, A naive diagram-chasing approach to formalisation of tame topology \S3.1.2, \S3.1.6. “

    Perhaps this has to be said differently because the reference is not good: the construction of the functor is trivial, but the sections cited are not self-contained and lack detail.

    Anonymous

    diff, v56, current

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 4th 2018

    This last comment is pretty confusing to me. Why include the reference if you consider it not good?

    • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 4th 2018

    Added arXiv link to the recently added paper by Gavrilovich

    diff, v57, current

  2. I have added a quick construction of the contravariant functor from finite sets to filters associated with a uniform structure, to the section “Categorical Intrepretation”.

    Anonymous

    diff, v58, current

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2018

    (Since these are anonymous edits, their author may not be reading the forum.)

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeFeb 15th 2023

    added pointer to:

    diff, v65, current

    • CommentRowNumber29.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 23rd 2023

    The article currently has no information on limits or colimits in the category of uniform spaces.

    It seems to me that the situation is similar to topological spaces: limits/colimits are computed on the level of underlying sets, equipping them with the final/initial uniformity.

    Is there a written source where this is spelled out?

    diff, v66, current

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2023

    See The Joy of Cats, page 350: that the forgetful functor U;UnifSetU; Unif \to Set is topological guarantees that it works as you say.

    • CommentRowNumber31.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 24th 2023

    Added:

    The category of uniform spaces

    Uniform spaces and uniform maps form a topological category.

    In particular, limits and colimits of uniform spaces are computed similarly to the case of topological spaces: take the limit/colimit of underlying sets and equip it with the final/initial uniform structure.

    See Chapter 21 in Joy of Cats for more information.

    diff, v67, current