Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeDec 17th 2016

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

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeDec 18th 2016

    That's a good observation.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJan 16th 2017

    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.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeJan 17th 2017

    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.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 17th 2017

    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 EE there is an anti-entourage FF such that for any x,yx,y, if ¬z,((x,z)E(y,z)F)\neg\forall z, ((x,z)\in E \Rightarrow (y,z) \in F) then (x,y)F(x,y)\in F. (This comes from syntopogenous transitivity in the biperfect case.)

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017

    H'm, and what happens if you write

    ¬z,((x,z)E(y,z)F) \neg\forall z, ((x,z)\in E \Rightarrow (y,z) \in F)

    as

    z,((x,z)E(y,z)F)? \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.)

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017

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

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

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

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

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

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2017

    z,((x,z)E(y,z)F) \exists z, ((x,z)\in E \wedge (y,z) \notin F) does seem nicer. I got ¬z,((x,z)E(y,z)F) \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 EBA \bowtie_E B defined by xA,yB,(x,y)E\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 EE there is an FF such that whenever A EBA\bowtie_E B there is a CC such that A F¬CA\bowtie_F \neg C and C FBC\bowtie_F B (as at proximity space).

    In the biperfect (uniform) case, if we fix A={x}A=\{x\}, then we may as well let BB be the largest set such that A EBA\bowtie_E B, i.e. B={z(x,z)E}B = \{ z \mid (x,z)\in E\}, and then CC the largest set such that C FBC\bowtie_F B, i.e. C={yzB,(y,z)F}C = \{ y \mid \forall z\in B, (y,z)\in F \}, and the remaining assertion is that A F¬CA \bowtie_F \neg C, i.e. that if yCy\notin C, meaning ¬z,((x,y)E(y,z)F)\neg\forall z, ((x,y)\in E \Rightarrow (y,z)\in F), then (x,y)F(x,y)\in F.

    Your proposal for a weaker axiom (equivalently, for any x,y,zx,y,z, if (x,z)E(x,z)\in E and (y,z)F(y,z)\notin F then (x,y)F(x,y)\in F) is I think what we get similarly by fixing both A={x}A=\{x\} and B={z}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 AA and BB 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 xx and zz more even-handedly.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2017

    Re: #7 (where I think you mean X×XX\times X everywhere, not XX), can you prove the transitivity axiom for entourages defined by A,UA=X×X\exists A,\; U \cup A = X\times X? If this holds for some given UU, we can find an AA such that UA=X×XU\cup A = X\times X and then use transitivity for the anti-uniformity to get an anti-entourage BB satisfying whatever transitivity, but then we seem to be stuck: there’s no way to get from BX×XB\subseteq X\times X to some VX×XV\subseteq X\times X such that VB=X×XV\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 AA be a neighborhood of xx if

    1. there is a BB such that xBx\bowtie B and {yyB}A\{ y \mid y\bowtie B\} \subseteq A
    2. there is a BB such that xBx\bowtie B and AB=XA\cup B = X
    3. there is a BB such that xBx\bowtie B and ¬BA\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 A,U(X×X)A\exists A,\; U \supseteq (X\times X) \setminus A that participates in an adjunction.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017

    where I think you mean X×XX\times X everywhere, not XX

    Is it too late to say that the set of points of the space is YY and XX is defined as Y×YY \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 groups1), so maybe we should see how these slight difference affect those examples.


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

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017

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

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2017

    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 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 XX is uniformly regular, the uniformity of uniform convergence on X AX^A is (apparently) not uniformly regular unless AA is covert. Interestingly, with anti-uniform spaces in mind I now notice that as long as XX is uniformly regular, X AX^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.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeJan 18th 2017

    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.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2017

    Right. Sorry, though, that was a digression.

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeJan 19th 2017
    • (edited Jan 19th 2017)

    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.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeJan 19th 2017

    The only ways I’ve been able to think of to write local decomposability localically are either vacuous (if we interpret ¬V\neg V as the complementary closed sublocale, since UCU=XU \cup \mathsf{C}U = X in the lattice of sublocales even constructively) or equivalent to regularity (if we interpret ¬V\neg V as the Heyting complement in the lattice of open sets, and replace the point xx by a covering of UU 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…

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

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

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2017

    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.

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeApr 6th 2017

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

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeApr 6th 2017

    Interesting!