Re: Uniform locales in Shv(X)

[Toby Bartels <categories@TobyBartels.name>]

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