# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeJan 25th 2011

Created a stubby page uniform locale.

• CommentRowNumber2.
• CommentAuthorTobyBartels
• CommentTimeJan 25th 2011

Thanks; I’ve never looked into these.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeDec 8th 2016

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.

• CommentRowNumber4.
• CommentAuthorDavidRoberts
• CommentTimeDec 8th 2016

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.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeDec 8th 2016

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.

• CommentRowNumber6.
• CommentAuthorTobyBartels
• CommentTimeDec 9th 2016
• (edited Dec 9th 2016)

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.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeDec 9th 2016

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$.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeDec 14th 2016

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.

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeDec 16th 2016

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?

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeDec 16th 2016

I have not.

• CommentRowNumber11.
• CommentAuthorTobyBartels
• CommentTimeDec 18th 2016

I rephrased to clarify that.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeDec 18th 2016

Thanks.

• CommentRowNumber13.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 25th 2019

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?

• CommentRowNumber14.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 27th 2019

The claim in question was added in Revision 6 by Mike Shulman on December 14, 2016 at 16:18:03.

• CommentRowNumber15.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 27th 2019

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.

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeJul 27th 2019

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.

1. 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.

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeJul 28th 2019

(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.)

• CommentRowNumber19.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 28th 2019

Added the equivalence between entourage uniformities and covering uniformities.

• CommentRowNumber20.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 28th 2019

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?

• CommentRowNumber21.
• CommentAuthorMike Shulman
• CommentTimeJul 28th 2019

Fair enough, but there’s a world of difference between “too much effort” and “impossible”. (-:

• CommentRowNumber22.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 29th 2019

Rearranged definitions to match Picado-Pultr; removed obsolete claims.

• CommentRowNumber23.
• CommentAuthorDmitri Pavlov
• CommentTimeJul 29th 2019
• (edited Jul 29th 2019)

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!

• CommentRowNumber24.
• CommentAuthorMike Shulman
• CommentTimeJul 31st 2019

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!”.

• CommentRowNumber25.
• CommentAuthorDmitri Pavlov
• CommentTimeAug 1st 2019

Complete uniformities. Completion of uniform locales. Criteria for completeness.

• CommentRowNumber26.
• CommentAuthorMike Shulman
• CommentTimeAug 3rd 2019

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.)

• CommentRowNumber27.
• CommentAuthorMike Shulman
• CommentTimeJun 10th 2021