Let’s hyperlink DOIs, otherwise what is the point:
Giovanni Curi, On the collection of points of a formal space, Annals of Pure and Applied Logic, 137 1-3 (2006) 126-146 doi:10.1016/j.apal.2005.05.019
* [[Giovanni Curi]], *On the collection of points of a formal space*, Annals of Pure and Applied Logic, **137** 1-3 (2006) 126-146 $[$[doi:10.1016/j.apal.2005.05.019](https://doi.org/10.1016/j.apal.2005.05.019)$]$
adding doi to reference “On the collection of points of a formal space”
Anonymous
]]>Added citation
Noted that since Picado & Pultr use classical logic throughout, it is not immediately clear whether the two definitions of uniform locale also coincide constructively. (It might be the case, but one would have to trace through the proof to be sure, which I haven’t done.)
]]>Complete uniformities. Completion of uniform locales. Criteria for completeness.
]]>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!”.
]]>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!
]]>Rearranged definitions to match Picado-Pultr; removed obsolete claims.
]]>Fair enough, but there’s a world of difference between “too much effort” and “impossible”. (-:
]]>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?
]]>Added the equivalence between entourage uniformities and covering uniformities.
]]>(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 #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.
]]>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.
]]>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.
]]>The claim in question was added in Revision 6 by Mike Shulman on December 14, 2016 at 16:18:03.
]]>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?
]]>Thanks.
]]>I rephrased to clarify that.
]]>I have not.
]]>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 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.
]]>Yes, the filter of entourages does have a base of open ones. If is any entourage, then its interior contains any entourage such that , hence is also an entourage.
One apparent problem is that for open subsets of the composite may not be open unless is overt. But I don’t think that’s really a problem; to say we can either interpret as a not-necessarily-open sublocale of (since images of sublocales always exist), or equivalently pull everything back to open parts of .
]]>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 (where is an entourage) in a uniform space, rather than (where now is a neighbourhood of ) 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.
]]>