Re: Uniform locales in Shv(X)

[henry@phare.normalesup.org]

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