10
$\begingroup$

A tight apartness relation on a set is a binary relation $\#$ such that the following conditions hold:

  • $x = y$ if and only if $\neg (x \# y)$.
  • If $x \# y$, then $y \# x$.
  • If $x \# z$, then either $x \# y$ or $y \# z$ for every $y$.

I want to understand this notion better. Classically, it is completely trivial. Thus, it makes sense to look at it in various toposes. I tried to use the Kripke-Joyal semantics to get the external interpretation of an arbitrary object of a topos with a tight apartness relation, but it seems that it does not give anything particularly interesting in general. Thus, I've got the following question:

Question: What are examples of objects in toposes with a tight apartness relation which externally correspond to some interesting or useful notion?

Since constructively, a set can have more than one tight apartness relation on it, I'd like to see examples of an object with two different tight apartness relations which both have interesting interpretations.

Edit: There are several "generic" examples of objects with tight apartness relations, i.e., objects that can be defined in every topos (e.g., Dedekind reals). I'm particularly interested in "non-generic" examples, i.e., objects that can be constructed only in a specific topos.

Improve this question
$\endgroup$
8
  • $\begingroup$ I'm a little out of my depth here, but I think the first bullet point tells you that in a topos, any object admitting an apartness relation must have decidable equality. I think the first two toposes I tend to think of besides $Set$ are $sSet$ and sheaves on a topological space $X$. In $sSet$, I think maybe only discrete objects have decidable equality? And in $Sh(X)$, maybe it's just coproducts of representables on clopen sets? $\endgroup$
    – Tim Campion
    Commented Feb 23, 2020 at 6:48
  • 1
    $\begingroup$ The relation with the Hausdorff topology may be helpful. $\endgroup$
    – Bas Spitters
    Commented Feb 23, 2020 at 11:48
  • 4
    $\begingroup$ @TimCampion It does not imply decidability of equality, it only implies that it is $\neg \neg$-separated. There are plenty of examples of objects with an apartness relation and without decidable equality. E.g., functions $\mathbb{N} \to \mathbb{N}$ and Dedekind reals. $\endgroup$
    – Valery Isaev
    Commented Feb 23, 2020 at 13:46
  • 1
    $\begingroup$ @TimCampion Yes, they both carry a tight apartness relation. Also, my second comment was completely wrong. First, the condition "$\neg \neg x = y \implies x = y$" is equivalent to the diagonal being $\neg \neg$-closed and not $\neg \neg$-dense. Second, as Ingo pointed out, it is actually equivalent to the object being $\neg \neg$-separated. $\endgroup$
    – Valery Isaev
    Commented Feb 23, 2020 at 16:11
  • 1
    $\begingroup$ @TimCampion I'm asking about tight apartness relations because every apartness relation on $X$ determine a tight one on a quotient of $X$. For example, the relation "$(x - y)$ is a unit" on a local ring is an apartness relation. The corresponding ideal is (the unique) maximal ideal consisting of non-units, the quotient is a Heyting field, and the tight apartness relation on this field is the same as before. Thus, I believe that, to understand apartness relations, it is enough to understand tight ones. $\endgroup$
    – Valery Isaev
    Commented Feb 23, 2020 at 16:27

1 Answer 1

Reset to default
12
$\begingroup$

I'm not precisely sure what you're looking for. Here is an example for the external interpretation of an apartness relation:

Recall that the object of Dedekind reals $\mathbb{R}$ in a sheaf topos $\mathrm{Sh}(X)$ is the sheaf $\mathcal{C}$ of continuous (Dedekind-)real-valued functions on $X$.

The apartness relation on $\mathbb{R}$, defined by $x \mathrel{\#} y \Longleftrightarrow x - y \text{ is invertible}$, is then the following subsheaf $\mathcal{E}$ of $\mathcal{C} \times \mathcal{C}$:

$$ \mathcal{E}(U) = \{ (f,g) \,|\, \text{for all $x \in U$: $f(x) - g(x) \in \mathbb{R}$ is invertible} \} $$

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ I'd like to see more examples like this one, but I think even more interesting are non-generic examples. That is, objects with tight apartness relations that can be constructed only in some particular topos (here, $\mathbb{R}$ can be constructed in any topos). $\endgroup$
    – Valery Isaev
    Commented Feb 23, 2020 at 16:55
  • 1
    $\begingroup$ @ValeryIsaev I think it would be a good idea to include this requirement into your question. $\endgroup$
    – Martin Brandenburg
    Commented Feb 23, 2020 at 19:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .