Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added to uniformly regular space a definition of “uniform apartness space” and a proof that under uniform regularity, these coincide with ordinary uniform spaces. I think this is interesting because it seems to be one of the purposes of uniform regularity (and local decomposability).
That's a good observation.
Apparently my brain was turned off when I wrote that axiom (5) of a uniform apartness space requires uniform regularity to prove from a uniform space. Either that or it’s turned off now, when I think it only needs the direction of de Morgan’s law that holds constructively. I fixed it.
I agree with your brain now.
By the way, I think that you should say ‘anti-entourage’ instead of ‘co-entourage’, to match the use of ‘anti-ideal’ and the like in constructive algebra.
Yes, you’re right. Feel free to fix it, or I will when I have time.
I also have a different suggestion for axiom (2) of a uniform apartness space that doesn’t require uniform regularity to prove from a uniform space, and I suspect sets up an adjunction between uniform spaces and uniform apartness spaces whose fixed points include the uniformly regular ones. Namely, for any anti-entourage $E$ there is an anti-entourage $F$ such that for any $x,y$, if $\neg\forall z, ((x,z)\in E \Rightarrow (y,z) \in F)$ then $(x,y)\in F$. (This comes from syntopogenous transitivity in the biperfect case.)
H'm, and what happens if you write
$\neg\forall z, ((x,z)\in E \Rightarrow (y,z) \in F)$as
$\exists z, ((x,z)\in E \wedge (y,z) \notin F) ?$This looks nicer and is even easier to prove. (Well, the full axiom is easier to prove, because this statement is harder to prove.)
The construction of an anti-uniformity from a uniformity can be expressed in two equivalent ways:
These suggest two inequivalent ways to construct a uniformity from an anti-uniformity:
The second is coarser, but they are equivalent if the anti-uniformity is uniformly regular.
$\exists z, ((x,z)\in E \wedge (y,z) \notin F)$ does seem nicer. I got $\neg\forall z, ((x,z)\in E \Rightarrow (y,z) \in F)$ from the syntopogenous perspective, where an anti-uniformity is described using the relations $A \bowtie_E B$ defined by $\forall x\in A, \forall y\in B, (x,y)\in E$. Currently my best guess at a weak transitivity axiom in that case is that for all $E$ there is an $F$ such that whenever $A\bowtie_E B$ there is a $C$ such that $A\bowtie_F \neg C$ and $C\bowtie_F B$ (as at proximity space).
In the biperfect (uniform) case, if we fix $A=\{x\}$, then we may as well let $B$ be the largest set such that $A\bowtie_E B$, i.e. $B = \{ z \mid (x,z)\in E\}$, and then $C$ the largest set such that $C\bowtie_F B$, i.e. $C = \{ y \mid \forall z\in B, (y,z)\in F \}$, and the remaining assertion is that $A \bowtie_F \neg C$, i.e. that if $y\notin C$, meaning $\neg\forall z, ((x,y)\in E \Rightarrow (y,z)\in F)$, then $(x,y)\in F$.
Your proposal for a weaker axiom (equivalently, for any $x,y,z$, if $(x,z)\in E$ and $(y,z)\notin F$ then $(x,y)\in F$) is I think what we get similarly by fixing both $A=\{x\}$ and $B=\{z\}$. On the other hand, we get an even stronger axiom (but still, I think, provable by negating the entourages of a uniformity) by allowing both $A$ and $B$ to be arbitrary.
I guess probably your axiom is the best one to use in the definition of anti-uniformity, though: it looks cleaner and it treats $x$ and $z$ more even-handedly.
Re: #7 (where I think you mean $X\times X$ everywhere, not $X$), can you prove the transitivity axiom for entourages defined by $\exists A,\; U \cup A = X\times X$? If this holds for some given $U$, we can find an $A$ such that $U\cup A = X\times X$ and then use transitivity for the anti-uniformity to get an anti-entourage $B$ satisfying whatever transitivity, but then we seem to be stuck: there’s no way to get from $B\subseteq X\times X$ to some $V\subseteq X\times X$ such that $V\cup B = X\times X$.
This is something I’ve been puzzling about also in the case of topological spaces and point-set apartness spaces. There there are at least three ways to try to make a topology from a point-set apartness: let $A$ be a neighborhood of $x$ if
The first one is what Bridges et. al. call the “apartness topology” associated to a point-set apartness space. Unfortunately, as far as I can tell it is not functorial from point-set apartness spaces to topological spaces, so it’s at least questionable as a notion of “underlying topology” of an apartness space. The second and third are functorial, but don’t produce a topology, only a pretopological space. However, the third definition sets up an adjunction between pretopological spaces and “pretopological apartness spaces” (those lacking the transitivity axiom), so it seems the best definition category-theoretically, and in the locally decomposable case they all agree.
I suspect that in the uniform case, it’ll also be $\exists A,\; U \supseteq (X\times X) \setminus A$ that participates in an adjunction.
where I think you mean $X\times X$ everywhere, not $X$
Is it too late to say that the set of points of the space is $Y$ and $X$ is defined as $Y \times Y$? :–)
can you prove the transitivity axiom
No, unless we have uniform regularity. Thus, using my new method of defining a uniformity from an anti-uniformity restores the symmetry, that defining one from the other requires uniform regularity. (But you changed the definition of a uniform apartness space so that defining an anti-uniformity from a uniformity does not require uniform regularity, so it's a bad idea after all.)
I am really getting an appreciation for uniform regularity (or local decomposability), that it makes all of the slightly different ways of doing things become equivalent. One reason for not imposing uniform regularity is that there are examples that don't satisfy it (such as arbitrary topological groups^{1}), so maybe we should see how these slight difference affect those examples.
Do we even have any others, at least for uniform spaces? ↩
The really radical step would be requiring local decomposability of every topological space, at least for purposes of analysis. A locally decomposable topological group is uniformly regular, after all.
What examples do we have of important topological spaces, especially in analysis, that cannot be proved locally decomposable? (A discrete space is locally decomposable iff its underlying set has decidable equality, but then those are probably the only sets that should have the discrete topology in constructive analysis.)
Generalizing the discrete-space example, an Alexandrov space is locally decomposable only when the preorder relation is decidable. But probably that’s also not so important in analysis.
(Regarding discrete topologies and decidable equality, Martin Escardo told me once that he thinks decidable equality is more than just having the discrete topology: it should also include being Hausdorff. For instance, a set with semidecidable equality should have the discrete topology but not be Hausdorff. This doesn’t make sense literally interpreted for topological spaces, since every discrete space is Hausdorff at least according to the usual notion of Hausdorff, but it makes perfect sense if you replace “Hausdorff” by another separation axiom like regularity or local decomposability, which together with discreteness imply decidable equality.)
Any gauge space whose distances are located reals is locally decomposable / uniformly regular, and that includes a lot of spaces in analysis. However, I guess there are some gauge spaces in analysis whose distances aren’t constructively located, like $L^\infty$ whose sup-norm is constructively only going to be a lower real number. More generally, there is the example I noticed before that even when $X$ is uniformly regular, the uniformity of uniform convergence on $X^A$ is (apparently) not uniformly regular unless $A$ is covert. Interestingly, with anti-uniform spaces in mind I now notice that as long as $X$ is uniformly regular, $X^A$ also has an anti-uniformity of uniform convergence that dualizes to the uniformity of uniform convergence (but not conversely), and maybe in practice that would be the more relevant structure to pay attention to.
I am a little suspicious of local decomposability because it seems so point-centric; I don’t know what it means for a locale to be locally decomposable. Regularity seems like a more honestly “topological” condition.
If we define ‘Hausdorff’ by requiring a strongly closed diagonal, then it becomes stronger, and for discrete spaces implies stable (but not decidable) equality. You said as much (but without the terminology ‘strongly closed’) at Hausdorff space, and I wrote some more there using this new terminology.
And as you also remarked there, a discrete space (which is always sober) is localically Hausdorff (using strongly closed maps as usual with locales) iff it has decidable equality precisely.
Right. Sorry, though, that was a digression.
Local decomposability does seem point-centric, but I wasn't worried about that, since we seemed to be doing point-wise analysis anyway.
That said, regularity also seems point-centric, but it turns out to have a localic description.
The only ways I’ve been able to think of to write local decomposability localically are either vacuous (if we interpret $\neg V$ as the complementary closed sublocale, since $U \cup \mathsf{C}U = X$ in the lattice of sublocales even constructively) or equivalent to regularity (if we interpret $\neg V$ as the Heyting complement in the lattice of open sets, and replace the point $x$ by a covering of $U$ by opens).
Uniform regularity for a uniform locale might be a nontrivially stronger condition than regularity of the underlying locale, though.
I wonder whether there is a uniform locale of uniform convergence? It’s not obvious to me how to proceed, even classically…
Ok, I’ve changed the definition of uniform apartness space as discussed in #5-8.
And now improved the theorem from an equivalence of uniformly regular spaces to an idempotent adjunction of general spaces, with uniformly regular spaces among the fixed points.
I edited uniform convergence space to reflect the idea that uniform regularity is optional. (By the way, this is another context, besides quasiuniform spaces, where a uniformly regular space need not be regular.)
Interesting!
1 to 20 of 20