Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeFeb 10th 2018
   • (edited Feb 10th 2018)
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexLet $X$ be a set with an [[apartness relation]]. We can then define a subset $U$ of $X$ to be open if and only if $$ \forall x, y. (x \in U \Rightarrow y \in U \vee x # y). $$ In that way, $X$ becomes a topological space. As detailed at _[[apartness relation]]_, the induced locale $X'$ can be described as a certain quotient of the discrete locale over $X$ in the category of locales. I'm trying to work out what the points of this locale are. The canonical continuous map $$ X \longrightarrow Pt(X'), x \mapsto \{ U \subseteq X | U open, x \in U \} $$ factors over $X/\sim$, where $({\sim})$ is the equivalence relation induced by the apartness, and I can show that the resulting map ${X/{\sim}} \to Pt(X')$ is injective. Is it surjective? (Assuming classical logic, it is. In this case furthermore $X'$ is a locally compact locale. But I need an intuitionistic proof.) My motivation is as follows. It's possible to pass from $X$ to the quotient set $X/{\sim}$; however, as we know, this loses information and is badly behaved in some sense. If the points of $X'$ turned out to be the elements of $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."

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

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

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

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

   $$X \longrightarrow Pt(X'), x \mapsto \{ U \subseteq X | U open, x \in U \}$$

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

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

   My motivation is as follows. It’s possible to pass from $X$ to the quotient set $X/{\sim}$; however, as we know, this loses information and is badly behaved in some sense. If the points of $X'$ turned out to be the elements of $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.”

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 11th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIn other words, the question is whether the apartness topology on $X$ is sober?

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

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 11th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, 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?

   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?

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeFeb 11th 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAs an aside, at [[sober space]] there is a broken reference >`\ref{OpenSubsetVersionOfClosedIrreducible}`

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

   \ref{OpenSubsetVersionOfClosedIrreducible}

5. • CommentRowNumber5.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeFeb 11th 2018
   • (edited Feb 11th 2018)
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexMike: Yes, exactly. The proof in classical logic exploits the subsets $$ 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 $F$ be a completely prime filter. Since $X = \bigcup_{x \in X} U_x \in F$, there is an element $x \in X$ such that $U_x \in F$. One can then show that $F$ is the image of $[x]$. To verify that $X'$ is locally compact, observe that any open subset $U$ can be written as the union $\bigcup_{x \in U} U_x$ and that $U_x$ is well below $U$.) I tried various rewordings of the definition of $U_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.]

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

   $$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 $F$ be a completely prime filter. Since $X = \bigcup_{x \in X} U_x \in F$, there is an element $x \in X$ such that $U_x \in F$. One can then show that $F$ is the image of $[x]$. To verify that $X'$ is locally compact, observe that any open subset $U$ can be written as the union $\bigcup_{x \in U} U_x$ and that $U_x$ is well below $U$.)

   I tried various rewordings of the definition of $U_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.]

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 11th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThis 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeFeb 12th 2018
   • (edited Feb 12th 2018)
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexHm. 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 $X'$ is canonically isomorphic to the discrete locale over the set $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$" and "$\sim x$" with axioms such as "$#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/{\sim}$. * We can define the category $Set_#$ of sets-with-apartness-relation, where morphisms are required to be strongly extensional. We then have a fully faithful functor $Set_# \to Top$. I don't think that there's a realistic hope for a fully faithful functor $Set_# \to Loc$; however, I hope there is such a functor if we restrict to the subcategory of sets-with-tight-apartness-relation.

   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 $X'$ is canonically isomorphic to the discrete locale over the set $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$” and “$\sim x$” with axioms such as “$#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/{\sim}$.
   • We can define the category $Set_#$ of sets-with-apartness-relation, where morphisms are required to be strongly extensional. We then have a fully faithful functor $Set_# \to Top$. I don’t think that there’s a realistic hope for a fully faithful functor $Set_# \to Loc$; however, I hope there is such a functor if we restrict to the subcategory of sets-with-tight-apartness-relation.
8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 12th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhy 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeFeb 12th 2018
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexIt depends on what we want, of course. The induced topology on sets-with-apartness-relation enjoys (constructively) the property that continuous maps $X \to Y$ bijectively correspond to strongly extensional maps $X \to Y$. However locale morphisms $X' \to Y'$ bijectively correspond to (assuming classical logic) arbitrary maps $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 $R$ into a ring-with-apartness-relation and thus into a topological ring. If $A$ is an $R$-algebra, then there is an induced structure of a topological ring on $A$. The classifying locale of the theory of open filters of $A$ 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.

   It depends on what we want, of course. The induced topology on sets-with-apartness-relation enjoys (constructively) the property that continuous maps $X \to Y$ bijectively correspond to strongly extensional maps $X \to Y$. However locale morphisms $X' \to Y'$ bijectively correspond to (assuming classical logic) arbitrary maps $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 $R$ into a ring-with-apartness-relation and thus into a topological ring. If $A$ is an $R$-algebra, then there is an induced structure of a topological ring on $A$. The classifying locale of the theory of open filters of $A$ 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.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 12th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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.

    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.

12. • CommentRowNumber12.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • PermaLink
    Author: martinescardo
    Format: TextIngo, 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?

    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?
13. • CommentRowNumber13.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)
    • PermaLink
    Author: IngoBlechschmidt
    Format: MarkdownItexMike: 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 $X$. In this case, the ordinary set quotient set $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 $x \sim y \Leftrightarrow \neg(x#y)$, as only the negation of the apartness relation is used, not the apartness relation itself. Let $X$ and $Y$ be sets-with-apartness-relation and assume for a second that the apartness relation on $Y$ is tight, so that we don't have to deal with the specialization preorder. In this case, set-theoretic maps from $X/{\sim}$ to $Y$ are constructively in bijection with those maps $X \to Y$ which respect the equivalence relation. I'd like to have some gadget such that morphisms from something related to $X$ to something related to $Y$ are constructively in bijection with those maps $X \to Y$ which reflect the apartness relation (i.e. are strongly extensional). One possibility is to equip $X$ and $Y$ 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.

    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 $X$. In this case, the ordinary set quotient set $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 $x \sim y \Leftrightarrow \neg(x#y)$, as only the negation of the apartness relation is used, not the apartness relation itself.

    Let $X$ and $Y$ be sets-with-apartness-relation and assume for a second that the apartness relation on $Y$ is tight, so that we don’t have to deal with the specialization preorder. In this case, set-theoretic maps from $X/{\sim}$ to $Y$ are constructively in bijection with those maps $X \to Y$ which respect the equivalence relation. I’d like to have some gadget such that morphisms from something related to $X$ to something related to $Y$ are constructively in bijection with those maps $X \to Y$ which reflect the apartness relation (i.e. are strongly extensional). One possibility is to equip $X$ and $Y$ 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.

14. • CommentRowNumber14.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)
    • PermaLink
    Author: martinescardo
    Format: MarkdownItexIt seems to me that you are looking for the universal strongly extensional map $(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 $x\sim y$ seems to contain negative information only, intuitively. However, let 1. $[x] =$ the equivalence class of $x$, and 1. $\underline{x} =$ the apartness class of $x$ (set of $y$ with $x\#y$). Then the apartness axioms give $\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 $A$ and $B$ to be apart iff there are $x \in A$ and $y \in B$ with $x\#y$. This apartness is clearly tight (by the very definition of $\sim$). And the map $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 \to \Omega^X$, and take its image. Then define $u,v: \Omega^X$ in the image to be apart iff there are $x$ and $y$ with $u=\underline{x}$, $v=\underline{y}$ and $x\#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.

    It seems to me that you are looking for the universal strongly extensional map $(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 $x\sim y$ seems to contain negative information only, intuitively. However, let

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

    Then the apartness axioms give $\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 $A$ and $B$ to be apart iff there are $x \in A$ and $y \in B$ with $x\#y$. This apartness is clearly tight (by the very definition of $\sim$). And the map $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 \to \Omega^X$, and take its image. Then define $u,v: \Omega^X$ in the image to be apart iff there are $x$ and $y$ with $u=\underline{x}$, $v=\underline{y}$ and $x\#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.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> 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^2$) as long as you select the "Markdown+Itex" radio button below the text entry box.

    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^2$) as long as you select the “Markdown+Itex” radio button below the text entry box.

16. • CommentRowNumber16.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)
    • PermaLink
    Author: martinescardo
    Format: MarkdownItexOh, 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?

    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?

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 13th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexClick on "Help" next to "Markdown+Itex", then on "iTeX".

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

18. • CommentRowNumber18.
    • CommentAuthormartinescardo
    • CommentTimeFeb 13th 2018
    • (edited Feb 13th 2018)
    • PermaLink
    Author: martinescardo
    Format: MarkdownItex(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 $X$ has some tight apartness $\#$, then $\neg\neg(x=y) \implies x=y$ for any $x,y \in X$, so that negative information about equality gives positive information about it. (This holds in the reals, Cantor space $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 $\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.

    (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 $X$ has some tight apartness $\#$, then $\neg\neg(x=y) \implies x=y$ for any $x,y \in X$, so that negative information about equality gives positive information about it. (This holds in the reals, Cantor space $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 $\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.

19. • CommentRowNumber19.
    • CommentAuthormartinescardo
    • CommentTimeFeb 15th 2018
    • (edited Feb 20th 2018)
    • PermaLink
    Author: martinescardo
    Format: MarkdownItexI have written the above construction of the tight reflection (the second one only) here in Agda: * [tight reflection](http://www.cs.bham.ac.uk/~mhe/agda-new/TotallySeparated.html#Apartness.reflexive) 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.)

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

    • tight reflection

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