Timeline for Tight apartness relations in toposes
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 23, 2020 at 20:10 | history | edited | Valery Isaev | CC BY-SA 4.0 |
added 285 characters in body
|
| Feb 23, 2020 at 17:58 | history | became hot network question | |||
| Feb 23, 2020 at 16:27 | comment | added | Valery Isaev | @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. | |
| Feb 23, 2020 at 16:11 | comment | added | Valery Isaev | @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. | |
| Feb 23, 2020 at 16:04 | comment | added | Valery Isaev | @IngoBlechschmidt Yes, you're right. I just was confused. I deleted my comment. | |
| Feb 23, 2020 at 16:01 | comment | added | Tim Campion | @ValeryIsaev Surely you're right. Just to clarify (since it's the "tight"-ness part that has me confused more so than the "apartness" part), you're saying that in a topos, $\mathbb N^{\mathbb N}$ and $\mathbb R$ have tight apartness relations, right? BTW is there a name for objects $X$ with $\neg\neg$-dense diagonal? I didn't realize there was a condition like this on the equality relation intermediate between decidability and non-decidability... | |
| Feb 23, 2020 at 15:48 | comment | added | Ingo Blechschmidt | @ValeryIsaev: Can you clarify? The condition "$\forall x,y : M. \neg\neg(x = y) \Rightarrow x = y$", interpreted in the internal language, is exactly the condition for the object $M$ to be separated with respect to the $\neg\neg$-topology. | |
| Feb 23, 2020 at 15:41 | answer | added | Ingo Blechschmidt | timeline score: 12 | |
| Feb 23, 2020 at 13:46 | comment | added | Valery Isaev | @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. | |
| Feb 23, 2020 at 11:48 | comment | added | Bas Spitters | The relation with the Hausdorff topology may be helpful. | |
| Feb 23, 2020 at 6:48 | comment | added | Tim Campion | 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? | |
| Feb 23, 2020 at 3:12 | history | asked | Valery Isaev | CC BY-SA 4.0 |