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.
I have added statement and proof (here) that in the category of Hausdorff spaces, inclusions of dense subsets are epi.
Briefly mentioned the converse and added pointer to
Surely a much cleaner proof is to recognize that the equalizer of two morphisms can be computed as a pullback
where is a closed inclusion, by Hausdorffness. By continuity, the pullback inclusion is also closed. By assumption, this inclusion contains a dense subset . Being therefore dense and closed, is all of . Hence on all of .
(By the way, this description of an equalizer as a pullback should probably replace what is currently at equalizer. I can get to this later.)
Sorry about the deletion.
I don’t think of one as being “abstract” and the other as being “explicit” – they are both quite explicit. (For example, that “dense” means the closure is the entire space is the very first line of dense subspace.) And “abstract” is for some people a skunked term. Thus I slightly adjusted the language.
added pointer to:
Added:
First introduced by Hausdorff in Grundzüge der Mengenlehre, Hausdorff spaces were the original concept of a topological space. Later the Hausdorffness condition was dropped, apparently first by Kuratowski in 1920s.
1 to 15 of 15