Re: Uniform locales in Shv(X)

[Jeff Egger <jeffegger@yahoo.ca>]

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/ ]