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 $f, g: X \rightrightarrows Y$ can be computed as a pullback
$\array{ E & \to & Y \\ \downarrow & & \downarrow \mathrlap{\delta} \\ X & \underset{(f, g)}{\to} & Y \times Y }$where $\delta: Y \to Y \times Y$ is a closed inclusion, by Hausdorffness. By continuity, the pullback inclusion $E \to X$ is also closed. By assumption, this inclusion contains a dense subset $A \hookrightarrow X$. Being therefore dense and closed, $E \to X$ is all of $X$. Hence $f = g$ on all of $X$.
(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:
1 to 14 of 14