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 beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics comma complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity 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 infinity integration integration-theory k-theory lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topological topology topos topos-theory type type-theory 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.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeFeb 10th 2018
    • (edited Feb 10th 2018)

    Let XX be a set with an apartness relation. We can then define a subset UU of XX to be open if and only if

    x,y.(xUyUx#y). \forall x, y. (x \in U \Rightarrow y \in U \vee x # y).

    In that way, XX becomes a topological space. As detailed at apartness relation, the induced locale XX' can be described as a certain quotient of the discrete locale over XX in the category of locales.

    I’m trying to work out what the points of this locale are. The canonical continuous map

    XPt(X),x{UX|Uopen,xU} X \longrightarrow Pt(X'), x \mapsto \{ U \subseteq X | U open, x \in U \}

    factors over X/X/\sim, where ()({\sim}) is the equivalence relation induced by the apartness, and I can show that the resulting map X/Pt(X){X/{\sim}} \to Pt(X') is injective. Is it surjective?

    (Assuming classical logic, it is. In this case furthermore XX' is a locally compact locale. But I need an intuitionistic proof.)

    My motivation is as follows. It’s possible to pass from XX to the quotient set X/X/{\sim}; however, as we know, this loses information and is badly behaved in some sense. If the points of XX' turned out to be the elements of X/X/{\sim}, we could subscribe to the following philosophy: “Sure you can consider the quotient. Just make sure to consider it in the category of locales instead of sets. The localic quotient will have exactly the points you expect, but will come with additional ’glue’ to create a well-behaved object.”

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2018

    In other words, the question is whether the apartness topology on XX is sober?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2018

    Well, that’s the question if the apartness is tight. Otherwise the question is whether it satisfies the “other half” of sobriety (the first half being essentially tightness of the apartness relation). Right?

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 11th 2018

    As an aside, at sober space there is a broken reference

    \ref{OpenSubsetVersionOfClosedIrreducible}

    • CommentRowNumber5.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeFeb 11th 2018
    • (edited Feb 11th 2018)

    Mike: Yes, exactly. The proof in classical logic exploits the subsets

    U x{yX|¬(x#y)}, U_x \coloneqq \{ y \in X \,|\, \neg(x # y) \},

    which we can classically prove to be open. (Surjectivity of the canonical map alluded to above then follows like this: Let FF be a completely prime filter. Since X= xXU xFX = \bigcup_{x \in X} U_x \in F, there is an element xXx \in X such that U xFU_x \in F. One can then show that FF is the image of [x][x]. To verify that XX' is locally compact, observe that any open subset UU can be written as the union xUU x\bigcup_{x \in U} U_x and that U xU_x is well below UU.)

    I tried various rewordings of the definition of U xU_x, in the hope of finding similar subsets which I can intuitionistically prove to be open, but failed.

    David: Thanks! I fixed that. [I don’t believe that lemma will help us here.]

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 11th 2018

    This is a good question. I’d like to know the answer, but I don’t have any ideas right now. If I had to guess, I would guess that this is not constructively provable, but I don’t have any real basis for that.

    • CommentRowNumber7.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeFeb 12th 2018
    • (edited Feb 12th 2018)

    Hm. Thank you for your assessment! I have to think about this some more. For the record, these are my preliminary observations:

    • In classical logic, the locale XX' is canonically isomorphic to the discrete locale over the set X/X/{\sim}. In particular, despite its appealing universal property in the category of locales, it does not seem to be the right object.
    • We can write down a propositional geometric theory with atomic propositions “#x# x” and “x\sim x” with axioms such as “#x#y{|x#y}#x \Rightarrow #y \vee \bigvee\{\top|x#y\}”. The hope was that because the apartness relation plays a role in the definition of the theory, the resulting classifying locale might be interesting. However it turns out that it is constructively canonically isomorphic to the discrete locale over X/X/{\sim}.
    • We can define the category Set #Set_# of sets-with-apartness-relation, where morphisms are required to be strongly extensional. We then have a fully faithful functor Set #TopSet_# \to Top. I don’t think that there’s a realistic hope for a fully faithful functor Set #LocSet_# \to Loc; however, I hope there is such a functor if we restrict to the subcategory of sets-with-tight-apartness-relation.
    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2018

    Why do you conclude “it does not seem to be the right object” in classical logic? In classical logic that’s just what I would expect; an apartness relation then is just (the negation of) an equivalence relation, and the right thing to do with it is just to take its ordinary quotient.

  1. It depends on what we want, of course. The induced topology on sets-with-apartness-relation enjoys (constructively) the property that continuous maps XYX \to Y bijectively correspond to strongly extensional maps XYX \to Y. However locale morphisms XYX' \to Y' bijectively correspond to (assuming classical logic) arbitrary maps X/Y/X/{\sim} \to Y/{\sim}. If both apartness relations happen to be tight, then there is no difference (still assuming classical logic); but if they aren’t, then there is a difference.

    I’m a bit flexible with what I really want. :-) My real motivation is the following: We can turn a local ring RR into a ring-with-apartness-relation and thus into a topological ring. If AA is an RR-algebra, then there is an induced structure of a topological ring on AA. The classifying locale of the theory of open filters of AA is precisely what algebraic geometers consider when they study the relative spectrum. However, the construction of that theory is ad hoc and only works because the definition of the topology happens to be expressible in geometric logic. I’d like to pass from topological rings to localic rings. Then I have hope that the classifying locale of sublocales which are filters is what I want.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2018

    I think maps between the quotients would be exactly what we want. In the presence of AC, they’re the same (modulo identifying continuous maps that are equivalent with respect to the specialization preorder), but in the absence of AC I would say the point of an equivalence relation (or “anti-equivalence relation”, i.e. apartness relation) is precisely to construct a quotient.

    I’ll need to think some more about local rings.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2018

    I think I probably don’t have anything to say about the local rings, because a “classifying locale of sublocales” sounds like some kind of hyperspace/hyperlocale, which I don’t know anything about.

    • CommentRowNumber12.
    • CommentAuthormartinescardo
    • CommentTimeFeb 12th 2018
    Ingo, could you please elaborate on this: "It’s possible to pass from X to the quotient set X/∼; however, as we know, this loses information and is badly behaved in some sense.".

    In what sense is information lost and in what sense is this quotient badly behaved?
    • CommentRowNumber13.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)

    Mike: Indeed. I’m hoping that the locale I’ll end up with is locally compact. In this case a locale of opens exists, namely the internal Hom to the Sierpinski locale.

    Martín: There is no problem at all if we start with some equivalence relation on XX. In this case, the ordinary set quotient set X/X/{\sim} is just fine. However, if we start with an apartness relation (#)({#}), then information will already be lost if we consider the induced equivalence relation ()({\sim}) defined by xy¬(x#y)x \sim y \Leftrightarrow \neg(x#y), as only the negation of the apartness relation is used, not the apartness relation itself.

    Let XX and YY be sets-with-apartness-relation and assume for a second that the apartness relation on YY is tight, so that we don’t have to deal with the specialization preorder. In this case, set-theoretic maps from X/X/{\sim} to YY are constructively in bijection with those maps XYX \to Y which respect the equivalence relation. I’d like to have some gadget such that morphisms from something related to XX to something related to YY are constructively in bijection with those maps XYX \to Y which reflect the apartness relation (i.e. are strongly extensional). One possibility is to equip XX and YY with the topology described in the first post of this discussion; but I’m led to believe that for my application, topological spaces won’t work and I’d better pass to locales.

    • CommentRowNumber14.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)

    It seems to me that you are looking for the universal strongly extensional map (X,#)(X,#)(X,\#)\to(X',\#') with #\#' a tight apartness (constructively).

    I think it is the quotient, with a suitably defined #\#' on equivalence classes.

    At first sight, the relation xyx\sim y seems to contain negative information only, intuitively. However, let

    1. [x]=[x] = the equivalence class of xx, and
    2. x̲=\underline{x} = the apartness class of xx (set of yy with x#yx\#y).

    Then the apartness axioms give x̲=y̲xy[x]=[y].\underline{x} = \underline{y} \iff x \sim y \iff [x] = [y].

    (Two elements have the same elements apart from them iff they are not apart.)

    On the quotient, you define two equivalence classes AA and BB to be apart iff there are xAx \in A and yBy \in B with x#yx\#y. This apartness is clearly tight (by the very definition of \sim). And the map x[x]x \mapsto [x] is strongly extensional (reflects apartness) by construction. The universality of this map is easy.

    Alternatively, you can construct a universal solution as follows: regard #\# as a map XΩ XX \to \Omega^X, and take its image. Then define u,v:Ω Xu,v: \Omega^X in the image to be apart iff there are xx and yy with u=x̲u=\underline{x}, v=y̲v=\underline{y} and x#yx\#y. Again this apartness is tight and this map reflects apartness by construction, and the universality of the corestriction of #\# to its image, equipped with this apartness relation, is again easy.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2018

    Two elements have the same elements apart from them iff they are not apart.

    That’s really interesting, I hadn’t noticed that before.

    By the way, Martin, you can write basic TeX code here ($x^2$ gives x 2x^2) as long as you select the “Markdown+Itex” radio button below the text entry box.

    • CommentRowNumber16.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)

    Oh, oh. I tried but I think I used more latex than is available. I’ll try to get it right. It may take a few trial-and-error iterations…

    … OK. I think I am done with the LaTeXing of my message. Is there a link with the allowed latex/markdown anywhere?

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2018

    Click on “Help” next to “Markdown+Itex”, then on “iTeX”.

    • CommentRowNumber18.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)

    (Thanks, Mike, for this - I hadn’t noticed the help button and I probably would not have guessed, had I seen it, that it would explain latex.)

    One thing to have in mind is that if a set XX has some tight apartness #\#, then ¬¬(x=y)x=y\neg\neg(x=y) \implies x=y for any x,yXx,y \in X, so that negative information about equality gives positive information about it. (This holds in the reals, Cantor space 2 2^\mathbb{N}, Baire space \mathbb{N}^\mathbb{N}, and more generally in metrizable sets and lots of sets that occur in practice.)

    If the apartness #\# is not necessarily tight, we can only say that ¬¬(x=y)xy\neg\neg(x=y) \implies x \sim y (two not-not-equal elements can’t be apart). The tightness axiom provides a way to turn negative information into positive information (elements that are not apart must be equal). In particular, the tight reflection (as above) identifies not-not-equal things.

    • CommentRowNumber19.
    • CommentAuthormartinescardo
    • CommentTimeFeb 14th 2018
    • (edited Feb 20th 2018)

    I have written the above construction of the tight reflection (the second one only) here in Agda:

    Search for “Apartness” for generalities, and “TightReflection” for what is discussed here. (Unfortunately, it is not possible at the moment to provide direct links to the relevant parts of this file, because minimal changes to the source break the links in the automatically generated html.)

    This uses univalent foundations, but only its 1-topos fragment, so to speak. Although one can consider apartness in arbitrary types, the ones which have tight apartness are sets, and hence the tight reflection of any apartness type is a set.

    (The source is also in my github project TypeTopology.)