Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added some discussion to Hausdorff space of how the localic and spatial versions compare in classical and constructive mathematics, including in particular the fact that I just learned (in discussion with Martin Escardo and Andrej Bauer) that a discrete locale is Hausdorff iff it has decidable equality.
I added to Hausdorff space a theorem characterizing some localically strongly Hausdorff spaces in terms of apartness relations, which is a sort of dual or converse to the theorem I recently added to apartness relation.
Clarified a confusing remark about separatedness in different categories. A separated scheme is certainly not the same thing as a scheme whose underlying Zariski locale is Hausdorff. I doubt even that a separated scheme is the same thing as a scheme whose underlying Zariski locale is separated over the classifying topos for local rings.
Re #4: This notion of “inclusion” is discussed at sublocale.
1 to 5 of 5