topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
A covert space is a topological space $X$ such that the unique map $X\to 1$ to the terminal point space is a closed map.
This should be compared with overt spaces, where $X\to 1$ is an open map, and compact spaces, where $X\to 1$ is a proper map. Since proper maps are closed, all compact spaces are covert.
In classical mathematics, every topological space is covert, just as every space is overt. However, in constructive mathematics, and in particular in synthetic topology, covertness can be a strong condition that already carries much of the power of compactness.
A locale $X$ is covert if the unique map $X\to 1$ is a closed map of locales, i.e. the adjunction $f^* : O(1) \rightleftarrows O(X) : f_*$ satisfies the Frobenius reciprocity condition $f_*(U\cup f^*(V)) = f_*(U)\cup V$.
If excluded middle holds, then every locale is covert.
Constructively, covertness is already interesting when $X$ is a set with the discrete topology. In this case, since $O(1) = P(1)$ is the poset of truth values (the subobject classifier) and $O(X)=P(X)$ is the powerset of $X$, covertness of $X$ can be expressed more logically as
if $P$ is a proposition and $Q$ a predicate on $X$ such that $\forall x\in X, (P \vee Q(x))$, then $P\vee (\forall x\in X, Q(x))$.
This is always true if $X$ is (Kuratowski) finite (in which case the discrete topology on $X$ is not just covert but compact), but in general it can be quite a strong condition.
In synthetic topology, covertness of sets carries much of the strength of compactness. (Note that here we are talking about covertness of sets — i.e. “spaces” in the sense of synthetic topology, i.e. basic objects of our foundational system — equipped with the “discrete topology” internal to our synthetic-topological formal system; these are quite different from sets whose intrinsic synthetic topology is discrete.) For instance, in various gros toposes of topological, smooth, or algebraic spaces, the covert spaces are precisely the compact ones; see Dubuc-Penon (who call covert sets “compact”).
Covert sets also satisfy the following property.
If $X$ is covert, then for any two predicates $P,Q$ on $X$ such that $\forall x\in X, (P(x) \vee Q(x))$, we have either $\exists x\in X, P(x)$ or $\forall x\in X, Q(x)$.
Let $P'$ be the proposition $\exists x\in X, P(x)$ in the defining property of covertness for $X$.
Note that if $P$ and $Q$ are incompatible (i.e. $\neg (P(x)\wedge Q(x))$), then this becomes the limited principle of omniscience for $A$. Thus, every covert set is omniscient?.
A locale $X$ is defined to be compact if its top element is inaccessible by directed joins, i.e. if $X = \bigvee S$ for some directed set $S\subseteq O(X)$ implies $X\le U$ for some $U\in S$. Since the right adjoint part $r_*$ of the locale morphism $r:X\to 1$ is defined by $r_*(U) = (U=X)$ (a truth value, since $O(1) = \Omega$ is the subobject classifier), this is equivalent to asking that $r_*$ preserve directed joins.
Contrary to a remark in Sketches of an Elephant, this condition implies that $X$ is covert, even constructively (and therefore if $X$ is compact then $X\to 1$ is a proper map, without the need to modify the notion of “compact locale”). For suppose $U\in O(X)$ and $V\in O(1) = \Omega$; we must show that if $r_\ast(U \cup r_\ast(V))$ is true, then so is $r_\ast(U) \cup V$. As remarked above, $r_\ast(W)$ is the truth value of the statement “$W=X$”, while $r^*(P) = \bigcup \{ X \mid P \}$. Suppose $r_\ast(U \cup r_\ast(V))$, i.e. that $U\cup \bigcup \{ X \mid V \} = X$. Now consider the set $\{ W\in O(X) \mid V \vee (W\le U) \}$; this is evidently directed, and our supposition in the last sentence says exactly that its union is $X$. Therefore, if $X$ is compact, there exists a $W$ such that $V \vee (W\le U)$ and $X\le W$. In other words, either $V$ or $X\le U$, i.e. either $V$ or $r_\ast(U)$, which is what we wanted. This proof appears to be due to Vermeulen.
Eduardo Dubuc and Jacques Penon, Objets compacts dans les topos,
Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics, 40(2), 1986, p. 203–217. doi:10.1017/S144678870002718X
Vermeulen, Proper maps of locales, Journal of Pure and Applied Algebra, 92, 1994, p. 79–107. (pdf (core.ac.uk))