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.
Created a stubby page uniform locale.
Thanks; I’ve never looked into these.
Thinking about this some more, I am puzzled by the fact that all definitions of uniform locales I have seen use the covering notion of uniformity. (Johnstone’s paper cited at uniform locale bills itself as a “I”, with a sequel promised to cover entourages, but as far as I can tell the sequel never appeared.) If you look at the usual equivalence between entourage and covering uniformities, the passage from an entourage uniformity to a covering uniformity is the direction that refers to points: the basic coverings are those of the form $\{ U[x] \mid x\in X \}$ for entourages $U$, i.e. each basic cover is indexed by the set of points of the space. So it seems clear to me that a treatment using entourages would be more “point-free”. In particular, an entourage, being a subspace of $X\times X$ whose image under one projection to $X$ is all of $X$, can be regarded as a “cover” of $X$ indexed by a space (the space $X$) rather than by a set; so it seems clearly limiting, when our spaces don’t have enough points, to restrict ourselves to covers indexed by sets rather than (point-free) spaces.
This reminds me of Andrew Stacey’s philosophy of “smoothly local” geometry: on has, for instance, charts on a manifold smoothly parameterized by the manifold itself, rather than an indexing set.
Hmm, now I think maybe my brain was turned off – given an entourage $U$, we can instead look at the cover by all opens $V$ such that $V\times V \subseteq U$, which doesn’t refer to points.
To my mind, the problem is that entourages aren't analogous to open subsets; they're analogous to neighbourhoods. You need a point to specify a neighbourhood, whereas you don't to specify an entourage, but that's just a consequence of the reversal of quantifiers when uniformizing: one says $\exists U, \forall x, \forall y, (x,y) \in U \Rightarrow$ (where $U$ is an entourage) in a uniform space, rather than $\forall x, \exists U, \forall y, y \in U \Rightarrow$ (where now $U$ is a neighbourhood of $x$) in a topological space. But they still behave like neighbourhoods, in particular not needing to be open, and that's not natural for locales.
At least the filter of neighbourhoods of a point in a topological space has a base consisting of open neighbourhoods. Does the filter of entourages in a uniform space have a base consisting of open entourages? I don't remember any such result, but it doesn't sound unreasonable.
Yes, the filter of entourages does have a base of open ones. If $U$ is any entourage, then its interior contains any entourage $V$ such that $V\circ V\circ V \subseteq U$, hence is also an entourage.
One apparent problem is that for open subsets $U,V$ of $X\times X$ the composite $U\circ V$ may not be open unless $X$ is overt. But I don’t think that’s really a problem; to say $V\circ V \subseteq U$ we can either interpret $V\circ V$ as a not-necessarily-open sublocale of $X\times X$ (since images of sublocales always exist), or equivalently pull everything back to open parts of $X\times X\times X$.
I fixed the covering-style definition at uniform locale to agree with Johnstone’s in the constructive case, and added what seems to me to be the most natural entourage-style definition.
That looks reasonable. When you say that the equivalence has maybe never appeared in the literature, do you merely mean that it may have never been properly published, or do you mean that it may have never been established at all. In other words, have you verified that they are equivalent?
I have not.
I rephrased to clarify that.
Thanks.
This articles claims that
It is not clear whether these definitions are equivalent. Most references (see below) use only covering uniformities, although Johnstone 89 promises an equivalence to entourage uniformities in a future paper.
I must be missing something, but doesn’t Corollary XII.3.4.3 in Picado and Pultr’s book Frames and Locales prove that these definitions are, in fact, equivalent?
The claim in question was added in Revision 6 by Mike Shulman on December 14, 2016 at 16:18:03.
While attempting to edit this page in order to add a description of the equivalence between covering and entourage uniformities, I encounter an error “Invalid LaTeX block: }”, even if I do not make any changes whatsoever.
In other words, it appears that Instiki/Maruku rejects the current version of this article.
Furthermore, it doesn’t say at what line the error occurs, so it is impossible to fix it.
I don’t have time to look at PP right now. But you could very well be right; probably that comment was written before I had acquired a copy of their book.
Re #15: I have fixed the page now. Impossible was a little strong; if one looked at the rendered page, one could see where the problem was. The new renderer is a little stricter than the old one, so there may be occasional occurrences of this for pages that have not been edited since the new renderer was introduced.
The problem in this case was an awful hack somebody had used to try to render something.
(And even if looking at the rendered page didn’t reveal the problem, one could find the problem by bisection, trying to render the first half of the page, then the first quarter or first three-quarters, etc.)
Re #18: I did think about bisecting, but decided it’s too much effort.
Re #17: Can we make the renderer print the line number where the parsing error occurs?
Fair enough, but there’s a world of difference between “too much effort” and “impossible”. (-:
Re #21: For me, “possible” includes, in particular, ability to overcome my laziness to do some tedious repetitive task. So it may be impossible to do after all!
That reminds me of the way my 6-year-old son uses words like “always” and “never”. E.g. “you never make pizza for dinner!” means “I asked you to make pizza for dinner today and you said no!”.
Added citation
1 to 27 of 27