Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeDec 17th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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).

   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).

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeDec 18th 2016
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThat\'s a good observation.

   That's a good observation.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJan 16th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexApparently 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeJan 17th 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 17th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, 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.)

   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.)

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeJan 18th 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexH\'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.)

   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.)

7. • CommentRowNumber7.
   • CommentAuthorTobyBartels
   • CommentTimeJan 18th 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe construction of an anti-uniformity from a uniformity can be expressed in two equivalent ways: * $\exists U,\; A \subseteq X \setminus U$, * $\exists U,\; A \cap U = \emptyset_X$. These suggest two *inequivalent* ways to construct a uniformity from an anti-uniformity: * $\exists A,\; U \supseteq X \setminus A$, * $\exists A,\; U \cup A = X$. The second is coarser, but they are equivalent if the anti-uniformity is uniformly regular.

   The construction of an anti-uniformity from a uniformity can be expressed in two equivalent ways:

   • $\exists U,\; A \subseteq X \setminus U$,
   • $\exists U,\; A \cap U = \emptyset_X$.

   These suggest two inequivalent ways to construct a uniformity from an anti-uniformity:

   • $\exists A,\; U \supseteq X \setminus A$,
   • $\exists A,\; U \cup A = X$.

   The second is coarser, but they are equivalent if the anti-uniformity is uniformly regular.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeJan 18th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex$ \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.

   $\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.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 18th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRe: #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 1. there is a $B$ such that $x\bowtie B$ and $\{ y \mid y\bowtie B\} \subseteq A$ 3. there is a $B$ such that $x\bowtie B$ and $A\cup B = X$ 2. there is a $B$ such that $x\bowtie B$ and $\neg B \subseteq A$ 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.

   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

   1. there is a $B$ such that $x\bowtie B$ and $\{ y \mid y\bowtie B\} \subseteq A$
   2. there is a $B$ such that $x\bowtie B$ and $A\cup B = X$
   3. there is a $B$ such that $x\bowtie B$ and $\neg B \subseteq A$

   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.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex>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[^others]), so maybe we should see how these slight difference affect those examples. [^others]: Do we even have any others, at least for uniform spaces?

    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¹), so maybe we should see how these slight difference affect those examples.

    ---

    1. Do we even have any others, at least for uniform spaces? ↩

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexThe 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.)

    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.)

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGeneralizing 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.

    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.

13. • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexIf 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRight. Sorry, though, that was a digression.

    Right. Sorry, though, that was a digression.

15. • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeJan 19th 2017
    • (edited Jan 19th 2017)
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexLocal 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.

    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.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe 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...

    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…

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOk, I've changed the definition of uniform apartness space as discussed in #5-8.

    Ok, I’ve changed the definition of uniform apartness space as discussed in #5-8.

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAnd 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.

    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.

19. • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeApr 6th 2017
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexI 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.)

    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.)

20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeApr 6th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexInteresting!

    Interesting!