Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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)”.
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.
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.
Looks great, thank you!
I added a remark that every uniform space comes with an inequality relation.
Interesting; that had not occurred to me before.
Now I see that Toby actually mentioned it here, but it didn’t make it onto the lab at that point.
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.
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.
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] )
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 ‘⋈’.
It’s very unfortunate that an “apartness space” is not the same as a set equipped with an “apartness relation”!
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?
@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).
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?)
I was probably thinking of quasiuniformities, and I don't know how to do those with covers.
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.
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.
Why is the title of this page “uniform space draft” and not “uniform space”?
On the assumption that this was a mistake (or left over from an initial attempt), I renamed it.
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
This last comment is pretty confusing to me. Why include the reference if you consider it not good?
Added arXiv link to the recently added paper by Gavrilovich
(Since these are anonymous edits, their author may not be reading the forum.)
adding redirects for preuniformity, preuniformities, preuniform space, and preuniform spaces
Anonymous
added pointer to:
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?
See The Joy of Cats, page 350: that the forgetful functor is topological guarantees that it works as you say.
Added:
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.
1 to 31 of 31