Re: Uniform locales in Shv(X)

Re: Uniform locales in Shv(X)

[Jeff Egger]

Dear Simon,

I was always told that one of the advantages of the "Tukey-style" 
definition (in terms of uniform covers) was that it would be easier to 
generalise toposes than the definition in terms of entourages. And yet, my 
(admittedly cursory) search for this promised generalisation hasn't turned 
up anything yet.

On the other hand, looking at the work of Jorge Picado et al., it seems to 
me---and here, I think, you and I are in agreement---that the only axiom 
which poses any problem is the "admissibility axiom". Specifically, for 
any locale L (internal to any topos E), one can define an object of Weil 
entourages for L: it comprises those elements of the frame underlying LxL 
such that (the nucleus corresponding to) the corresponding open sublocale 
contains (the nucleus corresponding to) the diagonal sublocale. It is 
moreover clear that this object is a meet-semilattice, so it makes sense 
to speak of filters in it---i.e., upward-closed sub-meet-semilattices. A 
Weil uniformity is a filter in this sense satisfying three further axioms: 
square-refinement (which asserts that a certain endomorphism of the filter 
is epi), symmetry (which says the filter is also closed under a further 
unary operation), and the one problematic axiom, "admissibility"; but I 
wonder how important this axiom really is? For locales with enough points, 
it exists to ensure that the topology derived from the uniformity is not 
coarser than the original. Perhaps, if we define a Weil pseudo-uniformity 
on L to be exactly as above minus the admissibility axiom, it is 
possible---at least in the case of a localic topos E=Shv(X)---to describe 
a second locale underlying the pseudouniformity? If so, then we don't 
really need formulate the admissibility axiom in the internal language of 
the topos.

Cheers,
Jeff.



--------------------------------------------
On Thu, 8/21/14, henry@phare.normalesup.org <henry@phare.normalesup.org> wrote:

  Subject: Re: categories: Uniform locales in Shv(X)
  To: "Jeff Egger" <jeffegger@yahoo.ca>
  Cc: categories@mta.ca
  Received: Thursday, August 21, 2014, 7:51 AM

  Dear Jeff,

  I think the problem is that
  (as far as I know) no one has developed a nice
  constructive theory of uniform locale. If
  I'm mistaken about that I would
  be
  really happy to know more about it.

  I have done in my thesis (in chapitre 3 section
  3,
  https://www.imj-prg.fr/~simon.henry/Thesis.pdf)
  the case of constructive
  metric locale,
  under the assumption that the map $Y \rightarrow X$ is
  open. Removing this openness hypothesis seems
  difficult but I stil have
  hope that this is
  possible, and I have a few idea about it...


  For the
  general case it seems to me that the only definition that
  have a
  chance to work properly without the
  openess condition is the definition by
  entourage and this one should be easy to
  externalise: any local section of
  the sheaf
  of entourage will corresponds to an open sublocale of Y
  \times_X
  Y, (containing the restriction of
  the diagonal to the open sublocale of
  $X$ on
  which it is defined ), and it should not be to hard to give
  the
  axioms that these have to satisfy... is
  this the kind of things your are
  looking for
  ?


  Best
  wishes,
  Simon Henry



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[Toby Bartels]

Jeff Egger <jeffegger@yahoo.ca> wrote in part:

>Perhaps, if we define a Weil pseudo-uniformity
>on L to be exactly as above minus the admissibility axiom, it is
>possible---at least in the case of a localic topos E=Shv(X)---to describe
>a second locale underlying the pseudouniformity? If so, then we don't
>really need formulate the admissibility axiom in the internal language of
>the topos.

It seems to me that describing this second locale
will be about as difficult as stating the admissibility axiom.
Indeed, this second locale should be a quotient of the original locale,
and then admissibility simply states that this quotient map is an iso.

The key to stating the admissibility axiom
is what it means for two opens to have "nonempty" intersection.
(If we have enough points, then this means that they have a point in common,
but in general the classical statement "not empty" weaker.)
Mike Shulman suggested on the nLab that A /\ B is "nonempty"
if, whenever it is bounded above by the join of a collection U of opens,
U is inhabited.  But this probably behaves best when the locale is overt.
As far as I know, nobody has worked out the details
(certainly they have not been worked out on the nLab).

This question of overtness may be related to Douglas Bridges's axiom S
in the constructive theory of (point-set) uniform spaces.
There has been some recent discussion of this issue
on the nForum (the discussion forum attached to the nLab):
http://nforum.mathforge.org/discussion/6149/located-uniform-spaces/
(which also has links to the relevant nLab pages).
Overtness is also equivalent to the openness hypothesis used by Simon.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[Jeff Egger]

Hi Toby, 

Many thanks for your comments.  

Over the weekend, I noticed a (probable) mistake in my previous posting: namely, the assertion that _only_ the admissibility axiom could require overtness of the locale  in question.  In fact, the natural way to define composition of entourages (qua relations) is to apply first the inverse image of 
  1xDeltax1 : LxLxL ---> LxLxLxL, 
and then the open image of 
  1x!x1: LxLxL ---> LxL.  
Thus the intuitive way of writing down the square-refinement axiom also requires L to be overt.  (Btw, when discussing that axiom  in my previous post, I carelessly wrote "epi" where I obviously meant "cofinal".)  Perhaps there is some other way of expressing that axiom, but I no longer care: I've reconciled myself to the idea that uniformity requires  overtness.

I also made some progress on 

>> Perhaps, if we define a Weil pseudo-uniformity
>> on L to be exactly as above minus the admissibility axiom, it is
>> possible---at least in the case of a localic topos E=Shv(X)---to describe
>> a second locale underlying the pseudouniformity? If so, then we don't
>> really need formulate the admissibility axiom in the internal language of
>> the topos.

Namely, I have an idea of how this might be done, but it requires a detour through gauge spaces  (=uniformities defined via families of pseudometrics, for those not familiar with the terminology) which I'm not sure is constructively valid.  In any case, I like this idea: in particular, if it works, then one could apply it to the case where L is a discrete locale and investigate to what extent the idea of a uniform space as a _set_ together with a family of entourages fails to capture the general idea.  

Cheers,
Jeff.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[henry]

Hi,

My point about the entourage approach was that it does not require
overtness at least for the basic definitions:

For example, you can state the axiom "for all entourage a there exists an
entourage c such that c.c <= a$ as" using the following form instead of
the composition of entourage:

pi_12 ^* c (intersection) pi_23^* c <= pi_13^*a

where pi_12, pi_23 and pi_13 denotes the three projection from X^3 to X^2.

the uniformly below relation can also be defined as: a is uniformly below
b if there exist an entourage c such that pi_1^* a (intersection) c <=
pi_2^* b and hence you can state the admissibility axiom without
overtness.

The absence of overtness still yields a lots of problems: for example the
uniformly below relation is no longer interpolative. (and I agree that it
is not clear at all that this is the good way of doing things)

When focusing on overt space everything work properly and one can defines
for example completeness and completion (it is actually a direct
consequence of the results about localic metric space in my thesis) but at
some point it yields other problems related to the fact that subspaces of
uniform spaces are no longer uniform space and this gives examples of
things that should be uniform spaces but which are not overt.


If you are willing to restrict to open maps then using the entourage
approach give a not to awful answer to your initial question: a relative
uniform structure on an open map f:Y ->X, is the given by a collection of
a family of open sublocales of Y \times_X Y which correspond to open
sublocales of the form {y_1,y_2,x | x \in U, (y_1,y_2) \in S(x) } for U an
open subset of X and S a section over U of the sheaf of entourage of Y in
sh(X). You just need to write down all the axioms that these things has to
satisfy but they are going to be relatively natural (and if you are only
interested to a notion of "basis of entourage" they I think they are not
going to be to complicated)

Cheers,
Simon

> Hi Toby,?
>
> Many thanks for your comments. ?
>
> Over the weekend, I noticed a (probable) mistake in my previous posting:
> namely, the assertion that _only_ the admissibility axiom could require
> overtness of the locale  in question. ?In fact, the natural way to define
> composition of entourages (qua relations) is to apply first the inverse
> image of?
> ? 1xDeltax1 : LxLxL ---> LxLxLxL,?
> and then the open image of?
> ? 1x!x1: LxLxL ---> LxL. ?
> Thus the intuitive way of writing down the square-refinement axiom also
> requires L to be overt. ?(Btw, when discussing that axiom  in my previous
> post, I carelessly wrote "epi" where I obviously meant "cofinal".)
> ?Perhaps there is some other way of expressing that axiom, but I no longer
> care: I've reconciled myself to the idea that uniformity requires
> overtness.
>
> I also made some progress on?
>
>>> Perhaps, if we define a Weil pseudo-uniformity
>>> on L to be exactly as above minus the admissibility axiom, it is
>>> possible---at least in the case of a localic topos E=Shv(X)---to
>>> describe
>>> a second locale underlying the pseudouniformity? If so, then we don't
>>> really need formulate the admissibility axiom in the internal language
>>> of
>>> the topos.
>
> Namely, I have an idea of how this might be done, but it requires a detour
> through gauge spaces  (=uniformities defined via families of
> pseudometrics, for those not familiar with the terminology) which I'm not
> sure is constructively valid. ?In any case, I like this idea: in
> particular, if it works, then one could apply it to the case where L is a
> discrete locale and investigate to what extent the idea of a uniform space
> as a _set_ together with a family of entourages fails to capture the
> general idea. ?
>
> Cheers,
> Jeff.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[Toby Bartels]

Jeff Egger <jeffegger@yahoo.ca> wrote in part:

>I have an idea of how this might be done, but it requires a detour through gauge spaces [...] which I'm not sure is constructively valid.

Presumably it's not valid if we don't at least have the classical theorem
that every pointwise uniformity comes from a family of psuedometrics.
The proof that I know of this relies on dependent choice,
as well as forming infima of inhabited sets of nonnegative real numbers.
These infima are constructively valid if we allow our pseudometrics
to take values in the upper real numbers instead of only the real numbers.
I don't know what to do about the dependent choice, however.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[Toby Bartels]

I wrote in part:

>I don't know what to do about the dependent choice, however.

Now I do!  Generalize from gauge spaces to prometric spaces.

There is a very precise analogy as follows:
equivalence relation : uniformity :: pseudometric : prometric.
So just as an entourage need not be transitive,
but instead there is a transitivity condition on the entire family,
so a distance map in a prometric need not satisfy the triangle inequality,
but instead a triangle inequality is imposed on the entire family.
A gauge generates a prometric, but not every prometric arises thus.

Then it's straightforward to get the uniformity underlying a prometric,
and also to get a universal gauge or universal prometric from a uniformity.
The question is whether this gives you back your original uniformity,
and this in turn hinges on whether there are enough distance maps
(which in the case of the gauge are pseudometrics) in the prometric.
Specifically, given an entourage U, we need a natural number n
and a uniformly continuous d such that {x,y | d(x,y) < 1/n} is in U.

An argument involving dependent choice and infima says yes, for the gauge.
For the prometric, we have a simpler argument, using only infima.
This argument works internally to any topos with a natural-numbers object
as long as the distance maps in our prometrics are valued in upper reals.

Specifically, given the entourage U, define d_U as follows:
d_U(x,y) := inf {t | t = 0 and (x,y) in U}.
That is, d_U(x,y) = 0 iff (x,y) in U,
and d_U(x,y) = infinity iff (x,y) not in U.
(If you don't want to allow infinite distances, use a finite upper bound;
this gives a different prometric but one with the same uniformity.
You can even get the same prometric by using an unbounded sequence of bounds.)
This violates the triangle inequality whenever U is not transitive,
but d_U(x,z) <= d_V(x,y) + d_V(y,z) when V . V <= U,
so we have a prometric if we start with a uniformity.

So anyway, if you use prometrics valued in upper real numbers,
then every uniformity is prometrizable, even if not gauge-able.

This is all for pointwise spaces, but the construction of d_U
should also work for a uniform cover in a uniform locale.
I have not checked this carefully, however.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[Giovanni Curi]

> Dear all,
>
> I found myself wondering yesterday "what does a uniform locale internal to

> Shv(X) look like?". In theory, this ought to be quite a simple thing: a
> locale map Y-->X equipped with a "fibrewise uniform structure". Has anyone

> already worked out a precise definition for the latter phrase? Pointers to

> relevant literature would be greatly appreciated!
>
>
> Cheers,
> Jeff.



Peter Johnstone started to investigate a theory of uniform locales based on
topos logic in:

"A constructive theory of uniform locales. I. Uniform covers". General
topology and applications (Staten Island, NY, 1989),
179-193, Lecture Notes in Pure and Appl. Math., 134, Dekker, New York, 1991.



As far as I remember, the role of overtness is also discussed in the paper.


An approach to metric and uniform locales that is suited to
constructive predicative systems can be found in


G. Curi, "On the collection of points of a formal space".
Annals of Pure and Applied Logic 137, 1-3, 2006, pp. 126-146,

and

G. Curi, "Constructive metrisability in point-free topology".
Theoretical Computer Science 305 (2003), no. 1-3, 85-109.


With kind regards,

   Giovanni Curi











[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Uniform locales in Shv(X)

[Jeff Egger]

Dear all,

I found myself wondering yesterday "what does a uniform locale internal to 
Shv(X) look like?". In theory, this ought to be quite a simple thing: a 
locale map Y-->X equipped with a "fibrewise uniform structure". Has anyone 
already worked out a precise definition for the latter phrase? Pointers to 
relevant literature would be greatly appreciated!

Cheers,
Jeff.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Uniform locales in Shv(X)

[henry]

Dear Jeff,

I think the problem is that (as far as I know) no one has developed a nice
constructive theory of uniform locale. If I'm mistaken about that I would
be really happy to know more about it.

I have done in my thesis (in chapitre 3 section 3,
https://www.imj-prg.fr/~simon.henry/Thesis.pdf) the case of constructive
metric locale, under the assumption that the map $Y \rightarrow X$ is
open. Removing this openness hypothesis seems difficult but I stil have
hope that this is possible, and I have a few idea about it...


For the general case it seems to me that the only definition that have a
chance to work properly without the openess condition is the definition by
entourage and this one should be easy to externalise: any local section of
the sheaf of entourage will corresponds to an open sublocale of Y \times_X
Y, (containing the restriction of the diagonal to the open sublocale of
$X$ on which it is defined ), and it should not be to hard to give the
axioms that these have to satisfy... is this the kind of things your are
looking for ?


Best wishes,
Simon Henry


> Dear all,
>
> I found myself wondering yesterday "what does a uniform locale internal to
> Shv(X) look like?". In theory, this ought to be quite a simple thing: a
> locale map Y-->X equipped with a "fibrewise uniform structure". Has anyone
> already worked out a precise definition for the latter phrase? Pointers to
> relevant literature would be greatly appreciated!
>
> Cheers,
> Jeff.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]