From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8297 Path: news.gmane.org!not-for-mail From: Jeff Egger Newsgroups: gmane.science.mathematics.categories Subject: Re: Uniform locales in Shv(X) Date: Thu, 21 Aug 2014 19:24:19 -0700 Message-ID: References: Reply-To: Jeff Egger NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1408709747 18907 80.91.229.3 (22 Aug 2014 12:15:47 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 22 Aug 2014 12:15:47 +0000 (UTC) Cc: Categories List To: "henry@phare.normalesup.org" Original-X-From: majordomo@mlist.mta.ca Fri Aug 22 14:15:42 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.186]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1XKnkD-0000e7-SY for gsmc-categories@m.gmane.org; Fri, 22 Aug 2014 14:15:02 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58382) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1XKnju-0000cm-Bk; Fri, 22 Aug 2014 09:14:42 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1XKnjs-0006jj-Uy for categories-list@mlist.mta.ca; Fri, 22 Aug 2014 09:14:40 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8297 Archived-At: 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 wrote: Subject: Re: categories: Uniform locales in Shv(X) To: "Jeff Egger" 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/ ]